Theorem ringm2neg

Description: Double negation of a product in a ring. ( mul2neg analog.) (Contributed by Mario Carneiro, 4-Dec-2014) (Proof shortened by AV, 30-Mar-2025)

	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		ringrng	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Rng}$$
8	4 7	syl	$$⊢\phi \to R\in \mathrm{Rng}$$
9	1 2 3 8 5 6	rngm2neg	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{·}N\left(Y\right)=X\underset{\dot{}}{·}Y$$