Metamath Proof Explorer

Theorem isclm

Description: A subcomplex module is a left module over a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses isclm.f 
|- F = ( Scalar ` W )
isclm.k 
|- K = ( Base ` F )
Assertion isclm 
|- ( W e. CMod <-> ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) )

Proof

Step Hyp Ref Expression
1 isclm.f 
 |-  F = ( Scalar ` W )
2 isclm.k 
 |-  K = ( Base ` F )
3 fvexd 
 |-  ( w = W -> ( Scalar ` w ) e. _V )
4 fvexd 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( Base ` f ) e. _V )
5 id 
 |-  ( f = ( Scalar ` w ) -> f = ( Scalar ` w ) )
6 fveq2 
 |-  ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) )
7 6 1 eqtr4di 
 |-  ( w = W -> ( Scalar ` w ) = F )
8 5 7 sylan9eqr 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> f = F )
9 8 adantr 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> f = F )
10 id 
 |-  ( k = ( Base ` f ) -> k = ( Base ` f ) )
11 8 fveq2d 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( Base ` f ) = ( Base ` F ) )
12 11 2 eqtr4di 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( Base ` f ) = K )
13 10 12 sylan9eqr 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> k = K )
14 13 oveq2d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( CCfld |`s k ) = ( CCfld |`s K ) )
15 9 14 eqeq12d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( f = ( CCfld |`s k ) <-> F = ( CCfld |`s K ) ) )
16 13 eleq1d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( k e. ( SubRing ` CCfld ) <-> K e. ( SubRing ` CCfld ) ) )
17 15 16 anbi12d 
 |-  ( ( ( w = W /\ f = ( Scalar ` w ) ) /\ k = ( Base ` f ) ) -> ( ( f = ( CCfld |`s k ) /\ k e. ( SubRing ` CCfld ) ) <-> ( F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )
18 4 17 sbcied 
 |-  ( ( w = W /\ f = ( Scalar ` w ) ) -> ( [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ k e. ( SubRing ` CCfld ) ) <-> ( F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )
19 3 18 sbcied 
 |-  ( w = W -> ( [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ k e. ( SubRing ` CCfld ) ) <-> ( F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )
20 df-clm 
 |-  CMod = { w e. LMod | [. ( Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = ( CCfld |`s k ) /\ k e. ( SubRing ` CCfld ) ) }
21 19 20 elrab2 
 |-  ( W e. CMod <-> ( W e. LMod /\ ( F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )
22 3anass 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) <-> ( W e. LMod /\ ( F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )
23 21 22 bitr4i 
 |-  ( W e. CMod <-> ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) )