Step | Hyp | Ref
| Expression |
1 | | legval.p |
. . . . . 6
⊢ 𝑃 = (Base‘𝐺) |
2 | | eqid 2738 |
. . . . . 6
⊢
(LineG‘𝐺) =
(LineG‘𝐺) |
3 | | legval.i |
. . . . . 6
⊢ 𝐼 = (Itv‘𝐺) |
4 | | legval.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | 4 | ad4antr 729 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → 𝐺 ∈ TarskiG) |
6 | | legtrd.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
7 | 6 | ad4antr 729 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → 𝐶 ∈ 𝑃) |
8 | | legtrd.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
9 | 8 | ad4antr 729 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → 𝐷 ∈ 𝑃) |
10 | | simp-4r 781 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → 𝑥 ∈ 𝑃) |
11 | | eqid 2738 |
. . . . . 6
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
12 | | legtrd.e |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
13 | 12 | ad4antr 729 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → 𝐸 ∈ 𝑃) |
14 | | simplr 766 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → 𝑦 ∈ 𝑃) |
15 | | legval.d |
. . . . . 6
⊢ − =
(dist‘𝐺) |
16 | | simpllr 773 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) |
17 | 16 | simpld 495 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → 𝑥 ∈ (𝐶𝐼𝐷)) |
18 | 1, 2, 3, 5, 7, 10,
9, 17 | btwncolg3 26918 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → (𝐷 ∈ (𝐶(LineG‘𝐺)𝑥) ∨ 𝐶 = 𝑥)) |
19 | | simprr 770 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → (𝐶 − 𝐷) = (𝐸 − 𝑦)) |
20 | 1, 2, 3, 5, 7, 9, 10, 11, 13, 14, 15, 18, 19 | lnext 26928 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → ∃𝑧 ∈ 𝑃 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) |
21 | 5 | ad2antrr 723 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝐺 ∈ TarskiG) |
22 | 13 | ad2antrr 723 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝐸 ∈ 𝑃) |
23 | | simplr 766 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝑧 ∈ 𝑃) |
24 | | simp-4r 781 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝑦 ∈ 𝑃) |
25 | | legtrd.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
26 | 25 | ad6antr 733 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝐹 ∈ 𝑃) |
27 | 7 | ad2antrr 723 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝐶 ∈ 𝑃) |
28 | 10 | ad2antrr 723 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝑥 ∈ 𝑃) |
29 | 9 | ad2antrr 723 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝐷 ∈ 𝑃) |
30 | | simpr 485 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) |
31 | 1, 15, 3, 11, 21, 27, 29, 28, 22, 24, 23, 30 | cgr3swap23 26885 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 〈“𝐶𝑥𝐷”〉(cgrG‘𝐺)〈“𝐸𝑧𝑦”〉) |
32 | 17 | ad2antrr 723 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝑥 ∈ (𝐶𝐼𝐷)) |
33 | 1, 15, 3, 11, 21, 27, 28, 29, 22, 23, 24, 31, 32 | tgbtwnxfr 26891 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝑧 ∈ (𝐸𝐼𝑦)) |
34 | | simpllr 773 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) |
35 | 34 | simpld 495 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝑦 ∈ (𝐸𝐼𝐹)) |
36 | 1, 15, 3, 21, 22, 23, 24, 26, 33, 35 | tgbtwnexch 26859 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → 𝑧 ∈ (𝐸𝐼𝐹)) |
37 | | simp-5r 783 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) |
38 | 37 | simprd 496 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → (𝐴 − 𝐵) = (𝐶 − 𝑥)) |
39 | 1, 15, 3, 11, 21, 27, 28, 29, 22, 23, 24, 31 | cgr3simp1 26881 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → (𝐶 − 𝑥) = (𝐸 − 𝑧)) |
40 | 38, 39 | eqtrd 2778 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → (𝐴 − 𝐵) = (𝐸 − 𝑧)) |
41 | 36, 40 | jca 512 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) ∧ 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉) → (𝑧 ∈ (𝐸𝐼𝐹) ∧ (𝐴 − 𝐵) = (𝐸 − 𝑧))) |
42 | 41 | ex 413 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) ∧ 𝑧 ∈ 𝑃) → (〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉 → (𝑧 ∈ (𝐸𝐼𝐹) ∧ (𝐴 − 𝐵) = (𝐸 − 𝑧)))) |
43 | 42 | reximdva 3203 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → (∃𝑧 ∈ 𝑃 〈“𝐶𝐷𝑥”〉(cgrG‘𝐺)〈“𝐸𝑦𝑧”〉 → ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝐸𝐼𝐹) ∧ (𝐴 − 𝐵) = (𝐸 − 𝑧)))) |
44 | 20, 43 | mpd 15 |
. . . 4
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) ∧ 𝑦 ∈ 𝑃) ∧ (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) → ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝐸𝐼𝐹) ∧ (𝐴 − 𝐵) = (𝐸 − 𝑧))) |
45 | | legtrd.2 |
. . . . . 6
⊢ (𝜑 → (𝐶 − 𝐷) ≤ (𝐸 − 𝐹)) |
46 | | legval.l |
. . . . . . 7
⊢ ≤ =
(≤G‘𝐺) |
47 | 1, 15, 3, 46, 4, 6,
8, 12, 25 | legov 26946 |
. . . . . 6
⊢ (𝜑 → ((𝐶 − 𝐷) ≤ (𝐸 − 𝐹) ↔ ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦)))) |
48 | 45, 47 | mpbid 231 |
. . . . 5
⊢ (𝜑 → ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) |
49 | 48 | ad2antrr 723 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) → ∃𝑦 ∈ 𝑃 (𝑦 ∈ (𝐸𝐼𝐹) ∧ (𝐶 − 𝐷) = (𝐸 − 𝑦))) |
50 | 44, 49 | r19.29a 3218 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) → ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝐸𝐼𝐹) ∧ (𝐴 − 𝐵) = (𝐸 − 𝑧))) |
51 | | legtrd.1 |
. . . 4
⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐶 − 𝐷)) |
52 | | legid.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
53 | | legid.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
54 | 1, 15, 3, 46, 4, 52, 53, 6, 8 | legov 26946 |
. . . 4
⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐶 − 𝐷) ↔ ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥)))) |
55 | 51, 54 | mpbid 231 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ 𝑃 (𝑥 ∈ (𝐶𝐼𝐷) ∧ (𝐴 − 𝐵) = (𝐶 − 𝑥))) |
56 | 50, 55 | r19.29a 3218 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝐸𝐼𝐹) ∧ (𝐴 − 𝐵) = (𝐸 − 𝑧))) |
57 | 1, 15, 3, 46, 4, 52, 53, 12, 25 | legov 26946 |
. 2
⊢ (𝜑 → ((𝐴 − 𝐵) ≤ (𝐸 − 𝐹) ↔ ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝐸𝐼𝐹) ∧ (𝐴 − 𝐵) = (𝐸 − 𝑧)))) |
58 | 56, 57 | mpbird 256 |
1
⊢ (𝜑 → (𝐴 − 𝐵) ≤ (𝐸 − 𝐹)) |