Theorem unitnegcl

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

	Ref	Expression
Hypotheses	unitnegcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	unitnegcl.2	⊢ 𝑁 = ( invg ‘ 𝑅 )
Assertion	unitnegcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		unitnegcl.1	⊢ 𝑈 = ( Unit ‘ 𝑅 )
2		unitnegcl.2	⊢ 𝑁 = ( invg ‘ 𝑅 )
3		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → 𝑅 ∈ Ring )
4		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	5 1	unitcl	⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
7	5 2	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
8	4 6 7	syl2an	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) )
9		eqid	⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
10	5 9 2	dvdsrneg	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) )
11	8 10	syldan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) )
12	5 2	grpinvinv	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
13	4 6 12	syl2an	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) = 𝑋 )
14	11 13	breqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) 𝑋 )
15		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
16		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
17		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
18		eqid	⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
19	1 16 9 17 18	isunit	⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
20	15 19	sylib	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
21	20	simpld	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
22	5 9	dvdsrtr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) 𝑋 ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
23	3 14 21 22	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
24	17	opprring	⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
25	24	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( oppr ‘ 𝑅 ) ∈ Ring )
26	17 5	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
27	17 2	opprneg	⊢ 𝑁 = ( invg ‘ ( oppr ‘ 𝑅 ) )
28	26 18 27	dvdsrneg	⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ ( 𝑁 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) )
29	25 8 28	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) )
30	29 13	breqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 )
31	20	simprd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
32	26 18	dvdsrtr	⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
33	25 30 31 32	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
34	1 16 9 17 18	isunit	⊢ ( ( 𝑁 ‘ 𝑋 ) ∈ 𝑈 ↔ ( ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
35	23 33 34	sylanbrc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝑈 )