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

Metamath Proof Explorer

Theorem asclinvg

Description: The group inverse (negation) of a lifted scalar is the lifted negation of the scalar. (Contributed by AV, 2-Sep-2019)

Ref Expression
Hypotheses asclinvg.a 
|- A = ( algSc ` W )
asclinvg.r 
|- R = ( Scalar ` W )
asclinvg.k 
|- B = ( Base ` R )
asclinvg.i 
|- I = ( invg ` R )
asclinvg.j 
|- J = ( invg ` W )
Assertion asclinvg 
|- ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> ( J ` ( A ` C ) ) = ( A ` ( I ` C ) ) )

Proof

Step Hyp Ref Expression
1 asclinvg.a 
 |-  A = ( algSc ` W )
2 asclinvg.r 
 |-  R = ( Scalar ` W )
3 asclinvg.k 
 |-  B = ( Base ` R )
4 asclinvg.i 
 |-  I = ( invg ` R )
5 asclinvg.j 
 |-  J = ( invg ` W )
6 simp2 
 |-  ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> W e. Ring )
7 simp1 
 |-  ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> W e. LMod )
8 1 2 6 7 asclghm 
 |-  ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> A e. ( R GrpHom W ) )
9 simp3 
 |-  ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> C e. B )
10 3 4 5 ghminv 
 |-  ( ( A e. ( R GrpHom W ) /\ C e. B ) -> ( A ` ( I ` C ) ) = ( J ` ( A ` C ) ) )
11 10 eqcomd 
 |-  ( ( A e. ( R GrpHom W ) /\ C e. B ) -> ( J ` ( A ` C ) ) = ( A ` ( I ` C ) ) )
12 8 9 11 syl2anc 
 |-  ( ( W e. LMod /\ W e. Ring /\ C e. B ) -> ( J ` ( A ` C ) ) = ( A ` ( I ` C ) ) )