Metamath Proof Explorer

Theorem clmabs

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

Ref Expression
Hypotheses clm0.f 
|- F = ( Scalar ` W )
clmsub.k 
|- K = ( Base ` F )
Assertion clmabs 
|- ( ( W e. CMod /\ A e. K ) -> ( abs ` A ) = ( ( norm ` F ) ` A ) )

Proof

Step Hyp Ref Expression
1 clm0.f 
 |-  F = ( Scalar ` W )
2 clmsub.k 
 |-  K = ( Base ` F )
3 1 2 clmsca 
 |-  ( W e. CMod -> F = ( CCfld |`s K ) )
4 3 fveq2d 
 |-  ( W e. CMod -> ( norm ` F ) = ( norm ` ( CCfld |`s K ) ) )
5 4 adantr 
 |-  ( ( W e. CMod /\ A e. K ) -> ( norm ` F ) = ( norm ` ( CCfld |`s K ) ) )
6 5 fveq1d 
 |-  ( ( W e. CMod /\ A e. K ) -> ( ( norm ` F ) ` A ) = ( ( norm ` ( CCfld |`s K ) ) ` A ) )
7 1 2 clmsubrg 
 |-  ( W e. CMod -> K e. ( SubRing ` CCfld ) )
8 subrgsubg 
 |-  ( K e. ( SubRing ` CCfld ) -> K e. ( SubGrp ` CCfld ) )
9 7 8 syl 
 |-  ( W e. CMod -> K e. ( SubGrp ` CCfld ) )
10 eqid 
 |-  ( CCfld |`s K ) = ( CCfld |`s K )
11 cnfldnm 
 |-  abs = ( norm ` CCfld )
12 eqid 
 |-  ( norm ` ( CCfld |`s K ) ) = ( norm ` ( CCfld |`s K ) )
13 10 11 12 subgnm2 
 |-  ( ( K e. ( SubGrp ` CCfld ) /\ A e. K ) -> ( ( norm ` ( CCfld |`s K ) ) ` A ) = ( abs ` A ) )
14 9 13 sylan 
 |-  ( ( W e. CMod /\ A e. K ) -> ( ( norm ` ( CCfld |`s K ) ) ` A ) = ( abs ` A ) )
15 6 14 eqtr2d 
 |-  ( ( W e. CMod /\ A e. K ) -> ( abs ` A ) = ( ( norm ` F ) ` A ) )