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