This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {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	rngm2neg	$⊢ φ \to N (X) \underset{˙}{\cdot} N (Y) = 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		rnggrp	$⊢ R \in Rng \to R \in Grp$
8	4 7	syl	$⊢ φ \to R \in Grp$
9	1 3 8 6	grpinvcld	$⊢ φ \to N (Y) \in B$
10	1 2 3 4 5 9	rngmneg1	$⊢ φ \to N (X) \underset{˙}{\cdot} N (Y) = N (X \underset{˙}{\cdot} N (Y))$
11	1 2 3 4 5 6	rngmneg2	$⊢ φ \to X \underset{˙}{\cdot} N (Y) = N (X \underset{˙}{\cdot} Y)$
12	11	fveq2d	$⊢ φ \to N (X \underset{˙}{\cdot} N (Y)) = N (N (X \underset{˙}{\cdot} Y))$
13	1 2	rngcl	$⊢ (R \in Rng \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
14	4 5 6 13	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$
15	1 3	grpinvinv	$⊢ (R \in Grp \land X \underset{˙}{\cdot} Y \in B) \to N (N (X \underset{˙}{\cdot} Y)) = X \underset{˙}{\cdot} Y$
16	8 14 15	syl2anc	$⊢ φ \to N (N (X \underset{˙}{\cdot} Y)) = X \underset{˙}{\cdot} Y$
17	10 12 16	3eqtrd	$⊢ φ \to N (X) \underset{˙}{\cdot} N (Y) = X \underset{˙}{\cdot} Y$