Theorem rngm2neg

Description: Double negation of a product in a non-unital ring ( mul2neg analog). (Contributed by Mario Carneiro, 4-Dec-2014) Generalization of ringm2neg . (Revised by AV, 17-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		rngneglmul.b	$$⊢B={\mathrm{Base}}_R$$
2		rngneglmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		rngneglmul.n	$$⊢N={inv}_g\left(R\right)$$
4		rngneglmul.r	$$⊢\phi \to R\in \mathrm{Rng}$$
5		rngneglmul.x	$$⊢\phi \to X\in B$$
6		rngneglmul.y	$$⊢\phi \to Y\in B$$
7		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
8	4 7	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
9	1 3 8 6	grpinvcld	$$⊢\phi \to N\left(Y\right)\in B$$
10	1 2 3 4 5 9	rngmneg1	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{·}N\left(Y\right)=N\left(X\underset{\dot{}}{·}N\left(Y\right)\right)$$
11	1 2 3 4 5 6	rngmneg2	$$⊢\phi \to X\underset{\dot{}}{·}N\left(Y\right)=N\left(X\underset{\dot{}}{·}Y\right)$$
12	11	fveq2d	$$⊢\phi \to N\left(X\underset{\dot{}}{·}N\left(Y\right)\right)=N\left(N\left(X\underset{\dot{}}{·}Y\right)\right)$$
13	1 2	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y\in B$$
14	4 5 6 13	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in B$$
15	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$$
16	8 14 15	syl2anc	$$⊢\phi \to N\left(N\left(X\underset{\dot{}}{·}Y\right)\right)=X\underset{\dot{}}{·}Y$$
17	10 12 16	3eqtrd	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{·}N\left(Y\right)=X\underset{\dot{}}{·}Y$$