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

Metamath Proof Explorer

Theorem ringm2neg

Description: Double negation of a product in a ring. ( mul2neg analog.) (Contributed by Mario Carneiro, 4-Dec-2014) (Proof shortened by AV, 30-Mar-2025)

	Ref	Expression
Hypotheses	ringneglmul.b	$⊢ B = {Base}_{R}$
	ringneglmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ringneglmul.n	$⊢ N = {inv}_{g} (R)$
	ringneglmul.r	$⊢ φ \to R \in Ring$
	ringneglmul.x	$⊢ φ \to X \in B$
	ringneglmul.y	$⊢ φ \to Y \in B$
Assertion	ringm2neg	$⊢ φ \to N (X) \underset{˙}{\cdot} N (Y) = X \underset{˙}{\cdot} Y$

Proof

Step	Hyp	Ref	Expression
1		ringneglmul.b	$⊢ B = {Base}_{R}$
2		ringneglmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		ringneglmul.n	$⊢ N = {inv}_{g} (R)$
4		ringneglmul.r	$⊢ φ \to R \in Ring$
5		ringneglmul.x	$⊢ φ \to X \in B$
6		ringneglmul.y	$⊢ φ \to Y \in B$
7		ringrng	$⊢ R \in Ring \to R \in Rng$
8	4 7	syl	$⊢ φ \to R \in Rng$
9	1 2 3 8 5 6	rngm2neg	$⊢ φ \to N (X) \underset{˙}{\cdot} N (Y) = X \underset{˙}{\cdot} Y$