Proof of Theorem ogrpaddltrbid
| Step | Hyp | Ref
| Expression |
| 1 | | ogrpaddlt.0 |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
| 2 | | ogrpaddlt.1 |
. . 3
⊢ < =
(lt‘𝐺) |
| 3 | | ogrpaddlt.2 |
. . 3
⊢ + =
(+g‘𝐺) |
| 4 | | ogrpaddltrd.1 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝑉) |
| 5 | 4 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 𝐺 ∈ 𝑉) |
| 6 | | ogrpaddltrd.2 |
. . . 4
⊢ (𝜑 →
(oppg‘𝐺) ∈ oGrp) |
| 7 | 6 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (oppg‘𝐺) ∈ oGrp) |
| 8 | | ogrpaddltrd.3 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 9 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 𝑋 ∈ 𝐵) |
| 10 | | ogrpaddltrd.4 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 11 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 𝑌 ∈ 𝐵) |
| 12 | | ogrpaddltrd.5 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
| 13 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 𝑍 ∈ 𝐵) |
| 14 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 𝑋 < 𝑌) |
| 15 | 1, 2, 3, 5, 7, 9, 11, 13, 14 | ogrpaddltrd 33096 |
. 2
⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (𝑍 + 𝑋) < (𝑍 + 𝑌)) |
| 16 | 4 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → 𝐺 ∈ 𝑉) |
| 17 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) →
(oppg‘𝐺) ∈ oGrp) |
| 18 | | ogrpgrp 33080 |
. . . . . . 7
⊢
((oppg‘𝐺) ∈ oGrp →
(oppg‘𝐺) ∈ Grp) |
| 19 | 6, 18 | syl 17 |
. . . . . 6
⊢ (𝜑 →
(oppg‘𝐺) ∈ Grp) |
| 20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) →
(oppg‘𝐺) ∈ Grp) |
| 21 | 8 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → 𝑋 ∈ 𝐵) |
| 22 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → 𝑍 ∈ 𝐵) |
| 23 | | eqid 2737 |
. . . . . . 7
⊢
(oppg‘𝐺) = (oppg‘𝐺) |
| 24 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘(oppg‘𝐺)) =
(+g‘(oppg‘𝐺)) |
| 25 | 3, 23, 24 | oppgplus 19367 |
. . . . . 6
⊢ (𝑋(+g‘(oppg‘𝐺))𝑍) = (𝑍 + 𝑋) |
| 26 | 23, 1 | oppgbas 19370 |
. . . . . . 7
⊢ 𝐵 =
(Base‘(oppg‘𝐺)) |
| 27 | 26, 24 | grpcl 18959 |
. . . . . 6
⊢
(((oppg‘𝐺) ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋(+g‘(oppg‘𝐺))𝑍) ∈ 𝐵) |
| 28 | 25, 27 | eqeltrrid 2846 |
. . . . 5
⊢
(((oppg‘𝐺) ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑍 + 𝑋) ∈ 𝐵) |
| 29 | 20, 21, 22, 28 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → (𝑍 + 𝑋) ∈ 𝐵) |
| 30 | 10 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → 𝑌 ∈ 𝐵) |
| 31 | 3, 23, 24 | oppgplus 19367 |
. . . . . 6
⊢ (𝑌(+g‘(oppg‘𝐺))𝑍) = (𝑍 + 𝑌) |
| 32 | 26, 24 | grpcl 18959 |
. . . . . 6
⊢
(((oppg‘𝐺) ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌(+g‘(oppg‘𝐺))𝑍) ∈ 𝐵) |
| 33 | 31, 32 | eqeltrrid 2846 |
. . . . 5
⊢
(((oppg‘𝐺) ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑍 + 𝑌) ∈ 𝐵) |
| 34 | 20, 30, 22, 33 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → (𝑍 + 𝑌) ∈ 𝐵) |
| 35 | 23 | oppggrpb 19377 |
. . . . . 6
⊢ (𝐺 ∈ Grp ↔
(oppg‘𝐺) ∈ Grp) |
| 36 | 20, 35 | sylibr 234 |
. . . . 5
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → 𝐺 ∈ Grp) |
| 37 | | eqid 2737 |
. . . . . 6
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 38 | 1, 37 | grpinvcl 19005 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵) → ((invg‘𝐺)‘𝑍) ∈ 𝐵) |
| 39 | 36, 22, 38 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → ((invg‘𝐺)‘𝑍) ∈ 𝐵) |
| 40 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → (𝑍 + 𝑋) < (𝑍 + 𝑌)) |
| 41 | 1, 2, 3, 16, 17, 29, 34, 39, 40 | ogrpaddltrd 33096 |
. . 3
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → (((invg‘𝐺)‘𝑍) + (𝑍 + 𝑋)) <
(((invg‘𝐺)‘𝑍) + (𝑍 + 𝑌))) |
| 42 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 43 | 1, 3, 42, 37 | grplinv 19007 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑍 ∈ 𝐵) → (((invg‘𝐺)‘𝑍) + 𝑍) = (0g‘𝐺)) |
| 44 | 36, 22, 43 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → (((invg‘𝐺)‘𝑍) + 𝑍) = (0g‘𝐺)) |
| 45 | 44 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → ((((invg‘𝐺)‘𝑍) + 𝑍) + 𝑋) = ((0g‘𝐺) + 𝑋)) |
| 46 | 1, 3 | grpass 18960 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑍) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → ((((invg‘𝐺)‘𝑍) + 𝑍) + 𝑋) = (((invg‘𝐺)‘𝑍) + (𝑍 + 𝑋))) |
| 47 | 36, 39, 22, 21, 46 | syl13anc 1374 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → ((((invg‘𝐺)‘𝑍) + 𝑍) + 𝑋) = (((invg‘𝐺)‘𝑍) + (𝑍 + 𝑋))) |
| 48 | 1, 3, 42 | grplid 18985 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((0g‘𝐺) + 𝑋) = 𝑋) |
| 49 | 36, 21, 48 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → ((0g‘𝐺) + 𝑋) = 𝑋) |
| 50 | 45, 47, 49 | 3eqtr3d 2785 |
. . 3
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → (((invg‘𝐺)‘𝑍) + (𝑍 + 𝑋)) = 𝑋) |
| 51 | 44 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → ((((invg‘𝐺)‘𝑍) + 𝑍) + 𝑌) = ((0g‘𝐺) + 𝑌)) |
| 52 | 1, 3 | grpass 18960 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘𝑍) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((((invg‘𝐺)‘𝑍) + 𝑍) + 𝑌) = (((invg‘𝐺)‘𝑍) + (𝑍 + 𝑌))) |
| 53 | 36, 39, 22, 30, 52 | syl13anc 1374 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → ((((invg‘𝐺)‘𝑍) + 𝑍) + 𝑌) = (((invg‘𝐺)‘𝑍) + (𝑍 + 𝑌))) |
| 54 | 1, 3, 42 | grplid 18985 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵) → ((0g‘𝐺) + 𝑌) = 𝑌) |
| 55 | 36, 30, 54 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → ((0g‘𝐺) + 𝑌) = 𝑌) |
| 56 | 51, 53, 55 | 3eqtr3d 2785 |
. . 3
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → (((invg‘𝐺)‘𝑍) + (𝑍 + 𝑌)) = 𝑌) |
| 57 | 41, 50, 56 | 3brtr3d 5174 |
. 2
⊢ ((𝜑 ∧ (𝑍 + 𝑋) < (𝑍 + 𝑌)) → 𝑋 < 𝑌) |
| 58 | 15, 57 | impbida 801 |
1
⊢ (𝜑 → (𝑋 < 𝑌 ↔ (𝑍 + 𝑋) < (𝑍 + 𝑌))) |