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 ) ) )