Metamath Proof Explorer

Theorem qcvs

Description: The field of rational 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 qcvs.q 
|- Q = ( ringLMod ` ( CCfld |`s QQ ) )
Assertion qcvs 
|- Q e. CVec

Proof

Step Hyp Ref Expression
1 qcvs.q 
 |-  Q = ( ringLMod ` ( CCfld |`s QQ ) )
2 qsubdrg 
 |-  ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing )
3 drngring 
 |-  ( ( CCfld |`s QQ ) e. DivRing -> ( CCfld |`s QQ ) e. Ring )
4 3 adantl 
 |-  ( ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) -> ( CCfld |`s QQ ) e. Ring )
5 2 4 ax-mp 
 |-  ( CCfld |`s QQ ) e. Ring
6 rlmlmod 
 |-  ( ( CCfld |`s QQ ) e. Ring -> ( ringLMod ` ( CCfld |`s QQ ) ) e. LMod )
7 5 6 ax-mp 
 |-  ( ringLMod ` ( CCfld |`s QQ ) ) e. LMod
8 2 simpri 
 |-  ( CCfld |`s QQ ) e. DivRing
9 rlmsca 
 |-  ( ( CCfld |`s QQ ) e. DivRing -> ( CCfld |`s QQ ) = ( Scalar ` ( ringLMod ` ( CCfld |`s QQ ) ) ) )
10 9 eqcomd 
 |-  ( ( CCfld |`s QQ ) e. DivRing -> ( Scalar ` ( ringLMod ` ( CCfld |`s QQ ) ) ) = ( CCfld |`s QQ ) )
11 8 10 ax-mp 
 |-  ( Scalar ` ( ringLMod ` ( CCfld |`s QQ ) ) ) = ( CCfld |`s QQ )
12 2 simpli 
 |-  QQ e. ( SubRing ` CCfld )
13 eqid 
 |-  ( Scalar ` ( ringLMod ` ( CCfld |`s QQ ) ) ) = ( Scalar ` ( ringLMod ` ( CCfld |`s QQ ) ) )
14 13 isclmi 
 |-  ( ( ( ringLMod ` ( CCfld |`s QQ ) ) e. LMod /\ ( Scalar ` ( ringLMod ` ( CCfld |`s QQ ) ) ) = ( CCfld |`s QQ ) /\ QQ e. ( SubRing ` CCfld ) ) -> ( ringLMod ` ( CCfld |`s QQ ) ) e. CMod )
15 7 11 12 14 mp3an 
 |-  ( ringLMod ` ( CCfld |`s QQ ) ) e. CMod
16 rlmlvec 
 |-  ( ( CCfld |`s QQ ) e. DivRing -> ( ringLMod ` ( CCfld |`s QQ ) ) e. LVec )
17 8 16 ax-mp 
 |-  ( ringLMod ` ( CCfld |`s QQ ) ) e. LVec
18 15 17 elini 
 |-  ( ringLMod ` ( CCfld |`s QQ ) ) e. ( CMod i^i LVec )
19 df-cvs 
 |-  CVec = ( CMod i^i LVec )
20 18 1 19 3eltr4i 
 |-  Q e. CVec