Proof of Theorem unitmulcl
Step | Hyp | Ref
| Expression |
1 | | simp1 1135 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑅 ∈ Ring) |
2 | | simp3 1137 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑌 ∈ 𝑈) |
3 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
4 | | unitmulcl.1 |
. . . . . . 7
⊢ 𝑈 = (Unit‘𝑅) |
5 | 3, 4 | unitcl 19901 |
. . . . . 6
⊢ (𝑌 ∈ 𝑈 → 𝑌 ∈ (Base‘𝑅)) |
6 | 2, 5 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑌 ∈ (Base‘𝑅)) |
7 | | simp2 1136 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑋 ∈ 𝑈) |
8 | | eqid 2738 |
. . . . . . . 8
⊢
(1r‘𝑅) = (1r‘𝑅) |
9 | | eqid 2738 |
. . . . . . . 8
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
10 | | eqid 2738 |
. . . . . . . 8
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
11 | | eqid 2738 |
. . . . . . . 8
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
12 | 4, 8, 9, 10, 11 | isunit 19899 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑈 ↔ (𝑋(∥r‘𝑅)(1r‘𝑅) ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
13 | 7, 12 | sylib 217 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋(∥r‘𝑅)(1r‘𝑅) ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
14 | 13 | simpld 495 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑋(∥r‘𝑅)(1r‘𝑅)) |
15 | | unitmulcl.2 |
. . . . . 6
⊢ · =
(.r‘𝑅) |
16 | 3, 9, 15 | dvdsrmul1 19895 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ (Base‘𝑅) ∧ 𝑋(∥r‘𝑅)(1r‘𝑅)) → (𝑋 · 𝑌)(∥r‘𝑅)((1r‘𝑅) · 𝑌)) |
17 | 1, 6, 14, 16 | syl3anc 1370 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌)(∥r‘𝑅)((1r‘𝑅) · 𝑌)) |
18 | 3, 15, 8 | ringlidm 19810 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ (Base‘𝑅)) →
((1r‘𝑅)
·
𝑌) = 𝑌) |
19 | 1, 6, 18 | syl2anc 584 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → ((1r‘𝑅) · 𝑌) = 𝑌) |
20 | 17, 19 | breqtrd 5100 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌)(∥r‘𝑅)𝑌) |
21 | 4, 8, 9, 10, 11 | isunit 19899 |
. . . . 5
⊢ (𝑌 ∈ 𝑈 ↔ (𝑌(∥r‘𝑅)(1r‘𝑅) ∧ 𝑌(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
22 | 2, 21 | sylib 217 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑌(∥r‘𝑅)(1r‘𝑅) ∧ 𝑌(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
23 | 22 | simpld 495 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑌(∥r‘𝑅)(1r‘𝑅)) |
24 | 3, 9 | dvdsrtr 19894 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑋 · 𝑌)(∥r‘𝑅)𝑌 ∧ 𝑌(∥r‘𝑅)(1r‘𝑅)) → (𝑋 · 𝑌)(∥r‘𝑅)(1r‘𝑅)) |
25 | 1, 20, 23, 24 | syl3anc 1370 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌)(∥r‘𝑅)(1r‘𝑅)) |
26 | 10 | opprring 19873 |
. . . 4
⊢ (𝑅 ∈ Ring →
(oppr‘𝑅) ∈ Ring) |
27 | 1, 26 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (oppr‘𝑅) ∈ Ring) |
28 | | eqid 2738 |
. . . . 5
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
29 | 3, 15, 10, 28 | opprmul 19865 |
. . . 4
⊢ (𝑌(.r‘(oppr‘𝑅))𝑋) = (𝑋 · 𝑌) |
30 | 3, 4 | unitcl 19901 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑈 → 𝑋 ∈ (Base‘𝑅)) |
31 | 7, 30 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑅)) |
32 | 22 | simprd 496 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑌(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
33 | 10, 3 | opprbas 19869 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘(oppr‘𝑅)) |
34 | 33, 11, 28 | dvdsrmul1 19895 |
. . . . . 6
⊢
(((oppr‘𝑅) ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅) ∧ 𝑌(∥r‘(oppr‘𝑅))(1r‘𝑅)) → (𝑌(.r‘(oppr‘𝑅))𝑋)(∥r‘(oppr‘𝑅))((1r‘𝑅)(.r‘(oppr‘𝑅))𝑋)) |
35 | 27, 31, 32, 34 | syl3anc 1370 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑌(.r‘(oppr‘𝑅))𝑋)(∥r‘(oppr‘𝑅))((1r‘𝑅)(.r‘(oppr‘𝑅))𝑋)) |
36 | 3, 15, 10, 28 | opprmul 19865 |
. . . . . 6
⊢
((1r‘𝑅)(.r‘(oppr‘𝑅))𝑋) = (𝑋 · (1r‘𝑅)) |
37 | 3, 15, 8 | ringridm 19811 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑋 ·
(1r‘𝑅)) =
𝑋) |
38 | 1, 31, 37 | syl2anc 584 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 ·
(1r‘𝑅)) =
𝑋) |
39 | 36, 38 | eqtrid 2790 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → ((1r‘𝑅)(.r‘(oppr‘𝑅))𝑋) = 𝑋) |
40 | 35, 39 | breqtrd 5100 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑌(.r‘(oppr‘𝑅))𝑋)(∥r‘(oppr‘𝑅))𝑋) |
41 | 29, 40 | eqbrtrrid 5110 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌)(∥r‘(oppr‘𝑅))𝑋) |
42 | 13 | simprd 496 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
43 | 33, 11 | dvdsrtr 19894 |
. . 3
⊢
(((oppr‘𝑅) ∈ Ring ∧ (𝑋 · 𝑌)(∥r‘(oppr‘𝑅))𝑋 ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅)) → (𝑋 · 𝑌)(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
44 | 27, 41, 42, 43 | syl3anc 1370 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌)(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
45 | 4, 8, 9, 10, 11 | isunit 19899 |
. 2
⊢ ((𝑋 · 𝑌) ∈ 𝑈 ↔ ((𝑋 · 𝑌)(∥r‘𝑅)(1r‘𝑅) ∧ (𝑋 · 𝑌)(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
46 | 25, 44, 45 | sylanbrc 583 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝑈) |