ringm2neg

Description: Double negation of a product in a ring. ( mul2neg analog.) (Contributed by Mario Carneiro, 4-Dec-2014)

	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$

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		ringgrp	$⊢ R \in Ring \to R \in Grp$
8	4 7	syl	$⊢ φ \to R \in Grp$
9	1 3	grpinvcl	$⊢ (R \in Grp \land Y \in B) \to N (Y) \in B$
10	8 6 9	syl2anc	$⊢ φ \to N (Y) \in B$
11	1 2 3 4 5 10	ringmneg1	$⊢ φ \to N (X) \underset{˙}{\cdot} N (Y) = N (X \underset{˙}{\cdot} N (Y))$
12	1 2 3 4 5 6	ringmneg2	$⊢ φ \to X \underset{˙}{\cdot} N (Y) = N (X \underset{˙}{\cdot} Y)$
13	12	fveq2d	$⊢ φ \to N (X \underset{˙}{\cdot} N (Y)) = N (N (X \underset{˙}{\cdot} Y))$
14	1 2	ringcl	$⊢ (R \in Ring \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
15	4 5 6 14	syl3anc	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$
16	1 3	grpinvinv	$⊢ (R \in Grp \land X \underset{˙}{\cdot} Y \in B) \to N (N (X \underset{˙}{\cdot} Y)) = X \underset{˙}{\cdot} Y$
17	8 15 16	syl2anc	$⊢ φ \to N (N (X \underset{˙}{\cdot} Y)) = X \underset{˙}{\cdot} Y$
18	11 13 17	3eqtrd	$⊢ φ \to N (X) \underset{˙}{\cdot} N (Y) = X \underset{˙}{\cdot} Y$

Metamath Proof Explorer