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 = {inv}_{g} (R)$
	asclinvg.j	$⊢ J = {inv}_{g} (W)$
Assertion	asclinvg	$⊢ (W \in LMod \land W \in Ring \land C \in B) \to J (A (C)) = A (I (C))$

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 = {inv}_{g} (R)$
5		asclinvg.j	$⊢ J = {inv}_{g} (W)$
6		simp2	$⊢ (W \in LMod \land W \in Ring \land C \in B) \to W \in Ring$
7		simp1	$⊢ (W \in LMod \land W \in Ring \land C \in B) \to W \in LMod$
8	1 2 6 7	asclghm	$⊢ (W \in LMod \land W \in Ring \land C \in B) \to A \in (R GrpHom W)$
9		simp3	$⊢ (W \in LMod \land W \in Ring \land C \in B) \to C \in B$
10	3 4 5	ghminv	$⊢ (A \in (R GrpHom W) \land C \in B) \to A (I (C)) = J (A (C))$
11	10	eqcomd	$⊢ (A \in (R GrpHom W) \land C \in B) \to J (A (C)) = A (I (C))$
12	8 9 11	syl2anc	$⊢ (W \in LMod \land W \in Ring \land C \in B) \to J (A (C)) = A (I (C))$

Metamath Proof Explorer