Proof of Theorem ornglmullt
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 | ornglmulle 31223 |
. 2
⊢ (𝜑 → (𝑍 · 𝑋)(le‘𝑅)(𝑍 · 𝑌)) |
24 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑍 · 𝑋) = (𝑍 · 𝑌)) → (𝑍 · 𝑋) = (𝑍 · 𝑌)) |
25 | 24 | oveq2d 7229 |
. . . . 5
⊢ ((𝜑 ∧ (𝑍 · 𝑋) = (𝑍 · 𝑌)) → (((invr‘𝑅)‘𝑍) · (𝑍 · 𝑋)) = (((invr‘𝑅)‘𝑍) · (𝑍 · 𝑌))) |
26 | | ornglmullt.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ DivRing) |
27 | 10 | pltne 17840 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ( 0 < 𝑍 → 0 ≠ 𝑍)) |
28 | 27 | imp 410 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 0 < 𝑍) → 0 ≠ 𝑍) |
29 | 4, 18, 7, 19, 28 | syl31anc 1375 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≠ 𝑍) |
30 | 29 | necomd 2996 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ≠ 0 ) |
31 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Unit‘𝑅) =
(Unit‘𝑅) |
32 | 1, 31, 3 | drngunit 19772 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ DivRing → (𝑍 ∈ (Unit‘𝑅) ↔ (𝑍 ∈ 𝐵 ∧ 𝑍 ≠ 0 ))) |
33 | 32 | biimpar 481 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ DivRing ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ≠ 0 )) → 𝑍 ∈ (Unit‘𝑅)) |
34 | 26, 7, 30, 33 | syl12anc 837 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ (Unit‘𝑅)) |
35 | | eqid 2737 |
. . . . . . . . . 10
⊢
(invr‘𝑅) = (invr‘𝑅) |
36 | | eqid 2737 |
. . . . . . . . . 10
⊢
(1r‘𝑅) = (1r‘𝑅) |
37 | 31, 35, 2, 36 | unitlinv 19695 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ (Unit‘𝑅)) →
(((invr‘𝑅)‘𝑍) · 𝑍) = (1r‘𝑅)) |
38 | 15, 34, 37 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 →
(((invr‘𝑅)‘𝑍) · 𝑍) = (1r‘𝑅)) |
39 | 38 | oveq1d 7228 |
. . . . . . 7
⊢ (𝜑 →
((((invr‘𝑅)‘𝑍) · 𝑍) · 𝑋) = ((1r‘𝑅) · 𝑋)) |
40 | 31, 35, 1 | ringinvcl 19694 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ (Unit‘𝑅)) →
((invr‘𝑅)‘𝑍) ∈ 𝐵) |
41 | 15, 34, 40 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 →
((invr‘𝑅)‘𝑍) ∈ 𝐵) |
42 | 1, 2 | ringass 19582 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
(((invr‘𝑅)‘𝑍) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → ((((invr‘𝑅)‘𝑍) · 𝑍) · 𝑋) = (((invr‘𝑅)‘𝑍) · (𝑍 · 𝑋))) |
43 | 15, 41, 7, 5, 42 | syl13anc 1374 |
. . . . . . 7
⊢ (𝜑 →
((((invr‘𝑅)‘𝑍) · 𝑍) · 𝑋) = (((invr‘𝑅)‘𝑍) · (𝑍 · 𝑋))) |
44 | 1, 2, 36 | ringlidm 19589 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ((1r‘𝑅) · 𝑋) = 𝑋) |
45 | 15, 5, 44 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 →
((1r‘𝑅)
·
𝑋) = 𝑋) |
46 | 39, 43, 45 | 3eqtr3d 2785 |
. . . . . 6
⊢ (𝜑 →
(((invr‘𝑅)‘𝑍) · (𝑍 · 𝑋)) = 𝑋) |
47 | 46 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑍 · 𝑋) = (𝑍 · 𝑌)) → (((invr‘𝑅)‘𝑍) · (𝑍 · 𝑋)) = 𝑋) |
48 | 38 | oveq1d 7228 |
. . . . . . 7
⊢ (𝜑 →
((((invr‘𝑅)‘𝑍) · 𝑍) · 𝑌) = ((1r‘𝑅) · 𝑌)) |
49 | 1, 2 | ringass 19582 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
(((invr‘𝑅)‘𝑍) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((((invr‘𝑅)‘𝑍) · 𝑍) · 𝑌) = (((invr‘𝑅)‘𝑍) · (𝑍 · 𝑌))) |
50 | 15, 41, 7, 6, 49 | syl13anc 1374 |
. . . . . . 7
⊢ (𝜑 →
((((invr‘𝑅)‘𝑍) · 𝑍) · 𝑌) = (((invr‘𝑅)‘𝑍) · (𝑍 · 𝑌))) |
51 | 1, 2, 36 | ringlidm 19589 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵) → ((1r‘𝑅) · 𝑌) = 𝑌) |
52 | 15, 6, 51 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 →
((1r‘𝑅)
·
𝑌) = 𝑌) |
53 | 48, 50, 52 | 3eqtr3d 2785 |
. . . . . 6
⊢ (𝜑 →
(((invr‘𝑅)‘𝑍) · (𝑍 · 𝑌)) = 𝑌) |
54 | 53 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑍 · 𝑋) = (𝑍 · 𝑌)) → (((invr‘𝑅)‘𝑍) · (𝑍 · 𝑌)) = 𝑌) |
55 | 25, 47, 54 | 3eqtr3d 2785 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 · 𝑋) = (𝑍 · 𝑌)) → 𝑋 = 𝑌) |
56 | 10 | pltne 17840 |
. . . . . . . 8
⊢ ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → 𝑋 ≠ 𝑌)) |
57 | 56 | imp 410 |
. . . . . . 7
⊢ (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝑋 ≠ 𝑌) |
58 | 4, 5, 6, 9, 57 | syl31anc 1375 |
. . . . . 6
⊢ (𝜑 → 𝑋 ≠ 𝑌) |
59 | 58 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑍 · 𝑋) = (𝑍 · 𝑌)) → 𝑋 ≠ 𝑌) |
60 | 59 | neneqd 2945 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 · 𝑋) = (𝑍 · 𝑌)) → ¬ 𝑋 = 𝑌) |
61 | 55, 60 | pm2.65da 817 |
. . 3
⊢ (𝜑 → ¬ (𝑍 · 𝑋) = (𝑍 · 𝑌)) |
62 | 61 | neqned 2947 |
. 2
⊢ (𝜑 → (𝑍 · 𝑋) ≠ (𝑍 · 𝑌)) |
63 | 1, 2 | ringcl 19579 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑍 · 𝑋) ∈ 𝐵) |
64 | 15, 7, 5, 63 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑍 · 𝑋) ∈ 𝐵) |
65 | 1, 2 | ringcl 19579 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑍 · 𝑌) ∈ 𝐵) |
66 | 15, 7, 6, 65 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑍 · 𝑌) ∈ 𝐵) |
67 | 8, 10 | pltval 17838 |
. . 3
⊢ ((𝑅 ∈ oRing ∧ (𝑍 · 𝑋) ∈ 𝐵 ∧ (𝑍 · 𝑌) ∈ 𝐵) → ((𝑍 · 𝑋) < (𝑍 · 𝑌) ↔ ((𝑍 · 𝑋)(le‘𝑅)(𝑍 · 𝑌) ∧ (𝑍 · 𝑋) ≠ (𝑍 · 𝑌)))) |
68 | 4, 64, 66, 67 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((𝑍 · 𝑋) < (𝑍 · 𝑌) ↔ ((𝑍 · 𝑋)(le‘𝑅)(𝑍 · 𝑌) ∧ (𝑍 · 𝑋) ≠ (𝑍 · 𝑌)))) |
69 | 23, 62, 68 | mpbir2and 713 |
1
⊢ (𝜑 → (𝑍 · 𝑋) < (𝑍 · 𝑌)) |