m2detleiblem7

	Ref	Expression
Hypotheses	m2detleiblem1.n	$⊢ N = \{1, 2\}$
	m2detleiblem1.p	$⊢ P = {Base}_{SymGrp (N)}$
	m2detleiblem1.y	$⊢ Y = ℤRHom (R)$
	m2detleiblem1.s	$⊢ S = pmSgn (N)$
	m2detleiblem1.o	$⊢ \underset{˙}{1} = 1_{R}$
	m2detleiblem1.i	$⊢ I = {inv}_{g} (R)$
	m2detleiblem1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	m2detleiblem1.m	$⊢ \underset{˙}{-} = -_{R}$
Assertion	m2detleiblem7	$⊢ (R \in Ring \land X \in {Base}_{R} \land Z \in {Base}_{R}) \to X +_{R} (I (\underset{˙}{1}) \underset{˙}{\cdot} Z) = X \underset{˙}{-} Z$

Step	Hyp	Ref	Expression
1		m2detleiblem1.n	$⊢ N = \{1, 2\}$
2		m2detleiblem1.p	$⊢ P = {Base}_{SymGrp (N)}$
3		m2detleiblem1.y	$⊢ Y = ℤRHom (R)$
4		m2detleiblem1.s	$⊢ S = pmSgn (N)$
5		m2detleiblem1.o	$⊢ \underset{˙}{1} = 1_{R}$
6		m2detleiblem1.i	$⊢ I = {inv}_{g} (R)$
7		m2detleiblem1.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		m2detleiblem1.m	$⊢ \underset{˙}{-} = -_{R}$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10		simpl	$⊢ (R \in Ring \land Z \in {Base}_{R}) \to R \in Ring$
11		simpr	$⊢ (R \in Ring \land Z \in {Base}_{R}) \to Z \in {Base}_{R}$
12	9 7 5 6 10 11	ringnegl	$⊢ (R \in Ring \land Z \in {Base}_{R}) \to I (\underset{˙}{1}) \underset{˙}{\cdot} Z = I (Z)$
13	12	3adant2	$⊢ (R \in Ring \land X \in {Base}_{R} \land Z \in {Base}_{R}) \to I (\underset{˙}{1}) \underset{˙}{\cdot} Z = I (Z)$
14	13	oveq2d	$⊢ (R \in Ring \land X \in {Base}_{R} \land Z \in {Base}_{R}) \to X +_{R} (I (\underset{˙}{1}) \underset{˙}{\cdot} Z) = X +_{R} I (Z)$
15		eqid	$⊢ +_{R} = +_{R}$
16	9 15 6 8	grpsubval	$⊢ (X \in {Base}_{R} \land Z \in {Base}_{R}) \to X \underset{˙}{-} Z = X +_{R} I (Z)$
17	16	3adant1	$⊢ (R \in Ring \land X \in {Base}_{R} \land Z \in {Base}_{R}) \to X \underset{˙}{-} Z = X +_{R} I (Z)$
18	14 17	eqtr4d	$⊢ (R \in Ring \land X \in {Base}_{R} \land Z \in {Base}_{R}) \to X +_{R} (I (\underset{˙}{1}) \underset{˙}{\cdot} Z) = X \underset{˙}{-} Z$

Metamath Proof Explorer