Metamath Proof Explorer

Theorem isclmi

Description: Reverse direction of isclm . (Contributed by Mario Carneiro, 30-Oct-2015)

Ref Expression
Hypothesis clm0.f 
|- F = ( Scalar ` W )
Assertion isclmi 
|- ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> W e. CMod )

Proof

Step Hyp Ref Expression
1 clm0.f 
 |-  F = ( Scalar ` W )
2 simp1 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> W e. LMod )
3 simp2 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> F = ( CCfld |`s K ) )
4 eqid 
 |-  ( CCfld |`s K ) = ( CCfld |`s K )
5 4 subrgbas 
 |-  ( K e. ( SubRing ` CCfld ) -> K = ( Base ` ( CCfld |`s K ) ) )
6 5 3ad2ant3 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> K = ( Base ` ( CCfld |`s K ) ) )
7 3 fveq2d 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( Base ` F ) = ( Base ` ( CCfld |`s K ) ) )
8 6 7 eqtr4d 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> K = ( Base ` F ) )
9 8 oveq2d 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( CCfld |`s K ) = ( CCfld |`s ( Base ` F ) ) )
10 3 9 eqtrd 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> F = ( CCfld |`s ( Base ` F ) ) )
11 simp3 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> K e. ( SubRing ` CCfld ) )
12 8 11 eqeltrrd 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( Base ` F ) e. ( SubRing ` CCfld ) )
13 eqid 
 |-  ( Base ` F ) = ( Base ` F )
14 1 13 isclm 
 |-  ( W e. CMod <-> ( W e. LMod /\ F = ( CCfld |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` CCfld ) ) )
15 2 10 12 14 syl3anbrc 
 |-  ( ( W e. LMod /\ F = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> W e. CMod )