Metamath Proof Explorer

Theorem clm1

Description: The identity of the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypothesis clm0.f 
|- F = ( Scalar ` W )
Assertion clm1 
|- ( W e. CMod -> 1 = ( 1r ` F ) )

Proof

Step Hyp Ref Expression
1 clm0.f 
 |-  F = ( Scalar ` W )
2 eqid 
 |-  ( Base ` F ) = ( Base ` F )
3 1 2 clmsubrg 
 |-  ( W e. CMod -> ( Base ` F ) e. ( SubRing ` CCfld ) )
4 eqid 
 |-  ( CCfld |`s ( Base ` F ) ) = ( CCfld |`s ( Base ` F ) )
5 cnfld1 
 |-  1 = ( 1r ` CCfld )
6 4 5 subrg1 
 |-  ( ( Base ` F ) e. ( SubRing ` CCfld ) -> 1 = ( 1r ` ( CCfld |`s ( Base ` F ) ) ) )
7 3 6 syl 
 |-  ( W e. CMod -> 1 = ( 1r ` ( CCfld |`s ( Base ` F ) ) ) )
8 1 2 clmsca 
 |-  ( W e. CMod -> F = ( CCfld |`s ( Base ` F ) ) )
9 8 fveq2d 
 |-  ( W e. CMod -> ( 1r ` F ) = ( 1r ` ( CCfld |`s ( Base ` F ) ) ) )
10 7 9 eqtr4d 
 |-  ( W e. CMod -> 1 = ( 1r ` F ) )