Theorem ringm2neg

Description: Double negation of a product in a ring. ( mul2neg analog.) (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	ringneglmul.b	$$⊢B={\mathrm{Base}}_R$$
	ringneglmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	ringneglmul.n	$$⊢N={inv}_g\left(R\right)$$
	ringneglmul.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	ringneglmul.x	$$⊢\phi \to X\in B$$
	ringneglmul.y	$$⊢\phi \to Y\in B$$
Assertion	ringm2neg	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{·}N\left(Y\right)=X\underset{\dot{}}{·}Y$$

Proof

Step	Hyp	Ref	Expression
1		ringneglmul.b	$$⊢B={\mathrm{Base}}_R$$
2		ringneglmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		ringneglmul.n	$$⊢N={inv}_g\left(R\right)$$
4		ringneglmul.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		ringneglmul.x	$$⊢\phi \to X\in B$$
6		ringneglmul.y	$$⊢\phi \to Y\in B$$
7		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
8	4 7	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
9	1 3	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge Y\in B\right)\to N\left(Y\right)\in B$$
10	8 6 9	syl2anc	$$⊢\phi \to N\left(Y\right)\in B$$
11	1 2 3 4 5 10	ringmneg1	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{·}N\left(Y\right)=N\left(X\underset{\dot{}}{·}N\left(Y\right)\right)$$
12	1 2 3 4 5 6	ringmneg2	$$⊢\phi \to X\underset{\dot{}}{·}N\left(Y\right)=N\left(X\underset{\dot{}}{·}Y\right)$$
13	12	fveq2d	$$⊢\phi \to N\left(X\underset{\dot{}}{·}N\left(Y\right)\right)=N\left(N\left(X\underset{\dot{}}{·}Y\right)\right)$$
14	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y\in B$$
15	4 5 6 14	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in B$$
16	1 3	grpinvinv	$$⊢\left(R\in \mathrm{Grp}\wedge X\underset{\dot{}}{·}Y\in B\right)\to N\left(N\left(X\underset{\dot{}}{·}Y\right)\right)=X\underset{\dot{}}{·}Y$$
17	8 15 16	syl2anc	$$⊢\phi \to N\left(N\left(X\underset{\dot{}}{·}Y\right)\right)=X\underset{\dot{}}{·}Y$$
18	11 13 17	3eqtrd	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{·}N\left(Y\right)=X\underset{\dot{}}{·}Y$$