Metamath Proof Explorer

Theorem bj-rveccmod

Description: Real vector spaces are subcomplex modules (elemental version). (Contributed by BJ, 6-Jan-2024)

Ref Expression
Assertion bj-rveccmod 
|- ( V e. RRVec -> V e. CMod )

Proof

Step Hyp Ref Expression
1 bj-rvecmod 
 |-  ( V e. RRVec -> V e. LMod )
2 df-refld 
 |-  RRfld = ( CCfld |`s RR )
3 2 a1i 
 |-  ( V e. RRVec -> RRfld = ( CCfld |`s RR ) )
4 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
5 4 simpli 
 |-  RR e. ( SubRing ` CCfld )
6 5 a1i 
 |-  ( V e. RRVec -> RR e. ( SubRing ` CCfld ) )
7 bj-rvecrr 
 |-  ( V e. RRVec -> ( Scalar ` V ) = RRfld )
8 7 eqcomd 
 |-  ( V e. RRVec -> RRfld = ( Scalar ` V ) )
9 rebase 
 |-  RR = ( Base ` RRfld )
10 9 a1i 
 |-  ( V e. RRVec -> RR = ( Base ` RRfld ) )
11 8 10 bj-isclm 
 |-  ( V e. RRVec -> ( V e. CMod <-> ( V e. LMod /\ RRfld = ( CCfld |`s RR ) /\ RR e. ( SubRing ` CCfld ) ) ) )
12 1 3 6 11 mpbir3and 
 |-  ( V e. RRVec -> V e. CMod )