Theorem rngmneg1

Description: Negation of a product in a non-unital ring ( mulneg1 analog). In contrast to ringmneg1 , 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	rngmneg1	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{·}Y=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 5	grprinvd	$$⊢\phi \to X{+}_{R}N\left(X\right)=0_R$$
12	11	oveq1d	$$⊢\phi \to \left(X{+}_{R}N\left(X\right)\right)\underset{\dot{}}{·}Y=0_R\underset{\dot{}}{·}Y$$
13	1 2 8	rnglz	$$⊢\left(R\in \mathrm{Rng}\wedge Y\in B\right)\to 0_R\underset{\dot{}}{·}Y=0_R$$
14	4 6 13	syl2anc	$$⊢\phi \to 0_R\underset{\dot{}}{·}Y=0_R$$
15	12 14	eqtrd	$$⊢\phi \to \left(X{+}_{R}N\left(X\right)\right)\underset{\dot{}}{·}Y=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 5	grpinvcld	$$⊢\phi \to N\left(X\right)\in B$$
19	1 2	rngcl	$$⊢\left(R\in \mathrm{Rng}\wedge N\left(X\right)\in B\wedge Y\in B\right)\to N\left(X\right)\underset{\dot{}}{·}Y\in B$$
20	4 18 6 19	syl3anc	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{·}Y\in B$$
21	1 7 8 3	grpinvid1	$$⊢\left(R\in \mathrm{Grp}\wedge X\underset{\dot{}}{·}Y\in B\wedge N\left(X\right)\underset{\dot{}}{·}Y\in B\right)\to \left(N\left(X\underset{\dot{}}{·}Y\right)=N\left(X\right)\underset{\dot{}}{·}Y\leftrightarrow \left(X\underset{\dot{}}{·}Y\right){+}_R\left(N\left(X\right)\underset{\dot{}}{·}Y\right)=0_R\right)$$
22	10 17 20 21	syl3anc	$$⊢\phi \to \left(N\left(X\underset{\dot{}}{·}Y\right)=N\left(X\right)\underset{\dot{}}{·}Y\leftrightarrow \left(X\underset{\dot{}}{·}Y\right){+}_R\left(N\left(X\right)\underset{\dot{}}{·}Y\right)=0_R\right)$$
23	1 7 2	rngdir	$$⊢\left(R\in \mathrm{Rng}\wedge \left(X\in B\wedge N\left(X\right)\in B\wedge Y\in B\right)\right)\to \left(X{+}_{R}N\left(X\right)\right)\underset{\dot{}}{·}Y=\left(X\underset{\dot{}}{·}Y\right){+}_R\left(N\left(X\right)\underset{\dot{}}{·}Y\right)$$
24	23	eqcomd	$$⊢\left(R\in \mathrm{Rng}\wedge \left(X\in B\wedge N\left(X\right)\in B\wedge Y\in B\right)\right)\to \left(X\underset{\dot{}}{·}Y\right){+}_R\left(N\left(X\right)\underset{\dot{}}{·}Y\right)=\left(X{+}_{R}N\left(X\right)\right)\underset{\dot{}}{·}Y$$
25	4 5 18 6 24	syl13anc	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y\right){+}_R\left(N\left(X\right)\underset{\dot{}}{·}Y\right)=\left(X{+}_{R}N\left(X\right)\right)\underset{\dot{}}{·}Y$$
26	25	eqeq1d	$$⊢\phi \to \left(\left(X\underset{\dot{}}{·}Y\right){+}_R\left(N\left(X\right)\underset{\dot{}}{·}Y\right)=0_R\leftrightarrow \left(X{+}_{R}N\left(X\right)\right)\underset{\dot{}}{·}Y=0_R\right)$$
27	22 26	bitrd	$$⊢\phi \to \left(N\left(X\underset{\dot{}}{·}Y\right)=N\left(X\right)\underset{\dot{}}{·}Y\leftrightarrow \left(X{+}_{R}N\left(X\right)\right)\underset{\dot{}}{·}Y=0_R\right)$$
28	15 27	mpbird	$$⊢\phi \to N\left(X\underset{\dot{}}{·}Y\right)=N\left(X\right)\underset{\dot{}}{·}Y$$
29	28	eqcomd	$$⊢\phi \to N\left(X\right)\underset{\dot{}}{·}Y=N\left(X\underset{\dot{}}{·}Y\right)$$