Theorem rngmneg2

Description: Negation of a product in a non-unital ring ( mulneg2 analog). In contrast to ringmneg2 , the proof does not (and cannot) make use of the existence of a ring unity. (Contributed 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	rngmneg2	$$⊢\phi \to X\underset{\dot{}}{·}N\left(Y\right)=N\left(X\underset{\dot{}}{·}Y\right)$$

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		eqid	$$⊢{+}_R={+}_R$$
8		eqid	$$⊢0_R=0_R$$
9		rnggrp	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Grp}$$
10	4 9	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
11	1 7 8 3 10 6	grplinvd	$$⊢\phi \to N\left(Y\right){+}_{R}Y=0_R$$
12	11	oveq2d	$$⊢\phi \to X\underset{\dot{}}{·}\left(N\left(Y\right){+}_{R}Y\right)=X\underset{\dot{}}{·}{0}_R$$
13	1 2 8	rngrz	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\right)\to X\underset{\dot{}}{·}{0}_R=0_R$$
14	4 5 13	syl2anc	$$⊢\phi \to X\underset{\dot{}}{·}{0}_R=0_R$$
15	12 14	eqtrd	$$⊢\phi \to X\underset{\dot{}}{·}\left(N\left(Y\right){+}_{R}Y\right)=0_R$$
16	1 2	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y\in B$$
17	4 5 6 16	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in B$$
18	1 3 10 6	grpinvcld	$$⊢\phi \to N\left(Y\right)\in B$$
19	1 2	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge X\in B\wedge N\left(Y\right)\in B\right)\to X\underset{\dot{}}{·}N\left(Y\right)\in B$$
20	4 5 18 19	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}N\left(Y\right)\in B$$
21	1 7 8 3	grpinvid2	$$⊢\left(R\in \mathrm{Grp}\wedge X\underset{\dot{}}{·}Y\in B\wedge X\underset{\dot{}}{·}N\left(Y\right)\in B\right)\to \left(N\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{·}N\left(Y\right)\leftrightarrow \left(X\underset{\dot{}}{·}N\left(Y\right)\right){+}_R\left(X\underset{\dot{}}{·}Y\right)=0_R\right)$$
22	10 17 20 21	syl3anc	$$⊢\phi \to \left(N\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{·}N\left(Y\right)\leftrightarrow \left(X\underset{\dot{}}{·}N\left(Y\right)\right){+}_R\left(X\underset{\dot{}}{·}Y\right)=0_R\right)$$
23	1 7 2	rngdi	$$⊢\left(R\in \mathrm{Rng}\wedge \left(X\in B\wedge N\left(Y\right)\in B\wedge Y\in B\right)\right)\to X\underset{\dot{}}{·}\left(N\left(Y\right){+}_{R}Y\right)=\left(X\underset{\dot{}}{·}N\left(Y\right)\right){+}_R\left(X\underset{\dot{}}{·}Y\right)$$
24	23	eqcomd	$$⊢\left(R\in \mathrm{Rng}\wedge \left(X\in B\wedge N\left(Y\right)\in B\wedge Y\in B\right)\right)\to \left(X\underset{\dot{}}{·}N\left(Y\right)\right){+}_R\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{·}\left(N\left(Y\right){+}_{R}Y\right)$$
25	4 5 18 6 24	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{·}N\left(Y\right)\right){+}_R\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{·}\left(N\left(Y\right){+}_{R}Y\right)$$
26	25	eqeq1d	$$⊢\phi \to \left(\left(X\underset{\dot{}}{·}N\left(Y\right)\right){+}_R\left(X\underset{\dot{}}{·}Y\right)=0_R\leftrightarrow X\underset{\dot{}}{·}\left(N\left(Y\right){+}_{R}Y\right)=0_R\right)$$
27	22 26	bitrd	$$⊢\phi \to \left(N\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{·}N\left(Y\right)\leftrightarrow X\underset{\dot{}}{·}\left(N\left(Y\right){+}_{R}Y\right)=0_R\right)$$
28	15 27	mpbird	$$⊢\phi \to N\left(X\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{·}N\left(Y\right)$$
29	28	eqcomd	$$⊢\phi \to X\underset{\dot{}}{·}N\left(Y\right)=N\left(X\underset{\dot{}}{·}Y\right)$$