dvdsrneg

Description: An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	dvdsr.1	$⊢ B = {Base}_{R}$
	dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
	dvdsrneg.5	$⊢ N = {inv}_{g} (R)$
Assertion	dvdsrneg	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{∥} N (X)$

Step	Hyp	Ref	Expression
1		dvdsr.1	$⊢ B = {Base}_{R}$
2		dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
3		dvdsrneg.5	$⊢ N = {inv}_{g} (R)$
4		id	$⊢ X \in B \to X \in B$
5		ringgrp	$⊢ R \in Ring \to R \in Grp$
6		eqid	$⊢ 1_{R} = 1_{R}$
7	1 6	ringidcl	$⊢ R \in Ring \to 1_{R} \in B$
8	1 3	grpinvcl	$⊢ (R \in Grp \land 1_{R} \in B) \to N (1_{R}) \in B$
9	5 7 8	syl2anc	$⊢ R \in Ring \to N (1_{R}) \in B$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11	1 2 10	dvdsrmul	$⊢ (X \in B \land N (1_{R}) \in B) \to X \underset{˙}{∥} (N (1_{R}) \cdot_{R} X)$
12	4 9 11	syl2anr	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{∥} (N (1_{R}) \cdot_{R} X)$
13		simpl	$⊢ (R \in Ring \land X \in B) \to R \in Ring$
14		simpr	$⊢ (R \in Ring \land X \in B) \to X \in B$
15	1 10 6 3 13 14	ringnegl	$⊢ (R \in Ring \land X \in B) \to N (1_{R}) \cdot_{R} X = N (X)$
16	12 15	breqtrd	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{∥} N (X)$

Metamath Proof Explorer