Proof of Theorem ogrpaddltbi
| Step | Hyp | Ref
| Expression |
| 1 | | ogrpaddlt.0 |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
| 2 | | ogrpaddlt.1 |
. . . 4
⊢ < =
(lt‘𝐺) |
| 3 | | ogrpaddlt.2 |
. . . 4
⊢ + =
(+g‘𝐺) |
| 4 | 1, 2, 3 | ogrpaddlt 33094 |
. . 3
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍)) |
| 5 | 4 | 3expa 1119 |
. 2
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍)) |
| 6 | | simpll 767 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝐺 ∈ oGrp) |
| 7 | | ogrpgrp 33080 |
. . . . . 6
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) |
| 8 | 6, 7 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝐺 ∈ Grp) |
| 9 | | simplr1 1216 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝑋 ∈ 𝐵) |
| 10 | | simplr3 1218 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝑍 ∈ 𝐵) |
| 11 | 1, 3 | grpcl 18959 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + 𝑍) ∈ 𝐵) |
| 12 | 8, 9, 10, 11 | syl3anc 1373 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑋 + 𝑍) ∈ 𝐵) |
| 13 | | simplr2 1217 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝑌 ∈ 𝐵) |
| 14 | 1, 3 | grpcl 18959 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵) |
| 15 | 8, 13, 10, 14 | syl3anc 1373 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑌 + 𝑍) ∈ 𝐵) |
| 16 | | eqid 2737 |
. . . . . 6
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 17 | 1, 16 | grpinvcl 19005 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵) → ((invg‘𝐺)‘𝑍) ∈ 𝐵) |
| 18 | 8, 10, 17 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((invg‘𝐺)‘𝑍) ∈ 𝐵) |
| 19 | | simpr 484 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑋 + 𝑍) < (𝑌 + 𝑍)) |
| 20 | 1, 2, 3 | ogrpaddlt 33094 |
. . . 4
⊢ ((𝐺 ∈ oGrp ∧ ((𝑋 + 𝑍) ∈ 𝐵 ∧ (𝑌 + 𝑍) ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑍) ∈ 𝐵) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑋 + 𝑍) +
((invg‘𝐺)‘𝑍)) < ((𝑌 + 𝑍) +
((invg‘𝐺)‘𝑍))) |
| 21 | 6, 12, 15, 18, 19, 20 | syl131anc 1385 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑋 + 𝑍) +
((invg‘𝐺)‘𝑍)) < ((𝑌 + 𝑍) +
((invg‘𝐺)‘𝑍))) |
| 22 | 1, 3 | grpass 18960 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑍) ∈ 𝐵)) → ((𝑋 + 𝑍) +
((invg‘𝐺)‘𝑍)) = (𝑋 + (𝑍 +
((invg‘𝐺)‘𝑍)))) |
| 23 | 8, 9, 10, 18, 22 | syl13anc 1374 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑋 + 𝑍) +
((invg‘𝐺)‘𝑍)) = (𝑋 + (𝑍 +
((invg‘𝐺)‘𝑍)))) |
| 24 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 25 | 1, 3, 24, 16 | grprinv 19008 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵) → (𝑍 +
((invg‘𝐺)‘𝑍)) = (0g‘𝐺)) |
| 26 | 8, 10, 25 | syl2anc 584 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑍 +
((invg‘𝐺)‘𝑍)) = (0g‘𝐺)) |
| 27 | 26 | oveq2d 7447 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑋 + (𝑍 +
((invg‘𝐺)‘𝑍))) = (𝑋 + (0g‘𝐺))) |
| 28 | 1, 3, 24 | grprid 18986 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + (0g‘𝐺)) = 𝑋) |
| 29 | 8, 9, 28 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑋 + (0g‘𝐺)) = 𝑋) |
| 30 | 23, 27, 29 | 3eqtrd 2781 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑋 + 𝑍) +
((invg‘𝐺)‘𝑍)) = 𝑋) |
| 31 | 1, 3 | grpass 18960 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑍) ∈ 𝐵)) → ((𝑌 + 𝑍) +
((invg‘𝐺)‘𝑍)) = (𝑌 + (𝑍 +
((invg‘𝐺)‘𝑍)))) |
| 32 | 8, 13, 10, 18, 31 | syl13anc 1374 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑌 + 𝑍) +
((invg‘𝐺)‘𝑍)) = (𝑌 + (𝑍 +
((invg‘𝐺)‘𝑍)))) |
| 33 | 26 | oveq2d 7447 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑌 + (𝑍 +
((invg‘𝐺)‘𝑍))) = (𝑌 + (0g‘𝐺))) |
| 34 | 1, 3, 24 | grprid 18986 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵) → (𝑌 + (0g‘𝐺)) = 𝑌) |
| 35 | 8, 13, 34 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑌 + (0g‘𝐺)) = 𝑌) |
| 36 | 32, 33, 35 | 3eqtrd 2781 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑌 + 𝑍) +
((invg‘𝐺)‘𝑍)) = 𝑌) |
| 37 | 21, 30, 36 | 3brtr3d 5174 |
. 2
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝑋 < 𝑌) |
| 38 | 5, 37 | impbida 801 |
1
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 < 𝑌 ↔ (𝑋 + 𝑍) < (𝑌 + 𝑍))) |