Proof of Theorem orngrmullt
Step | Hyp | Ref
| Expression |
1 | | ornglmullt.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
2 | | ornglmullt.t |
. . 3
⊢ · =
(.r‘𝑅) |
3 | | ornglmullt.0 |
. . 3
⊢ 0 =
(0g‘𝑅) |
4 | | ornglmullt.1 |
. . 3
⊢ (𝜑 → 𝑅 ∈ oRing) |
5 | | ornglmullt.2 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
6 | | ornglmullt.3 |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
7 | | ornglmullt.4 |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
8 | | eqid 2737 |
. . 3
⊢
(le‘𝑅) =
(le‘𝑅) |
9 | | ornglmullt.5 |
. . . 4
⊢ (𝜑 → 𝑋 < 𝑌) |
10 | | ornglmullt.l |
. . . . . 6
⊢ < =
(lt‘𝑅) |
11 | 8, 10 | pltle 17839 |
. . . . 5
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → 𝑋(le‘𝑅)𝑌)) |
12 | 11 | imp 410 |
. . . 4
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝑋(le‘𝑅)𝑌) |
13 | 4, 5, 6, 9, 12 | syl31anc 1375 |
. . 3
⊢ (𝜑 → 𝑋(le‘𝑅)𝑌) |
14 | | orngring 31218 |
. . . . . 6
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring) |
15 | 4, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
16 | | ringgrp 19567 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
17 | 1, 3 | grpidcl 18395 |
. . . . 5
⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
18 | 15, 16, 17 | 3syl 18 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝐵) |
19 | | ornglmullt.6 |
. . . 4
⊢ (𝜑 → 0 < 𝑍) |
20 | 8, 10 | pltle 17839 |
. . . . 5
⊢ ((𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ( 0 < 𝑍 → 0 (le‘𝑅)𝑍)) |
21 | 20 | imp 410 |
. . . 4
⊢ (((𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 0 < 𝑍) → 0 (le‘𝑅)𝑍) |
22 | 4, 18, 7, 19, 21 | syl31anc 1375 |
. . 3
⊢ (𝜑 → 0 (le‘𝑅)𝑍) |
23 | 1, 2, 3, 4, 5, 6, 7, 8, 13, 22 | orngrmulle 31224 |
. 2
⊢ (𝜑 → (𝑋 · 𝑍)(le‘𝑅)(𝑌 · 𝑍)) |
24 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑋 · 𝑍) = (𝑌 · 𝑍)) → (𝑋 · 𝑍) = (𝑌 · 𝑍)) |
25 | 24 | oveq1d 7228 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 · 𝑍) = (𝑌 · 𝑍)) → ((𝑋 · 𝑍)(/r‘𝑅)𝑍) = ((𝑌 · 𝑍)(/r‘𝑅)𝑍)) |
26 | | ornglmullt.d |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ DivRing) |
27 | 10 | pltne 17840 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ( 0 < 𝑍 → 0 ≠ 𝑍)) |
28 | 27 | imp 410 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 0 < 𝑍) → 0 ≠ 𝑍) |
29 | 4, 18, 7, 19, 28 | syl31anc 1375 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≠ 𝑍) |
30 | 29 | necomd 2996 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 ≠ 0 ) |
31 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
32 | 1, 31, 3 | drngunit 19772 |
. . . . . . . . 9
⊢ (𝑅 ∈ DivRing → (𝑍 ∈ (Unit‘𝑅) ↔ (𝑍 ∈ 𝐵 ∧ 𝑍 ≠ 0 ))) |
33 | 32 | biimpar 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ DivRing ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ≠ 0 )) → 𝑍 ∈ (Unit‘𝑅)) |
34 | 26, 7, 30, 33 | syl12anc 837 |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (Unit‘𝑅)) |
35 | | eqid 2737 |
. . . . . . . 8
⊢
(/r‘𝑅) = (/r‘𝑅) |
36 | 1, 31, 35, 2 | dvrcan3 19710 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ (Unit‘𝑅)) → ((𝑋 · 𝑍)(/r‘𝑅)𝑍) = 𝑋) |
37 | 15, 5, 34, 36 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ((𝑋 · 𝑍)(/r‘𝑅)𝑍) = 𝑋) |
38 | 37 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 · 𝑍) = (𝑌 · 𝑍)) → ((𝑋 · 𝑍)(/r‘𝑅)𝑍) = 𝑋) |
39 | 1, 31, 35, 2 | dvrcan3 19710 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ (Unit‘𝑅)) → ((𝑌 · 𝑍)(/r‘𝑅)𝑍) = 𝑌) |
40 | 15, 6, 34, 39 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ((𝑌 · 𝑍)(/r‘𝑅)𝑍) = 𝑌) |
41 | 40 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 · 𝑍) = (𝑌 · 𝑍)) → ((𝑌 · 𝑍)(/r‘𝑅)𝑍) = 𝑌) |
42 | 25, 38, 41 | 3eqtr3d 2785 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 · 𝑍) = (𝑌 · 𝑍)) → 𝑋 = 𝑌) |
43 | 10 | pltne 17840 |
. . . . . . . 8
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌)) |
44 | 43 | imp 410 |
. . . . . . 7
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝑋 ≠ 𝑌) |
45 | 4, 5, 6, 9, 44 | syl31anc 1375 |
. . . . . 6
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
46 | 45 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 · 𝑍) = (𝑌 · 𝑍)) → 𝑋 ≠ 𝑌) |
47 | 46 | neneqd 2945 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 · 𝑍) = (𝑌 · 𝑍)) → ¬ 𝑋 = 𝑌) |
48 | 42, 47 | pm2.65da 817 |
. . 3
⊢ (𝜑 → ¬ (𝑋 · 𝑍) = (𝑌 · 𝑍)) |
49 | 48 | neqned 2947 |
. 2
⊢ (𝜑 → (𝑋 · 𝑍) ≠ (𝑌 · 𝑍)) |
50 | 1, 2 | ringcl 19579 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 · 𝑍) ∈ 𝐵) |
51 | 15, 5, 7, 50 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑋 · 𝑍) ∈ 𝐵) |
52 | 1, 2 | ringcl 19579 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 · 𝑍) ∈ 𝐵) |
53 | 15, 6, 7, 52 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑌 · 𝑍) ∈ 𝐵) |
54 | 8, 10 | pltval 17838 |
. . 3
⊢ ((𝑅 ∈ oRing ∧ (𝑋 · 𝑍) ∈ 𝐵 ∧ (𝑌 · 𝑍) ∈ 𝐵) → ((𝑋 · 𝑍) < (𝑌 · 𝑍) ↔ ((𝑋 · 𝑍)(le‘𝑅)(𝑌 · 𝑍) ∧ (𝑋 · 𝑍) ≠ (𝑌 · 𝑍)))) |
55 | 4, 51, 53, 54 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((𝑋 · 𝑍) < (𝑌 · 𝑍) ↔ ((𝑋 · 𝑍)(le‘𝑅)(𝑌 · 𝑍) ∧ (𝑋 · 𝑍) ≠ (𝑌 · 𝑍)))) |
56 | 23, 49, 55 | mpbir2and 713 |
1
⊢ (𝜑 → (𝑋 · 𝑍) < (𝑌 · 𝑍)) |