Proof of Theorem unitmulcl
Step | Hyp | Ref
| Expression |
1 | | simp1 997 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑅 ∈ Ring) |
2 | | eqidd 2178 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (Base‘𝑅) = (Base‘𝑅)) |
3 | | unitmulcl.1 |
. . . . . . 7
⊢ 𝑈 = (Unit‘𝑅) |
4 | 3 | a1i 9 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑈 = (Unit‘𝑅)) |
5 | | ringsrg 13177 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ SRing) |
6 | 1, 5 | syl 14 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑅 ∈ SRing) |
7 | | simp3 999 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑌 ∈ 𝑈) |
8 | 2, 4, 6, 7 | unitcld 13230 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑌 ∈ (Base‘𝑅)) |
9 | | simp2 998 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑋 ∈ 𝑈) |
10 | | eqidd 2178 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (1r‘𝑅) = (1r‘𝑅)) |
11 | | eqidd 2178 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (∥r‘𝑅) =
(∥r‘𝑅)) |
12 | | eqidd 2178 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (oppr‘𝑅) =
(oppr‘𝑅)) |
13 | | eqidd 2178 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) →
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅))) |
14 | 4, 10, 11, 12, 13, 6 | isunitd 13228 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 ∈ 𝑈 ↔ (𝑋(∥r‘𝑅)(1r‘𝑅) ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅)))) |
15 | 9, 14 | mpbid 147 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋(∥r‘𝑅)(1r‘𝑅) ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
16 | 15 | simpld 112 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑋(∥r‘𝑅)(1r‘𝑅)) |
17 | | eqid 2177 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
18 | | eqid 2177 |
. . . . . 6
⊢
(∥r‘𝑅) = (∥r‘𝑅) |
19 | | unitmulcl.2 |
. . . . . 6
⊢ · =
(.r‘𝑅) |
20 | 17, 18, 19 | dvdsrmul1 13224 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ (Base‘𝑅) ∧ 𝑋(∥r‘𝑅)(1r‘𝑅)) → (𝑋 · 𝑌)(∥r‘𝑅)((1r‘𝑅) · 𝑌)) |
21 | 1, 8, 16, 20 | syl3anc 1238 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌)(∥r‘𝑅)((1r‘𝑅) · 𝑌)) |
22 | | eqid 2177 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
23 | 17, 19, 22 | ringlidm 13159 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ (Base‘𝑅)) →
((1r‘𝑅)
·
𝑌) = 𝑌) |
24 | 1, 8, 23 | syl2anc 411 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → ((1r‘𝑅) · 𝑌) = 𝑌) |
25 | 21, 24 | breqtrd 4029 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌)(∥r‘𝑅)𝑌) |
26 | 4, 10, 11, 12, 13, 6 | isunitd 13228 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑌 ∈ 𝑈 ↔ (𝑌(∥r‘𝑅)(1r‘𝑅) ∧ 𝑌(∥r‘(oppr‘𝑅))(1r‘𝑅)))) |
27 | 7, 26 | mpbid 147 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑌(∥r‘𝑅)(1r‘𝑅) ∧ 𝑌(∥r‘(oppr‘𝑅))(1r‘𝑅))) |
28 | 27 | simpld 112 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑌(∥r‘𝑅)(1r‘𝑅)) |
29 | 17, 18 | dvdsrtr 13223 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑋 · 𝑌)(∥r‘𝑅)𝑌 ∧ 𝑌(∥r‘𝑅)(1r‘𝑅)) → (𝑋 · 𝑌)(∥r‘𝑅)(1r‘𝑅)) |
30 | 1, 25, 28, 29 | syl3anc 1238 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌)(∥r‘𝑅)(1r‘𝑅)) |
31 | | eqid 2177 |
. . . . 5
⊢
(oppr‘𝑅) = (oppr‘𝑅) |
32 | 31 | opprring 13202 |
. . . 4
⊢ (𝑅 ∈ Ring →
(oppr‘𝑅) ∈ Ring) |
33 | 1, 32 | syl 14 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (oppr‘𝑅) ∈ Ring) |
34 | 2, 4, 6, 9 | unitcld 13230 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑋 ∈ (Base‘𝑅)) |
35 | 31, 17 | opprbasg 13200 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(Base‘𝑅) =
(Base‘(oppr‘𝑅))) |
36 | 1, 35 | syl 14 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (Base‘𝑅) =
(Base‘(oppr‘𝑅))) |
37 | 34, 36 | eleqtrd 2256 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑋 ∈
(Base‘(oppr‘𝑅))) |
38 | 27 | simprd 114 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑌(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
39 | | eqid 2177 |
. . . . . 6
⊢
(Base‘(oppr‘𝑅)) =
(Base‘(oppr‘𝑅)) |
40 | | eqid 2177 |
. . . . . 6
⊢
(∥r‘(oppr‘𝑅)) =
(∥r‘(oppr‘𝑅)) |
41 | | eqid 2177 |
. . . . . 6
⊢
(.r‘(oppr‘𝑅)) =
(.r‘(oppr‘𝑅)) |
42 | 39, 40, 41 | dvdsrmul1 13224 |
. . . . 5
⊢
(((oppr‘𝑅) ∈ Ring ∧ 𝑋 ∈
(Base‘(oppr‘𝑅)) ∧ 𝑌(∥r‘(oppr‘𝑅))(1r‘𝑅)) → (𝑌(.r‘(oppr‘𝑅))𝑋)(∥r‘(oppr‘𝑅))((1r‘𝑅)(.r‘(oppr‘𝑅))𝑋)) |
43 | 33, 37, 38, 42 | syl3anc 1238 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑌(.r‘(oppr‘𝑅))𝑋)(∥r‘(oppr‘𝑅))((1r‘𝑅)(.r‘(oppr‘𝑅))𝑋)) |
44 | 17, 19, 31, 41 | opprmulg 13196 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ∧ 𝑋 ∈ 𝑈) → (𝑌(.r‘(oppr‘𝑅))𝑋) = (𝑋 · 𝑌)) |
45 | 44 | 3com23 1209 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑌(.r‘(oppr‘𝑅))𝑋) = (𝑋 · 𝑌)) |
46 | 17, 22 | srgidcl 13112 |
. . . . . . 7
⊢ (𝑅 ∈ SRing →
(1r‘𝑅)
∈ (Base‘𝑅)) |
47 | 6, 46 | syl 14 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (1r‘𝑅) ∈ (Base‘𝑅)) |
48 | 17, 19, 31, 41 | opprmulg 13196 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
∈ (Base‘𝑅) ∧
𝑋 ∈ 𝑈) → ((1r‘𝑅)(.r‘(oppr‘𝑅))𝑋) = (𝑋 · (1r‘𝑅))) |
49 | 1, 47, 9, 48 | syl3anc 1238 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → ((1r‘𝑅)(.r‘(oppr‘𝑅))𝑋) = (𝑋 · (1r‘𝑅))) |
50 | 17, 19, 22 | ringridm 13160 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑅)) → (𝑋 ·
(1r‘𝑅)) =
𝑋) |
51 | 1, 34, 50 | syl2anc 411 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 ·
(1r‘𝑅)) =
𝑋) |
52 | 49, 51 | eqtrd 2210 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → ((1r‘𝑅)(.r‘(oppr‘𝑅))𝑋) = 𝑋) |
53 | 43, 45, 52 | 3brtr3d 4034 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌)(∥r‘(oppr‘𝑅))𝑋) |
54 | 15 | simprd 114 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
55 | 39, 40 | dvdsrtr 13223 |
. . 3
⊢
(((oppr‘𝑅) ∈ Ring ∧ (𝑋 · 𝑌)(∥r‘(oppr‘𝑅))𝑋 ∧ 𝑋(∥r‘(oppr‘𝑅))(1r‘𝑅)) → (𝑋 · 𝑌)(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
56 | 33, 53, 54, 55 | syl3anc 1238 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌)(∥r‘(oppr‘𝑅))(1r‘𝑅)) |
57 | 4, 10, 11, 12, 13, 6 | isunitd 13228 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → ((𝑋 · 𝑌) ∈ 𝑈 ↔ ((𝑋 · 𝑌)(∥r‘𝑅)(1r‘𝑅) ∧ (𝑋 · 𝑌)(∥r‘(oppr‘𝑅))(1r‘𝑅)))) |
58 | 30, 56, 57 | mpbir2and 944 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈) → (𝑋 · 𝑌) ∈ 𝑈) |