Proof of Theorem orngrmulle
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.3 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
16 | | ornglmullt.4 |
. . . . 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, 20, 16, 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 | 11, 23 | grpsubcl 17318 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌(-g‘𝑅)𝑋) ∈ 𝐵) |
27 | 10, 15, 20, 26 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝑌(-g‘𝑅)𝑋) ∈ 𝐵) |
28 | 11, 12, 23 | grpsubid 17322 |
. . . . . . 7
⊢ ((𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋(-g‘𝑅)𝑋) = 0 ) |
29 | 10, 20, 28 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝑋(-g‘𝑅)𝑋) = 0 ) |
30 | | orngmulle.5 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
31 | | orngmulle.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝑅) |
32 | 11, 31, 23 | ogrpsub 29048 |
. . . . . . 7
⊢ ((𝑅 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋(-g‘𝑅)𝑋) ≤ (𝑌(-g‘𝑅)𝑋)) |
33 | 3, 20, 15, 20, 30, 32 | syl131anc 1331 |
. . . . . 6
⊢ (𝜑 → (𝑋(-g‘𝑅)𝑋) ≤ (𝑌(-g‘𝑅)𝑋)) |
34 | 29, 33 | eqbrtrrd 4607 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝑌(-g‘𝑅)𝑋)) |
35 | | orngmulle.6 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝑍) |
36 | 11, 31, 12, 17 | orngmul 29134 |
. . . . 5
⊢ ((𝑅 ∈ oRing ∧ ((𝑌(-g‘𝑅)𝑋) ∈ 𝐵 ∧ 0 ≤ (𝑌(-g‘𝑅)𝑋)) ∧ (𝑍 ∈ 𝐵 ∧ 0 ≤ 𝑍)) → 0 ≤ ((𝑌(-g‘𝑅)𝑋) · 𝑍)) |
37 | 1, 27, 34, 16, 35, 36 | syl122anc 1327 |
. . . 4
⊢ (𝜑 → 0 ≤ ((𝑌(-g‘𝑅)𝑋) · 𝑍)) |
38 | 11, 17, 23, 8, 15, 20, 16 | rngsubdir 18423 |
. . . 4
⊢ (𝜑 → ((𝑌(-g‘𝑅)𝑋) · 𝑍) = ((𝑌 · 𝑍)(-g‘𝑅)(𝑋 · 𝑍))) |
39 | 37, 38 | breqtrd 4609 |
. . 3
⊢ (𝜑 → 0 ≤ ((𝑌 · 𝑍)(-g‘𝑅)(𝑋 · 𝑍))) |
40 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
41 | 11, 31, 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
⊢ (𝜑 → (𝑋 · 𝑍) ≤ (𝑌 · 𝑍)) |