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		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
16		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
17		eqid	⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
18	1 15 9 16 17	isunit	⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
19	18	bilani	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
20	19	simpld	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
21	5 9	dvdsrtr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) 𝑋 ∧ 𝑋 ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
22	3 14 20 21	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
23	16	opprring	⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
24	23	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( oppr ‘ 𝑅 ) ∈ Ring )
25	16 5	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
26	16 2	opprneg	⊢ 𝑁 = ( invg ‘ ( oppr ‘ 𝑅 ) )
27	25 17 26	dvdsrneg	⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ ( 𝑁 ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) )
28	24 8 27	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 𝑁 ‘ ( 𝑁 ‘ 𝑋 ) ) )
29	28 13	breqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 )
30	19	simprd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
31	25 17	dvdsrtr	⊢ ( ( ( oppr ‘ 𝑅 ) ∈ Ring ∧ ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
32	24 29 30 31	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) )
33	1 15 9 16 17	isunit	⊢ ( ( 𝑁 ‘ 𝑋 ) ∈ 𝑈 ↔ ( ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ∧ ( 𝑁 ‘ 𝑋 ) ( ∥r ‘ ( oppr ‘ 𝑅 ) ) ( 1r ‘ 𝑅 ) ) )
34	22 32 33	sylanbrc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝑈 )