Proof of Theorem ornglmulle
Step | Hyp | Ref
| Expression |
1 | | ornglmullt.1 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ oRing) |
2 | | orngogrp 29132 |
. . . . 5
⊢ (𝑅 ∈ oRing → 𝑅 ∈ oGrp) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ oGrp) |
4 | | isogrp 29033 |
. . . . 5
⊢ (𝑅 ∈ oGrp ↔ (𝑅 ∈ Grp ∧ 𝑅 ∈ oMnd)) |
5 | 4 | simprbi 479 |
. . . 4
⊢ (𝑅 ∈ oGrp → 𝑅 ∈ oMnd) |
6 | 3, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ oMnd) |
7 | | orngring 29131 |
. . . . . 6
⊢ (𝑅 ∈ oRing → 𝑅 ∈ Ring) |
8 | 1, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
9 | | ringgrp 18375 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
10 | 8, 9 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ Grp) |
11 | | ornglmullt.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
12 | | ornglmullt.0 |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
13 | 11, 12 | grpidcl 17273 |
. . . 4
⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
14 | 10, 13 | syl 17 |
. . 3
⊢ (𝜑 → 0 ∈ 𝐵) |
15 | | ornglmullt.4 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
16 | | ornglmullt.3 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
17 | | ornglmullt.t |
. . . . . 6
⊢ · =
(.r‘𝑅) |
18 | 11, 17 | ringcl 18384 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑍 · 𝑌) ∈ 𝐵) |
19 | 8, 15, 16, 18 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (𝑍 · 𝑌) ∈ 𝐵) |
20 | | ornglmullt.2 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
21 | 11, 17 | ringcl 18384 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑍 · 𝑋) ∈ 𝐵) |
22 | 8, 15, 20, 21 | syl3anc 1318 |
. . . 4
⊢ (𝜑 → (𝑍 · 𝑋) ∈ 𝐵) |
23 | | eqid 2610 |
. . . . 5
⊢
(-g‘𝑅) = (-g‘𝑅) |
24 | 11, 23 | grpsubcl 17318 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ (𝑍 · 𝑌) ∈ 𝐵 ∧ (𝑍 · 𝑋) ∈ 𝐵) → ((𝑍 · 𝑌)(-g‘𝑅)(𝑍 · 𝑋)) ∈ 𝐵) |
25 | 10, 19, 22, 24 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((𝑍 · 𝑌)(-g‘𝑅)(𝑍 · 𝑋)) ∈ 𝐵) |
26 | | orngmulle.6 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝑍) |
27 | 11, 23 | grpsubcl 17318 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌(-g‘𝑅)𝑋) ∈ 𝐵) |
28 | 10, 16, 20, 27 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝑌(-g‘𝑅)𝑋) ∈ 𝐵) |
29 | 11, 12, 23 | grpsubid 17322 |
. . . . . . 7
⊢ ((𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋(-g‘𝑅)𝑋) = 0 ) |
30 | 10, 20, 29 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝑋(-g‘𝑅)𝑋) = 0 ) |
31 | | orngmulle.5 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
32 | | orngmulle.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝑅) |
33 | 11, 32, 23 | ogrpsub 29048 |
. . . . . . 7
⊢ ((𝑅 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋(-g‘𝑅)𝑋) ≤ (𝑌(-g‘𝑅)𝑋)) |
34 | 3, 20, 16, 20, 31, 33 | syl131anc 1331 |
. . . . . 6
⊢ (𝜑 → (𝑋(-g‘𝑅)𝑋) ≤ (𝑌(-g‘𝑅)𝑋)) |
35 | 30, 34 | eqbrtrrd 4607 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝑌(-g‘𝑅)𝑋)) |
36 | 11, 32, 12, 17 | orngmul 29134 |
. . . . 5
⊢ ((𝑅 ∈ oRing ∧ (𝑍 ∈ 𝐵 ∧ 0 ≤ 𝑍) ∧ ((𝑌(-g‘𝑅)𝑋) ∈ 𝐵 ∧ 0 ≤ (𝑌(-g‘𝑅)𝑋))) → 0 ≤ (𝑍 · (𝑌(-g‘𝑅)𝑋))) |
37 | 1, 15, 26, 28, 35, 36 | syl122anc 1327 |
. . . 4
⊢ (𝜑 → 0 ≤ (𝑍 · (𝑌(-g‘𝑅)𝑋))) |
38 | 11, 17, 23, 8, 15, 16, 20 | ringsubdi 18422 |
. . . 4
⊢ (𝜑 → (𝑍 · (𝑌(-g‘𝑅)𝑋)) = ((𝑍 · 𝑌)(-g‘𝑅)(𝑍 · 𝑋))) |
39 | 37, 38 | breqtrd 4609 |
. . 3
⊢ (𝜑 → 0 ≤ ((𝑍 · 𝑌)(-g‘𝑅)(𝑍 · 𝑋))) |
40 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
41 | 11, 32, 40 | omndadd 29037 |
. . 3
⊢ ((𝑅 ∈ oMnd ∧ ( 0 ∈ 𝐵 ∧ ((𝑍 · 𝑌)(-g‘𝑅)(𝑍 · 𝑋)) ∈ 𝐵 ∧ (𝑍 · 𝑋) ∈ 𝐵) ∧ 0 ≤ ((𝑍 · 𝑌)(-g‘𝑅)(𝑍 · 𝑋))) → ( 0 (+g‘𝑅)(𝑍 · 𝑋)) ≤ (((𝑍 · 𝑌)(-g‘𝑅)(𝑍 · 𝑋))(+g‘𝑅)(𝑍 · 𝑋))) |
42 | 6, 14, 25, 22, 39, 41 | syl131anc 1331 |
. 2
⊢ (𝜑 → ( 0 (+g‘𝑅)(𝑍 · 𝑋)) ≤ (((𝑍 · 𝑌)(-g‘𝑅)(𝑍 · 𝑋))(+g‘𝑅)(𝑍 · 𝑋))) |
43 | 11, 40, 12 | grplid 17275 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ (𝑍 · 𝑋) ∈ 𝐵) → ( 0 (+g‘𝑅)(𝑍 · 𝑋)) = (𝑍 · 𝑋)) |
44 | 10, 22, 43 | syl2anc 691 |
. 2
⊢ (𝜑 → ( 0 (+g‘𝑅)(𝑍 · 𝑋)) = (𝑍 · 𝑋)) |
45 | 11, 40, 23 | grpnpcan 17330 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ (𝑍 · 𝑌) ∈ 𝐵 ∧ (𝑍 · 𝑋) ∈ 𝐵) → (((𝑍 · 𝑌)(-g‘𝑅)(𝑍 · 𝑋))(+g‘𝑅)(𝑍 · 𝑋)) = (𝑍 · 𝑌)) |
46 | 10, 19, 22, 45 | syl3anc 1318 |
. 2
⊢ (𝜑 → (((𝑍 · 𝑌)(-g‘𝑅)(𝑍 · 𝑋))(+g‘𝑅)(𝑍 · 𝑋)) = (𝑍 · 𝑌)) |
47 | 42, 44, 46 | 3brtr3d 4614 |
1
⊢ (𝜑 → (𝑍 · 𝑋) ≤ (𝑍 · 𝑌)) |