Proof of Theorem unitnegcl
Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → 𝑅 ∈ Ring) |
2 | | ringgrp 13137 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
3 | | eqidd 2178 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (Base‘𝑅) = (Base‘𝑅)) |
4 | | unitnegcl.1 |
. . . . . . . 8
⊢ 𝑈 = (Unit‘𝑅) |
5 | 4 | a1i 9 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → 𝑈 = (Unit‘𝑅)) |
6 | | ringsrg 13177 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing) |
7 | 6 | adantr 276 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → 𝑅 ∈ SRing) |
8 | | simpr 110 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ 𝑈) |
9 | 3, 5, 7, 8 | unitcld 13230 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑅)) |
10 | | eqid 2177 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
11 | | unitnegcl.2 |
. . . . . . 7
⊢ 𝑁 = (invg‘𝑅) |
12 | 10, 11 | grpinvcl 12875 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑁‘𝑋) ∈ (Base‘𝑅)) |
13 | 2, 9, 12 | syl2an2r 595 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ (Base‘𝑅)) |
14 | | eqid 2177 |
. . . . . 6
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
15 | 10, 14, 11 | dvdsrneg 13225 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁‘𝑋) ∈ (Base‘𝑅)) → (𝑁‘𝑋)(∥r‘𝑅)(𝑁‘(𝑁‘𝑋))) |
16 | 13, 15 | syldan 282 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋)(∥r‘𝑅)(𝑁‘(𝑁‘𝑋))) |
17 | 10, 11 | grpinvinv 12891 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑁‘(𝑁‘𝑋)) = 𝑋) |
18 | 2, 9, 17 | syl2an2r 595 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘(𝑁‘𝑋)) = 𝑋) |
19 | 16, 18 | breqtrd 4029 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋)(∥r‘𝑅)𝑋) |
20 | | eqidd 2178 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (1r‘𝑅) = (1r‘𝑅)) |
21 | | eqidd 2178 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (∥r‘𝑅) =
(∥r‘𝑅)) |
22 | | eqidd 2178 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (oppr‘𝑅) =
(oppr‘𝑅)) |
23 | | eqidd 2178 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) →
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅))) |
24 | 5, 20, 21, 22, 23, 7 | isunitd 13228 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋 ∈ 𝑈 ↔ (𝑋(∥r‘𝑅)(1r‘𝑅) ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅)))) |
25 | 8, 24 | mpbid 147 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑋(∥r‘𝑅)(1r‘𝑅) ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
26 | 25 | simpld 112 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → 𝑋(∥r‘𝑅)(1r‘𝑅)) |
27 | 10, 14 | dvdsrtr 13223 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑁‘𝑋)(∥r‘𝑅)𝑋 ∧ 𝑋(∥r‘𝑅)(1r‘𝑅)) → (𝑁‘𝑋)(∥r‘𝑅)(1r‘𝑅)) |
28 | 1, 19, 26, 27 | syl3anc 1238 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋)(∥r‘𝑅)(1r‘𝑅)) |
29 | | eqid 2177 |
. . . . 5
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
30 | 29 | opprring 13202 |
. . . 4
⊢ (𝑅 ∈ Ring →
(oppr‘𝑅) ∈ Ring) |
31 | 30 | adantr 276 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (oppr‘𝑅) ∈ Ring) |
32 | 29, 10 | opprbasg 13200 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) =
(Base‘(oppr‘𝑅))) |
33 | 32 | eleq2d 2247 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → ((𝑁‘𝑋) ∈ (Base‘𝑅) ↔ (𝑁‘𝑋) ∈
(Base‘(oppr‘𝑅)))) |
34 | 33 | adantr 276 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝑁‘𝑋) ∈ (Base‘𝑅) ↔ (𝑁‘𝑋) ∈
(Base‘(oppr‘𝑅)))) |
35 | 13, 34 | mpbid 147 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈
(Base‘(oppr‘𝑅))) |
36 | | eqid 2177 |
. . . . . . 7
⊢
(Base‘(oppr‘𝑅)) =
(Base‘(oppr‘𝑅)) |
37 | | eqid 2177 |
. . . . . . 7
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
38 | | eqid 2177 |
. . . . . . 7
⊢
(invg‘(oppr‘𝑅)) =
(invg‘(oppr‘𝑅)) |
39 | 36, 37, 38 | dvdsrneg 13225 |
. . . . . 6
⊢
(((oppr‘𝑅) ∈ Ring ∧ (𝑁‘𝑋) ∈
(Base‘(oppr‘𝑅))) → (𝑁‘𝑋)(∥r‘(oppr‘𝑅))((invg‘(oppr‘𝑅))‘(𝑁‘𝑋))) |
40 | 30, 35, 39 | syl2an2r 595 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋)(∥r‘(oppr‘𝑅))((invg‘(oppr‘𝑅))‘(𝑁‘𝑋))) |
41 | 29, 11 | opprnegg 13206 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑁 =
(invg‘(oppr‘𝑅))) |
42 | 41 | fveq1d 5517 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (𝑁‘(𝑁‘𝑋)) =
((invg‘(oppr‘𝑅))‘(𝑁‘𝑋))) |
43 | 42 | breq2d 4015 |
. . . . . 6
⊢ (𝑅 ∈ Ring → ((𝑁‘𝑋)(∥r‘(oppr‘𝑅))(𝑁‘(𝑁‘𝑋))
↔ (𝑁‘𝑋)(∥r‘(oppr‘𝑅))((invg‘(oppr‘𝑅))‘(𝑁‘𝑋)))) |
44 | 43 | adantr 276 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝑁‘𝑋)(∥r‘(oppr‘𝑅))(𝑁‘(𝑁‘𝑋))
↔ (𝑁‘𝑋)(∥r‘(oppr‘𝑅))((invg‘(oppr‘𝑅))‘(𝑁‘𝑋)))) |
45 | 40, 44 | mpbird 167 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋)(∥r‘(oppr‘𝑅))(𝑁‘(𝑁‘𝑋))) |
46 | 45, 18 | breqtrd 4029 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋)(∥r‘(oppr‘𝑅))𝑋) |
47 | 25 | simprd 114 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
48 | 36, 37 | dvdsrtr 13223 |
. . 3
⊢
(((oppr‘𝑅) ∈ Ring ∧ (𝑁‘𝑋)(∥r‘(oppr‘𝑅))𝑋 ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅)) → (𝑁‘𝑋)(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
49 | 31, 46, 47, 48 | syl3anc 1238 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋)(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
50 | 5, 20, 21, 22, 23, 7 | isunitd 13228 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → ((𝑁‘𝑋) ∈ 𝑈 ↔ ((𝑁‘𝑋)(∥r‘𝑅)(1r‘𝑅) ∧ (𝑁‘𝑋)(∥r‘(oppr‘𝑅))(1r‘𝑅)))) |
51 | 28, 49, 50 | mpbir2and 944 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈) → (𝑁‘𝑋) ∈ 𝑈) |