rngmneg2

Description: Negation of a product in a non-unital ring ( mulneg2 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 = {Base}_{R}$
	rngneglmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rngneglmul.n	$⊢ N = {inv}_{g} (R)$
	rngneglmul.r	$⊢ φ \to R \in Rng$
	rngneglmul.x	$⊢ φ \to X \in B$
	rngneglmul.y	$⊢ φ \to Y \in B$
Assertion	rngmneg2	$⊢ φ \to X \underset{˙}{\cdot} N (Y) = N (X \underset{˙}{\cdot} Y)$

Proof

Step	Hyp	Ref	Expression
1		rngneglmul.b	$⊢ B = {Base}_{R}$
2		rngneglmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		rngneglmul.n	$⊢ N = {inv}_{g} (R)$
4		rngneglmul.r	$⊢ φ \to R \in Rng$
5		rngneglmul.x	$⊢ φ \to X \in B$
6		rngneglmul.y	$⊢ φ \to Y \in B$
7		eqid	$⊢ +_{R} = +_{R}$
8		eqid	$⊢ 0_{R} = 0_{R}$
9		rnggrp	$⊢ R \in Rng \to R \in Grp$
10	4 9	syl	$⊢ φ \to R \in Grp$
11	1 7 8 3 10 6	grplinvd	$⊢ φ \to N (Y) +_{R} Y = 0_{R}$
12	11	oveq2d	$⊢ φ \to X \underset{˙}{\cdot} (N (Y) +_{R} Y) = X \underset{˙}{\cdot} 0_{R}$
13	1 2 8	rngrz	$⊢ (R \in Rng \land X \in B) \to X \underset{˙}{\cdot} 0_{R} = 0_{R}$
14	4 5 13	syl2anc	$⊢ φ \to X \underset{˙}{\cdot} 0_{R} = 0_{R}$
15	12 14	eqtrd	$⊢ φ \to X \underset{˙}{\cdot} (N (Y) +_{R} Y) = 0_{R}$
16	1 2	rngcl	$⊢ (R \in Rng \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
17	4 5 6 16	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$
18	1 3 10 6	grpinvcld	$⊢ φ \to N (Y) \in B$
19	1 2	rngcl	$⊢ (R \in Rng \land X \in B \land N (Y) \in B) \to X \underset{˙}{\cdot} N (Y) \in B$
20	4 5 18 19	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} N (Y) \in B$
21	1 7 8 3	grpinvid2	$⊢ (R \in Grp \land X \underset{˙}{\cdot} Y \in B \land X \underset{˙}{\cdot} N (Y) \in B) \to (N (X \underset{˙}{\cdot} Y) = X \underset{˙}{\cdot} N (Y) \leftrightarrow (X \underset{˙}{\cdot} N (Y)) +_{R} (X \underset{˙}{\cdot} Y) = 0_{R})$
22	10 17 20 21	syl3anc	$⊢ φ \to (N (X \underset{˙}{\cdot} Y) = X \underset{˙}{\cdot} N (Y) \leftrightarrow (X \underset{˙}{\cdot} N (Y)) +_{R} (X \underset{˙}{\cdot} Y) = 0_{R})$
23	1 7 2	rngdi	$⊢ (R \in Rng \land (X \in B \land N (Y) \in B \land Y \in B)) \to X \underset{˙}{\cdot} (N (Y) +_{R} Y) = (X \underset{˙}{\cdot} N (Y)) +_{R} (X \underset{˙}{\cdot} Y)$
24	23	eqcomd	$⊢ (R \in Rng \land (X \in B \land N (Y) \in B \land Y \in B)) \to (X \underset{˙}{\cdot} N (Y)) +_{R} (X \underset{˙}{\cdot} Y) = X \underset{˙}{\cdot} (N (Y) +_{R} Y)$
25	4 5 18 6 24	syl13anc	$⊢ φ \to (X \underset{˙}{\cdot} N (Y)) +_{R} (X \underset{˙}{\cdot} Y) = X \underset{˙}{\cdot} (N (Y) +_{R} Y)$
26	25	eqeq1d	$⊢ φ \to ((X \underset{˙}{\cdot} N (Y)) +_{R} (X \underset{˙}{\cdot} Y) = 0_{R} \leftrightarrow X \underset{˙}{\cdot} (N (Y) +_{R} Y) = 0_{R})$
27	22 26	bitrd	$⊢ φ \to (N (X \underset{˙}{\cdot} Y) = X \underset{˙}{\cdot} N (Y) \leftrightarrow X \underset{˙}{\cdot} (N (Y) +_{R} Y) = 0_{R})$
28	15 27	mpbird	$⊢ φ \to N (X \underset{˙}{\cdot} Y) = X \underset{˙}{\cdot} N (Y)$
29	28	eqcomd	$⊢ φ \to X \underset{˙}{\cdot} N (Y) = N (X \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem rngmneg2

Proof