This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clmneg

Description: Negation 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 clmneg 
|- ( ( W e. CMod /\ A e. K ) -> -u A = ( ( invg ` 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 -> ( invg ` F ) = ( invg ` ( CCfld |`s K ) ) )
5 4 adantr 
 |-  ( ( W e. CMod /\ A e. K ) -> ( invg ` F ) = ( invg ` ( CCfld |`s K ) ) )
6 5 fveq1d 
 |-  ( ( W e. CMod /\ A e. K ) -> ( ( invg ` F ) ` A ) = ( ( invg ` ( 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 eqid 
 |-  ( invg ` CCfld ) = ( invg ` CCfld )
12 eqid 
 |-  ( invg ` ( CCfld |`s K ) ) = ( invg ` ( CCfld |`s K ) )
13 10 11 12 subginv 
 |-  ( ( K e. ( SubGrp ` CCfld ) /\ A e. K ) -> ( ( invg ` CCfld ) ` A ) = ( ( invg ` ( CCfld |`s K ) ) ` A ) )
14 9 13 sylan 
 |-  ( ( W e. CMod /\ A e. K ) -> ( ( invg ` CCfld ) ` A ) = ( ( invg ` ( CCfld |`s K ) ) ` A ) )
15 1 2 clmsscn 
 |-  ( W e. CMod -> K C_ CC )
16 15 sselda 
 |-  ( ( W e. CMod /\ A e. K ) -> A e. CC )
17 cnfldneg 
 |-  ( A e. CC -> ( ( invg ` CCfld ) ` A ) = -u A )
18 16 17 syl 
 |-  ( ( W e. CMod /\ A e. K ) -> ( ( invg ` CCfld ) ` A ) = -u A )
19 6 14 18 3eqtr2rd 
 |-  ( ( W e. CMod /\ A e. K ) -> -u A = ( ( invg ` F ) ` A ) )