Metamath Proof Explorer

Theorem recvs

Description: The field of the real numbers as left module over itself is a subcomplex vector space. The vector operation is + , and the scalar product is x. . (Contributed by AV, 22-Oct-2021)

Ref Expression
Hypothesis recvs.r 
|- R = ( ringLMod ` RRfld )
Assertion recvs 
|- R e. CVec

Proof

Step Hyp Ref Expression
1 recvs.r 
 |-  R = ( ringLMod ` RRfld )
2 refld 
 |-  RRfld e. Field
3 fldidom 
 |-  ( RRfld e. Field -> RRfld e. IDomn )
4 isidom 
 |-  ( RRfld e. IDomn <-> ( RRfld e. CRing /\ RRfld e. Domn ) )
5 crngring 
 |-  ( RRfld e. CRing -> RRfld e. Ring )
6 5 adantr 
 |-  ( ( RRfld e. CRing /\ RRfld e. Domn ) -> RRfld e. Ring )
7 4 6 sylbi 
 |-  ( RRfld e. IDomn -> RRfld e. Ring )
8 3 7 syl 
 |-  ( RRfld e. Field -> RRfld e. Ring )
9 2 8 ax-mp 
 |-  RRfld e. Ring
10 rlmlmod 
 |-  ( RRfld e. Ring -> ( ringLMod ` RRfld ) e. LMod )
11 9 10 ax-mp 
 |-  ( ringLMod ` RRfld ) e. LMod
12 rlmsca 
 |-  ( RRfld e. Field -> RRfld = ( Scalar ` ( ringLMod ` RRfld ) ) )
13 2 12 ax-mp 
 |-  RRfld = ( Scalar ` ( ringLMod ` RRfld ) )
14 df-refld 
 |-  RRfld = ( CCfld |`s RR )
15 13 14 eqtr3i 
 |-  ( Scalar ` ( ringLMod ` RRfld ) ) = ( CCfld |`s RR )
16 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
17 16 simpli 
 |-  RR e. ( SubRing ` CCfld )
18 eqid 
 |-  ( Scalar ` ( ringLMod ` RRfld ) ) = ( Scalar ` ( ringLMod ` RRfld ) )
19 18 isclmi 
 |-  ( ( ( ringLMod ` RRfld ) e. LMod /\ ( Scalar ` ( ringLMod ` RRfld ) ) = ( CCfld |`s RR ) /\ RR e. ( SubRing ` CCfld ) ) -> ( ringLMod ` RRfld ) e. CMod )
20 11 15 17 19 mp3an 
 |-  ( ringLMod ` RRfld ) e. CMod
21 16 simpri 
 |-  RRfld e. DivRing
22 rlmlvec 
 |-  ( RRfld e. DivRing -> ( ringLMod ` RRfld ) e. LVec )
23 21 22 ax-mp 
 |-  ( ringLMod ` RRfld ) e. LVec
24 20 23 elini 
 |-  ( ringLMod ` RRfld ) e. ( CMod i^i LVec )
25 df-cvs 
 |-  CVec = ( CMod i^i LVec )
26 24 1 25 3eltr4i 
 |-  R e. CVec