Proof of Theorem ogrpsublt
| Step | Hyp | Ref
| Expression |
| 1 | | simp3 1139 |
. . . . 5
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝑋 < 𝑌) |
| 2 | | simp1 1137 |
. . . . . 6
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝐺 ∈ oGrp) |
| 3 | | simp21 1207 |
. . . . . 6
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝑋 ∈ 𝐵) |
| 4 | | simp22 1208 |
. . . . . 6
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝑌 ∈ 𝐵) |
| 5 | | eqid 2737 |
. . . . . . 7
⊢
(le‘𝐺) =
(le‘𝐺) |
| 6 | | ogrpsublt.1 |
. . . . . . 7
⊢ < =
(lt‘𝐺) |
| 7 | 5, 6 | pltval 18377 |
. . . . . 6
⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋(le‘𝐺)𝑌 ∧ 𝑋 ≠ 𝑌))) |
| 8 | 2, 3, 4, 7 | syl3anc 1373 |
. . . . 5
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 < 𝑌 ↔ (𝑋(le‘𝐺)𝑌 ∧ 𝑋 ≠ 𝑌))) |
| 9 | 1, 8 | mpbid 232 |
. . . 4
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋(le‘𝐺)𝑌 ∧ 𝑋 ≠ 𝑌)) |
| 10 | 9 | simpld 494 |
. . 3
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝑋(le‘𝐺)𝑌) |
| 11 | | ogrpsublt.0 |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
| 12 | | ogrpsublt.2 |
. . . 4
⊢ − =
(-g‘𝐺) |
| 13 | 11, 5, 12 | ogrpsub 33093 |
. . 3
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋(le‘𝐺)𝑌) → (𝑋 − 𝑍)(le‘𝐺)(𝑌 − 𝑍)) |
| 14 | 10, 13 | syld3an3 1411 |
. 2
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍)(le‘𝐺)(𝑌 − 𝑍)) |
| 15 | 9 | simprd 495 |
. . 3
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝑋 ≠ 𝑌) |
| 16 | | ogrpgrp 33080 |
. . . . . 6
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) |
| 17 | 2, 16 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝐺 ∈ Grp) |
| 18 | | simp23 1209 |
. . . . 5
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → 𝑍 ∈ 𝐵) |
| 19 | 11, 12 | grpsubrcan 19039 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑍) = (𝑌 − 𝑍) ↔ 𝑋 = 𝑌)) |
| 20 | 17, 3, 4, 18, 19 | syl13anc 1374 |
. . . 4
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ((𝑋 − 𝑍) = (𝑌 − 𝑍) ↔ 𝑋 = 𝑌)) |
| 21 | 20 | necon3bid 2985 |
. . 3
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ((𝑋 − 𝑍) ≠ (𝑌 − 𝑍) ↔ 𝑋 ≠ 𝑌)) |
| 22 | 15, 21 | mpbird 257 |
. 2
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍) ≠ (𝑌 − 𝑍)) |
| 23 | 11, 12 | grpsubcl 19038 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 − 𝑍) ∈ 𝐵) |
| 24 | 17, 3, 18, 23 | syl3anc 1373 |
. . 3
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍) ∈ 𝐵) |
| 25 | 11, 12 | grpsubcl 19038 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 − 𝑍) ∈ 𝐵) |
| 26 | 17, 4, 18, 25 | syl3anc 1373 |
. . 3
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑌 − 𝑍) ∈ 𝐵) |
| 27 | 5, 6 | pltval 18377 |
. . 3
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 − 𝑍) ∈ 𝐵 ∧ (𝑌 − 𝑍) ∈ 𝐵) → ((𝑋 − 𝑍) < (𝑌 − 𝑍) ↔ ((𝑋 − 𝑍)(le‘𝐺)(𝑌 − 𝑍) ∧ (𝑋 − 𝑍) ≠ (𝑌 − 𝑍)))) |
| 28 | 2, 24, 26, 27 | syl3anc 1373 |
. 2
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ((𝑋 − 𝑍) < (𝑌 − 𝑍) ↔ ((𝑋 − 𝑍)(le‘𝐺)(𝑌 − 𝑍) ∧ (𝑋 − 𝑍) ≠ (𝑌 − 𝑍)))) |
| 29 | 14, 22, 28 | mpbir2and 713 |
1
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍) < (𝑌 − 𝑍)) |