Step |
Hyp |
Ref |
Expression |
1 |
|
cnring |
|- CCfld e. Ring |
2 |
|
ax-resscn |
|- RR C_ CC |
3 |
|
eqidd |
|- ( T. -> ( ( subringAlg ` CCfld ) ` RR ) = ( ( subringAlg ` CCfld ) ` RR ) ) |
4 |
3
|
mptru |
|- ( ( subringAlg ` CCfld ) ` RR ) = ( ( subringAlg ` CCfld ) ` RR ) |
5 |
|
cnfldbas |
|- CC = ( Base ` CCfld ) |
6 |
4 5
|
sraring |
|- ( ( CCfld e. Ring /\ RR C_ CC ) -> ( ( subringAlg ` CCfld ) ` RR ) e. Ring ) |
7 |
1 2 6
|
mp2an |
|- ( ( subringAlg ` CCfld ) ` RR ) e. Ring |
8 |
|
ringgrp |
|- ( ( ( subringAlg ` CCfld ) ` RR ) e. Ring -> ( ( subringAlg ` CCfld ) ` RR ) e. Grp ) |
9 |
7 8
|
ax-mp |
|- ( ( subringAlg ` CCfld ) ` RR ) e. Grp |
10 |
|
refld |
|- RRfld e. Field |
11 |
|
isfld |
|- ( RRfld e. Field <-> ( RRfld e. DivRing /\ RRfld e. CRing ) ) |
12 |
10 11
|
mpbi |
|- ( RRfld e. DivRing /\ RRfld e. CRing ) |
13 |
12
|
simpli |
|- RRfld e. DivRing |
14 |
|
drngring |
|- ( RRfld e. DivRing -> RRfld e. Ring ) |
15 |
13 14
|
ax-mp |
|- RRfld e. Ring |
16 |
|
simpr1 |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> b e. RR ) |
17 |
16
|
recnd |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> b e. CC ) |
18 |
|
simpr3 |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> y e. CC ) |
19 |
17 18
|
mulcld |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> ( b x. y ) e. CC ) |
20 |
|
simpr2 |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> x e. CC ) |
21 |
17 18 20
|
adddid |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> ( b x. ( y + x ) ) = ( ( b x. y ) + ( b x. x ) ) ) |
22 |
|
simpl |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> a e. RR ) |
23 |
22
|
recnd |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> a e. CC ) |
24 |
23 17 18
|
adddird |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) |
25 |
19 21 24
|
3jca |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> ( ( b x. y ) e. CC /\ ( b x. ( y + x ) ) = ( ( b x. y ) + ( b x. x ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) ) |
26 |
23 17 18
|
mulassd |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> ( ( a x. b ) x. y ) = ( a x. ( b x. y ) ) ) |
27 |
18
|
mulid2d |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> ( 1 x. y ) = y ) |
28 |
25 26 27
|
jca32 |
|- ( ( a e. RR /\ ( b e. RR /\ x e. CC /\ y e. CC ) ) -> ( ( ( b x. y ) e. CC /\ ( b x. ( y + x ) ) = ( ( b x. y ) + ( b x. x ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) /\ ( ( ( a x. b ) x. y ) = ( a x. ( b x. y ) ) /\ ( 1 x. y ) = y ) ) ) |
29 |
28
|
ralrimivvva |
|- ( a e. RR -> A. b e. RR A. x e. CC A. y e. CC ( ( ( b x. y ) e. CC /\ ( b x. ( y + x ) ) = ( ( b x. y ) + ( b x. x ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) /\ ( ( ( a x. b ) x. y ) = ( a x. ( b x. y ) ) /\ ( 1 x. y ) = y ) ) ) |
30 |
29
|
rgen |
|- A. a e. RR A. b e. RR A. x e. CC A. y e. CC ( ( ( b x. y ) e. CC /\ ( b x. ( y + x ) ) = ( ( b x. y ) + ( b x. x ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) /\ ( ( ( a x. b ) x. y ) = ( a x. ( b x. y ) ) /\ ( 1 x. y ) = y ) ) |
31 |
2 5
|
sseqtri |
|- RR C_ ( Base ` CCfld ) |
32 |
31
|
a1i |
|- ( T. -> RR C_ ( Base ` CCfld ) ) |
33 |
3 32
|
srabase |
|- ( T. -> ( Base ` CCfld ) = ( Base ` ( ( subringAlg ` CCfld ) ` RR ) ) ) |
34 |
33
|
mptru |
|- ( Base ` CCfld ) = ( Base ` ( ( subringAlg ` CCfld ) ` RR ) ) |
35 |
5 34
|
eqtri |
|- CC = ( Base ` ( ( subringAlg ` CCfld ) ` RR ) ) |
36 |
|
cnfldadd |
|- + = ( +g ` CCfld ) |
37 |
3 32
|
sraaddg |
|- ( T. -> ( +g ` CCfld ) = ( +g ` ( ( subringAlg ` CCfld ) ` RR ) ) ) |
38 |
37
|
mptru |
|- ( +g ` CCfld ) = ( +g ` ( ( subringAlg ` CCfld ) ` RR ) ) |
39 |
36 38
|
eqtri |
|- + = ( +g ` ( ( subringAlg ` CCfld ) ` RR ) ) |
40 |
|
cnfldmul |
|- x. = ( .r ` CCfld ) |
41 |
3 32
|
sravsca |
|- ( T. -> ( .r ` CCfld ) = ( .s ` ( ( subringAlg ` CCfld ) ` RR ) ) ) |
42 |
41
|
mptru |
|- ( .r ` CCfld ) = ( .s ` ( ( subringAlg ` CCfld ) ` RR ) ) |
43 |
40 42
|
eqtri |
|- x. = ( .s ` ( ( subringAlg ` CCfld ) ` RR ) ) |
44 |
|
df-refld |
|- RRfld = ( CCfld |`s RR ) |
45 |
3 32
|
srasca |
|- ( T. -> ( CCfld |`s RR ) = ( Scalar ` ( ( subringAlg ` CCfld ) ` RR ) ) ) |
46 |
45
|
mptru |
|- ( CCfld |`s RR ) = ( Scalar ` ( ( subringAlg ` CCfld ) ` RR ) ) |
47 |
44 46
|
eqtri |
|- RRfld = ( Scalar ` ( ( subringAlg ` CCfld ) ` RR ) ) |
48 |
|
rebase |
|- RR = ( Base ` RRfld ) |
49 |
|
replusg |
|- + = ( +g ` RRfld ) |
50 |
|
remulr |
|- x. = ( .r ` RRfld ) |
51 |
|
re1r |
|- 1 = ( 1r ` RRfld ) |
52 |
35 39 43 47 48 49 50 51
|
islmod |
|- ( ( ( subringAlg ` CCfld ) ` RR ) e. LMod <-> ( ( ( subringAlg ` CCfld ) ` RR ) e. Grp /\ RRfld e. Ring /\ A. a e. RR A. b e. RR A. x e. CC A. y e. CC ( ( ( b x. y ) e. CC /\ ( b x. ( y + x ) ) = ( ( b x. y ) + ( b x. x ) ) /\ ( ( a + b ) x. y ) = ( ( a x. y ) + ( b x. y ) ) ) /\ ( ( ( a x. b ) x. y ) = ( a x. ( b x. y ) ) /\ ( 1 x. y ) = y ) ) ) ) |
53 |
9 15 30 52
|
mpbir3an |
|- ( ( subringAlg ` CCfld ) ` RR ) e. LMod |
54 |
47
|
islvec |
|- ( ( ( subringAlg ` CCfld ) ` RR ) e. LVec <-> ( ( ( subringAlg ` CCfld ) ` RR ) e. LMod /\ RRfld e. DivRing ) ) |
55 |
53 13 54
|
mpbir2an |
|- ( ( subringAlg ` CCfld ) ` RR ) e. LVec |