This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) (Proof shortened by SN, 23-Nov-2024)

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 isfld 
 |-  ( RRfld e. Field <-> ( RRfld e. DivRing /\ RRfld e. CRing ) )
4 3 simprbi 
 |-  ( RRfld e. Field -> RRfld e. CRing )
5 4 crngringd 
 |-  ( RRfld e. Field -> RRfld e. Ring )
6 rlmlmod 
 |-  ( RRfld e. Ring -> ( ringLMod ` RRfld ) e. LMod )
7 2 5 6 mp2b 
 |-  ( ringLMod ` RRfld ) e. LMod
8 rlmsca 
 |-  ( RRfld e. Field -> RRfld = ( Scalar ` ( ringLMod ` RRfld ) ) )
9 2 8 ax-mp 
 |-  RRfld = ( Scalar ` ( ringLMod ` RRfld ) )
10 df-refld 
 |-  RRfld = ( CCfld |`s RR )
11 9 10 eqtr3i 
 |-  ( Scalar ` ( ringLMod ` RRfld ) ) = ( CCfld |`s RR )
12 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
13 12 simpli 
 |-  RR e. ( SubRing ` CCfld )
14 eqid 
 |-  ( Scalar ` ( ringLMod ` RRfld ) ) = ( Scalar ` ( ringLMod ` RRfld ) )
15 14 isclmi 
 |-  ( ( ( ringLMod ` RRfld ) e. LMod /\ ( Scalar ` ( ringLMod ` RRfld ) ) = ( CCfld |`s RR ) /\ RR e. ( SubRing ` CCfld ) ) -> ( ringLMod ` RRfld ) e. CMod )
16 7 11 13 15 mp3an 
 |-  ( ringLMod ` RRfld ) e. CMod
17 12 simpri 
 |-  RRfld e. DivRing
18 rlmlvec 
 |-  ( RRfld e. DivRing -> ( ringLMod ` RRfld ) e. LVec )
19 17 18 ax-mp 
 |-  ( ringLMod ` RRfld ) e. LVec
20 16 19 elini 
 |-  ( ringLMod ` RRfld ) e. ( CMod i^i LVec )
21 df-cvs 
 |-  CVec = ( CMod i^i LVec )
22 20 1 21 3eltr4i 
 |-  R e. CVec