Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdlemkuu Structured version   Unicode version

Theorem cdlemkuu 31766
 Description: Convert between function and operation forms of . TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013.)
Hypotheses
Ref Expression
cdlemk3.b
cdlemk3.l
cdlemk3.j
cdlemk3.m
cdlemk3.a
cdlemk3.h
cdlemk3.t
cdlemk3.r
cdlemk3.s
cdlemk3.u1
cdlemk3.o2
cdlemk3.u2
Assertion
Ref Expression
cdlemkuu
Distinct variable groups:   ,,,,   ,   ,,,,   ,   ,,,,,   ,,   ,,,   ,   ,   ,,   ,,,,   ,,   ,,,,   ,,,,   ,,,,
Allowed substitution hints:   (,,,)   (,,,,)   ()   (,,)   ()   (,,,,)   ()   (,,)   (,)   (,,,)   ()   (,,,)   (,,,)   ()   (,,)   ()   (,,,,)   (,,,,)

Proof of Theorem cdlemkuu
StepHypRef Expression
1 fveq2 5731 . . . . . . . . 9
2 cdlemk3.o2 . . . . . . . . 9
31, 2syl6eqr 2488 . . . . . . . 8
43fveq1d 5733 . . . . . . 7
5 cnveq 5049 . . . . . . . . 9
65coeq2d 5038 . . . . . . . 8
76fveq2d 5735 . . . . . . 7
84, 7oveq12d 6102 . . . . . 6
98oveq2d 6100 . . . . 5
109eqeq2d 2449 . . . 4
1110riotabidv 6554 . . 3
12 fveq2 5731 . . . . . . 7
1312oveq2d 6100 . . . . . 6
14 coeq1 5033 . . . . . . . 8
1514fveq2d 5735 . . . . . . 7
1615oveq2d 6100 . . . . . 6
1713, 16oveq12d 6102 . . . . 5
1817eqeq2d 2449 . . . 4
1918riotabidv 6554 . . 3
20 cdlemk3.u1 . . 3
21 riotaex 6556 . . 3
2211, 19, 20, 21ovmpt2 6212 . 2
23 cdlemk3.b . . . 4
24 cdlemk3.l . . . 4
25 cdlemk3.j . . . 4
26 cdlemk3.a . . . 4
27 cdlemk3.h . . . 4
28 cdlemk3.t . . . 4
29 cdlemk3.r . . . 4
30 cdlemk3.m . . . 4
31 cdlemk3.u2 . . . 4
3223, 24, 25, 26, 27, 28, 29, 30, 31cdlemksv 31715 . . 3