Metamath Proof Explorer

Theorem clmsub

Description: Subtraction 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 clmsub 
|- ( ( W e. CMod /\ A e. K /\ B e. K ) -> ( A - B ) = ( A ( -g ` F ) B ) )

Proof

Step Hyp Ref Expression
1 clm0.f 
 |-  F = ( Scalar ` W )
2 clmsub.k 
 |-  K = ( Base ` F )
3 1 2 clmsubrg 
 |-  ( W e. CMod -> K e. ( SubRing ` CCfld ) )
4 subrgsubg 
 |-  ( K e. ( SubRing ` CCfld ) -> K e. ( SubGrp ` CCfld ) )
5 3 4 syl 
 |-  ( W e. CMod -> K e. ( SubGrp ` CCfld ) )
6 cnfldsub 
 |-  - = ( -g ` CCfld )
7 eqid 
 |-  ( CCfld |`s K ) = ( CCfld |`s K )
8 eqid 
 |-  ( -g ` ( CCfld |`s K ) ) = ( -g ` ( CCfld |`s K ) )
9 6 7 8 subgsub 
 |-  ( ( K e. ( SubGrp ` CCfld ) /\ A e. K /\ B e. K ) -> ( A - B ) = ( A ( -g ` ( CCfld |`s K ) ) B ) )
10 5 9 syl3an1 
 |-  ( ( W e. CMod /\ A e. K /\ B e. K ) -> ( A - B ) = ( A ( -g ` ( CCfld |`s K ) ) B ) )
11 1 2 clmsca 
 |-  ( W e. CMod -> F = ( CCfld |`s K ) )
12 11 fveq2d 
 |-  ( W e. CMod -> ( -g ` F ) = ( -g ` ( CCfld |`s K ) ) )
13 12 3ad2ant1 
 |-  ( ( W e. CMod /\ A e. K /\ B e. K ) -> ( -g ` F ) = ( -g ` ( CCfld |`s K ) ) )
14 13 oveqd 
 |-  ( ( W e. CMod /\ A e. K /\ B e. K ) -> ( A ( -g ` F ) B ) = ( A ( -g ` ( CCfld |`s K ) ) B ) )
15 10 14 eqtr4d 
 |-  ( ( W e. CMod /\ A e. K /\ B e. K ) -> ( A - B ) = ( A ( -g ` F ) B ) )