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 31339 |
. . 3
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍)) |
5 | 4 | 3expa 1117 |
. 2
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍)) |
6 | | simpll 764 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝐺 ∈ oGrp) |
7 | | ogrpgrp 31325 |
. . . . . 6
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝐺 ∈ Grp) |
9 | | simplr1 1214 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝑋 ∈ 𝐵) |
10 | | simplr3 1216 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝑍 ∈ 𝐵) |
11 | 1, 3 | grpcl 18583 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 + 𝑍) ∈ 𝐵) |
12 | 8, 9, 10, 11 | syl3anc 1370 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑋 + 𝑍) ∈ 𝐵) |
13 | | simplr2 1215 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝑌 ∈ 𝐵) |
14 | 1, 3 | grpcl 18583 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 + 𝑍) ∈ 𝐵) |
15 | 8, 13, 10, 14 | syl3anc 1370 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑌 + 𝑍) ∈ 𝐵) |
16 | | eqid 2740 |
. . . . . 6
⊢
(invg‘𝐺) = (invg‘𝐺) |
17 | 1, 16 | grpinvcl 18625 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵) → ((invg‘𝐺)‘𝑍) ∈ 𝐵) |
18 | 8, 10, 17 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((invg‘𝐺)‘𝑍) ∈ 𝐵) |
19 | | simpr 485 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑋 + 𝑍) < (𝑌 + 𝑍)) |
20 | 1, 2, 3 | ogrpaddlt 31339 |
. . . 4
⊢ ((𝐺 ∈ oGrp ∧ ((𝑋 + 𝑍) ∈ 𝐵 ∧ (𝑌 + 𝑍) ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑍) ∈ 𝐵) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑋 + 𝑍) +
((invg‘𝐺)‘𝑍)) < ((𝑌 + 𝑍) +
((invg‘𝐺)‘𝑍))) |
21 | 6, 12, 15, 18, 19, 20 | syl131anc 1382 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑋 + 𝑍) +
((invg‘𝐺)‘𝑍)) < ((𝑌 + 𝑍) +
((invg‘𝐺)‘𝑍))) |
22 | 1, 3 | grpass 18584 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑍) ∈ 𝐵)) → ((𝑋 + 𝑍) +
((invg‘𝐺)‘𝑍)) = (𝑋 + (𝑍 +
((invg‘𝐺)‘𝑍)))) |
23 | 8, 9, 10, 18, 22 | syl13anc 1371 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑋 + 𝑍) +
((invg‘𝐺)‘𝑍)) = (𝑋 + (𝑍 +
((invg‘𝐺)‘𝑍)))) |
24 | | eqid 2740 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
25 | 1, 3, 24, 16 | grprinv 18627 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵) → (𝑍 +
((invg‘𝐺)‘𝑍)) = (0g‘𝐺)) |
26 | 8, 10, 25 | syl2anc 584 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑍 +
((invg‘𝐺)‘𝑍)) = (0g‘𝐺)) |
27 | 26 | oveq2d 7287 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑋 + (𝑍 +
((invg‘𝐺)‘𝑍))) = (𝑋 + (0g‘𝐺))) |
28 | 1, 3, 24 | grprid 18608 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + (0g‘𝐺)) = 𝑋) |
29 | 8, 9, 28 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑋 + (0g‘𝐺)) = 𝑋) |
30 | 23, 27, 29 | 3eqtrd 2784 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑋 + 𝑍) +
((invg‘𝐺)‘𝑍)) = 𝑋) |
31 | 1, 3 | grpass 18584 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ((invg‘𝐺)‘𝑍) ∈ 𝐵)) → ((𝑌 + 𝑍) +
((invg‘𝐺)‘𝑍)) = (𝑌 + (𝑍 +
((invg‘𝐺)‘𝑍)))) |
32 | 8, 13, 10, 18, 31 | syl13anc 1371 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑌 + 𝑍) +
((invg‘𝐺)‘𝑍)) = (𝑌 + (𝑍 +
((invg‘𝐺)‘𝑍)))) |
33 | 26 | oveq2d 7287 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑌 + (𝑍 +
((invg‘𝐺)‘𝑍))) = (𝑌 + (0g‘𝐺))) |
34 | 1, 3, 24 | grprid 18608 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵) → (𝑌 + (0g‘𝐺)) = 𝑌) |
35 | 8, 13, 34 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → (𝑌 + (0g‘𝐺)) = 𝑌) |
36 | 32, 33, 35 | 3eqtrd 2784 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → ((𝑌 + 𝑍) +
((invg‘𝐺)‘𝑍)) = 𝑌) |
37 | 21, 30, 36 | 3brtr3d 5110 |
. 2
⊢ (((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ (𝑋 + 𝑍) < (𝑌 + 𝑍)) → 𝑋 < 𝑌) |
38 | 5, 37 | impbida 798 |
1
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 < 𝑌 ↔ (𝑋 + 𝑍) < (𝑌 + 𝑍))) |