Theorem m2detleiblem7

Description: Lemma 7 for m2detleib . (Contributed by AV, 20-Dec-2018)

	Ref	Expression
Hypotheses	m2detleiblem1.n	$$⊢N=\left\{1,2\right\}$$
	m2detleiblem1.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
	m2detleiblem1.y	$$⊢Y=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	m2detleiblem1.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
	m2detleiblem1.o	$$⊢\underset{\dot{}}{1}=1_R$$
	m2detleiblem1.i	$$⊢I={inv}_g\left(R\right)$$
	m2detleiblem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	m2detleiblem1.m	$$⊢\underset{\dot{}}{-}={-}_R$$
Assertion	m2detleiblem7	$$⊢\left(R\in \mathrm{Ring}\wedge X\in {\mathrm{Base}}_R\wedge Z\in {\mathrm{Base}}_R\right)\to X{+}_R\left(I\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}Z\right)=X\underset{\dot{}}{-}Z$$

Proof

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