This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝑈 )