Metamath Proof Explorer

Theorem ccfldsrarelvec

Description: The subring algebra of the complex numbers over the real numbers is a left vector space. (Contributed by Thierry Arnoux, 20-Aug-2023)

Ref Expression
Assertion ccfldsrarelvec 
|- ( ( subringAlg ` CCfld ) ` RR ) e. LVec

Proof

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 mullidd 
 |-  ( ( 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