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	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	asclinvg.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	asclinvg.k	⊢ 𝐵 = ( Base ‘ 𝑅 )
	asclinvg.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
	asclinvg.j	⊢ 𝐽 = ( invg ‘ 𝑊 )
Assertion	asclinvg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → ( 𝐽 ‘ ( 𝐴 ‘ 𝐶 ) ) = ( 𝐴 ‘ ( 𝐼 ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		asclinvg.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		asclinvg.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		asclinvg.k	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		asclinvg.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
5		asclinvg.j	⊢ 𝐽 = ( invg ‘ 𝑊 )
6		simp2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → 𝑊 ∈ Ring )
7		simp1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → 𝑊 ∈ LMod )
8	1 2 6 7	asclghm	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → 𝐴 ∈ ( 𝑅 GrpHom 𝑊 ) )
9		simp3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
10	3 4 5	ghminv	⊢ ( ( 𝐴 ∈ ( 𝑅 GrpHom 𝑊 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐴 ‘ ( 𝐼 ‘ 𝐶 ) ) = ( 𝐽 ‘ ( 𝐴 ‘ 𝐶 ) ) )
11	10	eqcomd	⊢ ( ( 𝐴 ∈ ( 𝑅 GrpHom 𝑊 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐽 ‘ ( 𝐴 ‘ 𝐶 ) ) = ( 𝐴 ‘ ( 𝐼 ‘ 𝐶 ) ) )
12	8 9 11	syl2anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → ( 𝐽 ‘ ( 𝐴 ‘ 𝐶 ) ) = ( 𝐴 ‘ ( 𝐼 ‘ 𝐶 ) ) )