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 = {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	rngmneg1	$⊢ φ \to N (X) \underset{˙}{\cdot} 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 5	grprinvd	$⊢ φ \to X +_{R} N (X) = 0_{R}$
12	11	oveq1d	$⊢ φ \to (X +_{R} N (X)) \underset{˙}{\cdot} Y = 0_{R} \underset{˙}{\cdot} Y$
13	1 2 8	rnglz	$⊢ (R \in Rng \land Y \in B) \to 0_{R} \underset{˙}{\cdot} Y = 0_{R}$
14	4 6 13	syl2anc	$⊢ φ \to 0_{R} \underset{˙}{\cdot} Y = 0_{R}$
15	12 14	eqtrd	$⊢ φ \to (X +_{R} N (X)) \underset{˙}{\cdot} 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 5	grpinvcld	$⊢ φ \to N (X) \in B$
19	1 2	rngcl	$⊢ (R \in Rng \land N (X) \in B \land Y \in B) \to N (X) \underset{˙}{\cdot} Y \in B$
20	4 18 6 19	syl3anc	$⊢ φ \to N (X) \underset{˙}{\cdot} Y \in B$
21	1 7 8 3	grpinvid1	$⊢ (R \in Grp \land X \underset{˙}{\cdot} Y \in B \land N (X) \underset{˙}{\cdot} Y \in B) \to (N (X \underset{˙}{\cdot} Y) = N (X) \underset{˙}{\cdot} Y \leftrightarrow (X \underset{˙}{\cdot} Y) +_{R} (N (X) \underset{˙}{\cdot} Y) = 0_{R})$
22	10 17 20 21	syl3anc	$⊢ φ \to (N (X \underset{˙}{\cdot} Y) = N (X) \underset{˙}{\cdot} Y \leftrightarrow (X \underset{˙}{\cdot} Y) +_{R} (N (X) \underset{˙}{\cdot} Y) = 0_{R})$
23	1 7 2	rngdir	$⊢ (R \in Rng \land (X \in B \land N (X) \in B \land Y \in B)) \to (X +_{R} N (X)) \underset{˙}{\cdot} Y = (X \underset{˙}{\cdot} Y) +_{R} (N (X) \underset{˙}{\cdot} Y)$
24	23	eqcomd	$⊢ (R \in Rng \land (X \in B \land N (X) \in B \land Y \in B)) \to (X \underset{˙}{\cdot} Y) +_{R} (N (X) \underset{˙}{\cdot} Y) = (X +_{R} N (X)) \underset{˙}{\cdot} Y$
25	4 5 18 6 24	syl13anc	$⊢ φ \to (X \underset{˙}{\cdot} Y) +_{R} (N (X) \underset{˙}{\cdot} Y) = (X +_{R} N (X)) \underset{˙}{\cdot} Y$
26	25	eqeq1d	$⊢ φ \to ((X \underset{˙}{\cdot} Y) +_{R} (N (X) \underset{˙}{\cdot} Y) = 0_{R} \leftrightarrow (X +_{R} N (X)) \underset{˙}{\cdot} Y = 0_{R})$
27	22 26	bitrd	$⊢ φ \to (N (X \underset{˙}{\cdot} Y) = N (X) \underset{˙}{\cdot} Y \leftrightarrow (X +_{R} N (X)) \underset{˙}{\cdot} Y = 0_{R})$
28	15 27	mpbird	$⊢ φ \to N (X \underset{˙}{\cdot} Y) = N (X) \underset{˙}{\cdot} Y$
29	28	eqcomd	$⊢ φ \to N (X) \underset{˙}{\cdot} Y = N (X \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem rngmneg1

Proof