unitnegcl

Description: The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	unitnegcl.1	$⊢ U = Unit (R)$
	unitnegcl.2	$⊢ N = {inv}_{g} (R)$
Assertion	unitnegcl	$⊢ (R \in Ring \land X \in U) \to N (X) \in U$

Proof

Step	Hyp	Ref	Expression
1		unitnegcl.1	$⊢ U = Unit (R)$
2		unitnegcl.2	$⊢ N = {inv}_{g} (R)$
3		simpl	$⊢ (R \in Ring \land X \in U) \to R \in Ring$
4		ringgrp	$⊢ R \in Ring \to R \in Grp$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	5 1	unitcl	$⊢ X \in U \to X \in {Base}_{R}$
7	5 2	grpinvcl	$⊢ (R \in Grp \land X \in {Base}_{R}) \to N (X) \in {Base}_{R}$
8	4 6 7	syl2an	$⊢ (R \in Ring \land X \in U) \to N (X) \in {Base}_{R}$
9		eqid	$⊢ ∥_{r} (R) = ∥_{r} (R)$
10	5 9 2	dvdsrneg	$⊢ (R \in Ring \land N (X) \in {Base}_{R}) \to N (X) ∥_{r} (R) N (N (X))$
11	8 10	syldan	$⊢ (R \in Ring \land X \in U) \to N (X) ∥_{r} (R) N (N (X))$
12	5 2	grpinvinv	$⊢ (R \in Grp \land X \in {Base}_{R}) \to N (N (X)) = X$
13	4 6 12	syl2an	$⊢ (R \in Ring \land X \in U) \to N (N (X)) = X$
14	11 13	breqtrd	$⊢ (R \in Ring \land X \in U) \to N (X) ∥_{r} (R) X$
15		simpr	$⊢ (R \in Ring \land X \in U) \to X \in U$
16		eqid	$⊢ 1_{R} = 1_{R}$
17		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
18		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
19	1 16 9 17 18	isunit	$⊢ X \in U \leftrightarrow (X ∥_{r} (R) 1_{R} \land X ∥_{r} ({opp}_{r} (R)) 1_{R})$
20	15 19	sylib	$⊢ (R \in Ring \land X \in U) \to (X ∥_{r} (R) 1_{R} \land X ∥_{r} ({opp}_{r} (R)) 1_{R})$
21	20	simpld	$⊢ (R \in Ring \land X \in U) \to X ∥_{r} (R) 1_{R}$
22	5 9	dvdsrtr	$⊢ (R \in Ring \land N (X) ∥_{r} (R) X \land X ∥_{r} (R) 1_{R}) \to N (X) ∥_{r} (R) 1_{R}$
23	3 14 21 22	syl3anc	$⊢ (R \in Ring \land X \in U) \to N (X) ∥_{r} (R) 1_{R}$
24	17	opprring	$⊢ R \in Ring \to {opp}_{r} (R) \in Ring$
25	24	adantr	$⊢ (R \in Ring \land X \in U) \to {opp}_{r} (R) \in Ring$
26	17 5	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (R)}$
27	17 2	opprneg	$⊢ N = {inv}_{g} ({opp}_{r} (R))$
28	26 18 27	dvdsrneg	$⊢ ({opp}_{r} (R) \in Ring \land N (X) \in {Base}_{R}) \to N (X) ∥_{r} ({opp}_{r} (R)) N (N (X))$
29	25 8 28	syl2anc	$⊢ (R \in Ring \land X \in U) \to N (X) ∥_{r} ({opp}_{r} (R)) N (N (X))$
30	29 13	breqtrd	$⊢ (R \in Ring \land X \in U) \to N (X) ∥_{r} ({opp}_{r} (R)) X$
31	20	simprd	$⊢ (R \in Ring \land X \in U) \to X ∥_{r} ({opp}_{r} (R)) 1_{R}$
32	26 18	dvdsrtr	$⊢ ({opp}_{r} (R) \in Ring \land N (X) ∥_{r} ({opp}_{r} (R)) X \land X ∥_{r} ({opp}_{r} (R)) 1_{R}) \to N (X) ∥_{r} ({opp}_{r} (R)) 1_{R}$
33	25 30 31 32	syl3anc	$⊢ (R \in Ring \land X \in U) \to N (X) ∥_{r} ({opp}_{r} (R)) 1_{R}$
34	1 16 9 17 18	isunit	$⊢ N (X) \in U \leftrightarrow (N (X) ∥_{r} (R) 1_{R} \land N (X) ∥_{r} ({opp}_{r} (R)) 1_{R})$
35	23 33 34	sylanbrc	$⊢ (R \in Ring \land X \in U) \to N (X) \in U$

Metamath Proof Explorer

Theorem unitnegcl

Proof