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		eqid	$⊢ 1_{R} = 1_{R}$
16		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
17		eqid	$⊢ ∥_{r} ({opp}_{r} (R)) = ∥_{r} ({opp}_{r} (R))$
18	1 15 9 16 17	isunit	$⊢ X \in U \leftrightarrow (X ∥_{r} (R) 1_{R} \land X ∥_{r} ({opp}_{r} (R)) 1_{R})$
19	18	bilani	$⊢ (R \in Ring \land X \in U) \to (X ∥_{r} (R) 1_{R} \land X ∥_{r} ({opp}_{r} (R)) 1_{R})$
20	19	simpld	$⊢ (R \in Ring \land X \in U) \to X ∥_{r} (R) 1_{R}$
21	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}$
22	3 14 20 21	syl3anc	$⊢ (R \in Ring \land X \in U) \to N (X) ∥_{r} (R) 1_{R}$
23	16	opprring	$⊢ R \in Ring \to {opp}_{r} (R) \in Ring$
24	23	adantr	$⊢ (R \in Ring \land X \in U) \to {opp}_{r} (R) \in Ring$
25	16 5	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (R)}$
26	16 2	opprneg	$⊢ N = {inv}_{g} ({opp}_{r} (R))$
27	25 17 26	dvdsrneg	$⊢ ({opp}_{r} (R) \in Ring \land N (X) \in {Base}_{R}) \to N (X) ∥_{r} ({opp}_{r} (R)) N (N (X))$
28	24 8 27	syl2anc	$⊢ (R \in Ring \land X \in U) \to N (X) ∥_{r} ({opp}_{r} (R)) N (N (X))$
29	28 13	breqtrd	$⊢ (R \in Ring \land X \in U) \to N (X) ∥_{r} ({opp}_{r} (R)) X$
30	19	simprd	$⊢ (R \in Ring \land X \in U) \to X ∥_{r} ({opp}_{r} (R)) 1_{R}$
31	25 17	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}$
32	24 29 30 31	syl3anc	$⊢ (R \in Ring \land X \in U) \to N (X) ∥_{r} ({opp}_{r} (R)) 1_{R}$
33	1 15 9 16 17	isunit	$⊢ N (X) \in U \leftrightarrow (N (X) ∥_{r} (R) 1_{R} \land N (X) ∥_{r} ({opp}_{r} (R)) 1_{R})$
34	22 32 33	sylanbrc	$⊢ (R \in Ring \land X \in U) \to N (X) \in U$

Metamath Proof Explorer

Theorem unitnegcl

Proof