Step | Hyp | Ref
| Expression |
1 | | dfcgra2.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
2 | | dfcgra2.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
3 | | eqid 2778 |
. . . . 5
⊢
(hlG‘𝐺) =
(hlG‘𝐺) |
4 | | dfcgra2.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | 4 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐺 ∈ TarskiG) |
6 | | dfcgra2.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
7 | 6 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐴 ∈ 𝑃) |
8 | | dfcgra2.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
9 | 8 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐵 ∈ 𝑃) |
10 | | dfcgra2.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
11 | 10 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐶 ∈ 𝑃) |
12 | | dfcgra2.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
13 | 12 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐷 ∈ 𝑃) |
14 | | dfcgra2.e |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
15 | 14 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐸 ∈ 𝑃) |
16 | | dfcgra2.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
17 | 16 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐹 ∈ 𝑃) |
18 | | simpr 479 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
19 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18 | cgrane1 26160 |
. . . 4
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐴 ≠ 𝐵) |
20 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18 | cgrane2 26161 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐵 ≠ 𝐶) |
21 | 20 | necomd 3024 |
. . . 4
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐶 ≠ 𝐵) |
22 | 19, 21 | jca 507 |
. . 3
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → (𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵)) |
23 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18 | cgrane3 26162 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐸 ≠ 𝐷) |
24 | 23 | necomd 3024 |
. . . 4
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐷 ≠ 𝐸) |
25 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18 | cgrane4 26163 |
. . . . 5
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐸 ≠ 𝐹) |
26 | 25 | necomd 3024 |
. . . 4
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → 𝐹 ≠ 𝐸) |
27 | 24, 26 | jca 507 |
. . 3
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸)) |
28 | | simprl 761 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) |
29 | | simprr 763 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) |
30 | 5 | ad5antr 724 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐺 ∈ TarskiG) |
31 | | simp-5r 776 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎 ∈ 𝑃) |
32 | 9 | ad5antr 724 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐵 ∈ 𝑃) |
33 | | simp-4r 774 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐 ∈ 𝑃) |
34 | | simpllr 766 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑑 ∈ 𝑃) |
35 | 15 | ad5antr 724 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐸 ∈ 𝑃) |
36 | | simplr 759 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑓 ∈ 𝑃) |
37 | 17 | ad5antr 724 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹 ∈ 𝑃) |
38 | 13 | ad5antr 724 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷 ∈ 𝑃) |
39 | 11 | ad5antr 724 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ∈ 𝑃) |
40 | 7 | ad5antr 724 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ∈ 𝑃) |
41 | 18 | ad5antr 724 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
42 | 1, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41 | cgracom 26170 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝐴𝐵𝐶”〉) |
43 | 28 | simplld 758 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ∈ (𝐵𝐼𝑎)) |
44 | | dfcgra2.m |
. . . . . . . . . . . . . . . . . 18
⊢ − =
(dist‘𝐺) |
45 | 19 | ad5antr 724 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ≠ 𝐵) |
46 | 1, 44, 2, 30, 32, 40, 31, 43, 45 | tgbtwnne 25841 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐵 ≠ 𝑎) |
47 | 1, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45 | btwnhl1 25963 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴((hlG‘𝐺)‘𝐵)𝑎) |
48 | 1, 2, 3, 40, 31, 32, 30, 47 | hlcomd 25955 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝐴) |
49 | 1, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48 | cgrahl1 26164 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝑎𝐵𝐶”〉) |
50 | 28 | simprld 762 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ∈ (𝐵𝐼𝑐)) |
51 | 21 | ad5antr 724 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ≠ 𝐵) |
52 | 1, 44, 2, 30, 32, 39, 33, 50, 51 | tgbtwnne 25841 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐵 ≠ 𝑐) |
53 | 1, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51 | btwnhl1 25963 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶((hlG‘𝐺)‘𝐵)𝑐) |
54 | 1, 2, 3, 39, 33, 32, 30, 53 | hlcomd 25955 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝐶) |
55 | 1, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54 | cgrahl2 26165 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝑎𝐵𝑐”〉) |
56 | 1, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55 | cgracom 26170 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 〈“𝑎𝐵𝑐”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
57 | 29 | simplld 758 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷 ∈ (𝐸𝐼𝑑)) |
58 | 24 | ad5antr 724 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷 ≠ 𝐸) |
59 | 1, 44, 2, 30, 35, 38, 34, 57, 58 | tgbtwnne 25841 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐸 ≠ 𝑑) |
60 | 1, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58 | btwnhl1 25963 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐷((hlG‘𝐺)‘𝐸)𝑑) |
61 | 1, 2, 3, 38, 34, 35, 30, 60 | hlcomd 25955 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑑((hlG‘𝐺)‘𝐸)𝐷) |
62 | 1, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61 | cgrahl1 26164 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 〈“𝑎𝐵𝑐”〉(cgrA‘𝐺)〈“𝑑𝐸𝐹”〉) |
63 | 29 | simprld 762 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹 ∈ (𝐸𝐼𝑓)) |
64 | 26 | ad5antr 724 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹 ≠ 𝐸) |
65 | 1, 44, 2, 30, 35, 37, 36, 63, 64 | tgbtwnne 25841 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐸 ≠ 𝑓) |
66 | 1, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64 | btwnhl1 25963 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐹((hlG‘𝐺)‘𝐸)𝑓) |
67 | 1, 2, 3, 37, 36, 35, 30, 66 | hlcomd 25955 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑓((hlG‘𝐺)‘𝐸)𝐹) |
68 | 1, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67 | cgrahl2 26165 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 〈“𝑎𝐵𝑐”〉(cgrA‘𝐺)〈“𝑑𝐸𝑓”〉) |
69 | 1, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68 | cgrane1 26160 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎 ≠ 𝐵) |
70 | 1, 2, 3, 31, 40, 32, 30, 69 | hlid 25960 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝑎) |
71 | 1, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68 | cgrane2 26161 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐵 ≠ 𝑐) |
72 | 71 | necomd 3024 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐 ≠ 𝐵) |
73 | 1, 2, 3, 33, 40, 32, 30, 72 | hlid 25960 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝑐) |
74 | 1, 44, 2, 30, 32, 40, 31, 43 | tgbtwncom 25839 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐴 ∈ (𝑎𝐼𝐵)) |
75 | 28 | simplrd 760 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐴 − 𝑎) = (𝐸 − 𝐷)) |
76 | 1, 44, 2, 30, 40, 31, 35, 38, 75 | tgcgrcoml 25830 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑎 − 𝐴) = (𝐸 − 𝐷)) |
77 | 29 | simplrd 760 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐷 − 𝑑) = (𝐵 − 𝐴)) |
78 | 77 | eqcomd 2784 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝐴) = (𝐷 − 𝑑)) |
79 | 1, 44, 2, 30, 32, 40, 38, 34, 78 | tgcgrcoml 25830 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐴 − 𝐵) = (𝐷 − 𝑑)) |
80 | 1, 44, 2, 30, 31, 40, 32, 35, 38, 34, 74, 57, 76, 79 | tgcgrextend 25836 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑎 − 𝐵) = (𝐸 − 𝑑)) |
81 | 1, 44, 2, 30, 31, 32, 35, 34, 80 | tgcgrcoml 25830 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝑎) = (𝐸 − 𝑑)) |
82 | 1, 44, 2, 30, 32, 39, 33, 50 | tgbtwncom 25839 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → 𝐶 ∈ (𝑐𝐼𝐵)) |
83 | 28 | simprrd 764 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐶 − 𝑐) = (𝐸 − 𝐹)) |
84 | 1, 44, 2, 30, 39, 33, 35, 37, 83 | tgcgrcoml 25830 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑐 − 𝐶) = (𝐸 − 𝐹)) |
85 | 29 | simprrd 764 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐹 − 𝑓) = (𝐵 − 𝐶)) |
86 | 85 | eqcomd 2784 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝐶) = (𝐹 − 𝑓)) |
87 | 1, 44, 2, 30, 32, 39, 37, 36, 86 | tgcgrcoml 25830 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐶 − 𝐵) = (𝐹 − 𝑓)) |
88 | 1, 44, 2, 30, 33, 39, 32, 35, 37, 36, 82, 63, 84, 87 | tgcgrextend 25836 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑐 − 𝐵) = (𝐸 − 𝑓)) |
89 | 1, 44, 2, 30, 33, 32, 35, 36, 88 | tgcgrcoml 25830 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝐵 − 𝑐) = (𝐸 − 𝑓)) |
90 | 1, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 73, 81, 89 | cgracgr 26166 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (𝑎 − 𝑐) = (𝑑 − 𝑓)) |
91 | 28, 29, 90 | 3jca 1119 |
. . . . . . . 8
⊢
(((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) |
92 | 91 | ex 403 |
. . . . . . 7
⊢
((((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) |
93 | 92 | reximdva 3198 |
. . . . . 6
⊢
(((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) → (∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) → ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) |
94 | 93 | reximdva 3198 |
. . . . 5
⊢ ((((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) → (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) |
95 | 94 | imp 397 |
. . . 4
⊢
(((((𝜑 ∧
〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) ∧ 𝑎 ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) |
96 | 1, 44, 2, 4, 8, 6, 14, 12 | axtgsegcon 25815 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑎 ∈ 𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷))) |
97 | 1, 44, 2, 4, 8, 10,
14, 16 | axtgsegcon 25815 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑐 ∈ 𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) |
98 | | reeanv 3293 |
. . . . . . . 8
⊢
(∃𝑎 ∈
𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ↔ (∃𝑎 ∈ 𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ ∃𝑐 ∈ 𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) |
99 | 96, 97, 98 | sylanbrc 578 |
. . . . . . 7
⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) |
100 | 1, 44, 2, 4, 14, 12, 8, 6 | axtgsegcon 25815 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑑 ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴))) |
101 | 1, 44, 2, 4, 14, 16, 8, 10 | axtgsegcon 25815 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) |
102 | | reeanv 3293 |
. . . . . . . 8
⊢
(∃𝑑 ∈
𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ↔ (∃𝑑 ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ ∃𝑓 ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) |
103 | 100, 101,
102 | sylanbrc 578 |
. . . . . . 7
⊢ (𝜑 → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) |
104 | 99, 103 | jca 507 |
. . . . . 6
⊢ (𝜑 → (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
105 | | r19.41vv 3277 |
. . . . . . . . 9
⊢
(∃𝑑 ∈
𝑃 ∃𝑓 ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))))) |
106 | | ancom 454 |
. . . . . . . . . 10
⊢ ((((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
107 | 106 | 2rexbii 3225 |
. . . . . . . . 9
⊢
(∃𝑑 ∈
𝑃 ∃𝑓 ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
108 | | ancom 454 |
. . . . . . . . 9
⊢
((∃𝑑 ∈
𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
109 | 105, 107,
108 | 3bitr3i 293 |
. . . . . . . 8
⊢
(∃𝑑 ∈
𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
110 | 109 | 2rexbii 3225 |
. . . . . . 7
⊢
(∃𝑎 ∈
𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
111 | | r19.41vv 3277 |
. . . . . . 7
⊢
(∃𝑎 ∈
𝑃 ∃𝑐 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ (∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
112 | 110, 111 | bitr2i 268 |
. . . . . 6
⊢
((∃𝑎 ∈
𝑃 ∃𝑐 ∈ 𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) ↔ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
113 | 104, 112 | sylib 210 |
. . . . 5
⊢ (𝜑 → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
114 | 113 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
115 | 95, 114 | reximddv2 3202 |
. . 3
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) |
116 | 22, 27, 115 | 3jca 1119 |
. 2
⊢ ((𝜑 ∧ 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) → ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) |
117 | | df-3an 1073 |
. . 3
⊢ (((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) ↔ (((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸)) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) |
118 | 4 | ad6antr 726 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐺 ∈ TarskiG) |
119 | 12 | ad6antr 726 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ∈ 𝑃) |
120 | 14 | ad6antr 726 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐸 ∈ 𝑃) |
121 | 16 | ad6antr 726 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹 ∈ 𝑃) |
122 | 6 | ad6antr 726 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴 ∈ 𝑃) |
123 | 8 | ad6antr 726 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐵 ∈ 𝑃) |
124 | 10 | ad6antr 726 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ∈ 𝑃) |
125 | | simp-4r 774 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑦 ∈ 𝑃) |
126 | | simp-5r 776 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑥 ∈ 𝑃) |
127 | | simpllr 766 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑧 ∈ 𝑃) |
128 | | simplr 759 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑡 ∈ 𝑃) |
129 | | eqid 2778 |
. . . . . . . . . . . . . 14
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
130 | | simpr1 1205 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹)))) |
131 | 130 | simplld 758 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴 ∈ (𝐵𝐼𝑥)) |
132 | | simpr2 1207 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶)))) |
133 | 132 | simplld 758 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ∈ (𝐸𝐼𝑧)) |
134 | 1, 44, 2, 118, 120, 119, 127, 133 | tgbtwncom 25839 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ∈ (𝑧𝐼𝐸)) |
135 | 132 | simplrd 760 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐷 − 𝑧) = (𝐵 − 𝐴)) |
136 | 135 | eqcomd 2784 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝐴) = (𝐷 − 𝑧)) |
137 | 1, 44, 2, 118, 123, 122, 119, 127, 136 | tgcgrcomr 25829 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝐴) = (𝑧 − 𝐷)) |
138 | 130 | simplrd 760 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐴 − 𝑥) = (𝐸 − 𝐷)) |
139 | 1, 44, 2, 118, 122, 126, 120, 119, 138 | tgcgrcomr 25829 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐴 − 𝑥) = (𝐷 − 𝐸)) |
140 | 1, 44, 2, 118, 123, 122, 126, 127, 119, 120, 131, 134, 137, 139 | tgcgrextend 25836 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝑥) = (𝑧 − 𝐸)) |
141 | 1, 44, 2, 118, 123, 126, 127, 120, 140 | tgcgrcoml 25830 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑥 − 𝐵) = (𝑧 − 𝐸)) |
142 | 130 | simprld 762 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ∈ (𝐵𝐼𝑦)) |
143 | 1, 44, 2, 118, 123, 124, 125, 142 | tgbtwncom 25839 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ∈ (𝑦𝐼𝐵)) |
144 | 132 | simprld 762 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹 ∈ (𝐸𝐼𝑡)) |
145 | 130 | simprrd 764 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐶 − 𝑦) = (𝐸 − 𝐹)) |
146 | 1, 44, 2, 118, 124, 125, 120, 121, 145 | tgcgrcoml 25830 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑦 − 𝐶) = (𝐸 − 𝐹)) |
147 | 132 | simprrd 764 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐹 − 𝑡) = (𝐵 − 𝐶)) |
148 | 147 | eqcomd 2784 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝐶) = (𝐹 − 𝑡)) |
149 | 1, 44, 2, 118, 123, 124, 121, 128, 148 | tgcgrcoml 25830 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐶 − 𝐵) = (𝐹 − 𝑡)) |
150 | 1, 44, 2, 118, 125, 124, 123, 120, 121, 128, 143, 144, 146, 149 | tgcgrextend 25836 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑦 − 𝐵) = (𝐸 − 𝑡)) |
151 | 1, 44, 2, 118, 125, 123, 120, 128, 150 | tgcgrcoml 25830 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝐵 − 𝑦) = (𝐸 − 𝑡)) |
152 | | simpr3 1209 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑥 − 𝑦) = (𝑧 − 𝑡)) |
153 | 1, 44, 2, 118, 126, 125, 127, 128, 152 | tgcgrcomlr 25831 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → (𝑦 − 𝑥) = (𝑡 − 𝑧)) |
154 | 1, 44, 129, 118, 126, 123, 125, 127, 120, 128, 141, 151, 153 | trgcgr 25867 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 〈“𝑥𝐵𝑦”〉(cgrG‘𝐺)〈“𝑧𝐸𝑡”〉) |
155 | | simp-6r 778 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) |
156 | 155 | simprld 762 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷 ≠ 𝐸) |
157 | 1, 44, 2, 118, 120, 119, 127, 133, 156 | tgbtwnne 25841 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐸 ≠ 𝑧) |
158 | 1, 2, 3, 120, 127, 119, 118, 123, 133, 157, 156 | btwnhl1 25963 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐷((hlG‘𝐺)‘𝐸)𝑧) |
159 | 1, 2, 3, 119, 127, 120, 118, 158 | hlcomd 25955 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑧((hlG‘𝐺)‘𝐸)𝐷) |
160 | 155 | simprrd 764 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹 ≠ 𝐸) |
161 | 1, 44, 2, 118, 120, 121, 128, 144, 160 | tgbtwnne 25841 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐸 ≠ 𝑡) |
162 | 1, 2, 3, 120, 128, 121, 118, 123, 144, 161, 160 | btwnhl1 25963 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐹((hlG‘𝐺)‘𝐸)𝑡) |
163 | 1, 2, 3, 121, 128, 120, 118, 162 | hlcomd 25955 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝑡((hlG‘𝐺)‘𝐸)𝐹) |
164 | 1, 2, 3, 118, 126, 123, 125, 119, 120, 121, 127, 128, 154, 159, 163 | iscgrad 26159 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 〈“𝑥𝐵𝑦”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
165 | 1, 2, 118, 3, 126, 123, 125, 119, 120, 121, 164 | cgracom 26170 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝑥𝐵𝑦”〉) |
166 | 155 | simplld 758 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴 ≠ 𝐵) |
167 | 1, 44, 2, 118, 123, 122, 126, 131, 166 | tgbtwnne 25841 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐵 ≠ 𝑥) |
168 | 1, 2, 3, 123, 126, 122, 118, 122, 131, 167, 166 | btwnhl1 25963 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐴((hlG‘𝐺)‘𝐵)𝑥) |
169 | 1, 2, 3, 118, 119, 120, 121, 126, 123, 125, 165, 122, 168 | cgrahl1 26164 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝐴𝐵𝑦”〉) |
170 | 155 | simplrd 760 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶 ≠ 𝐵) |
171 | 1, 44, 2, 118, 123, 124, 125, 142, 170 | tgbtwnne 25841 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐵 ≠ 𝑦) |
172 | 1, 2, 3, 123, 125, 124, 118, 122, 142, 171, 170 | btwnhl1 25963 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 𝐶((hlG‘𝐺)‘𝐵)𝑦) |
173 | 1, 2, 3, 118, 119, 120, 121, 122, 123, 125, 169, 124, 172 | cgrahl2 26165 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝐴𝐵𝐶”〉) |
174 | 1, 2, 118, 3, 119, 120, 121, 122, 123, 124, 173 | cgracom 26170 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
175 | 174 | adantl3r 740 |
. . . . . . 7
⊢
((((((((𝜑 ∧
((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) ∧ 𝑧 ∈ 𝑃) ∧ 𝑡 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
176 | | simpr 479 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) |
177 | | eqidd 2779 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑧 → 𝐷 = 𝐷) |
178 | | oveq2 6930 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑧 → (𝐸𝐼𝑑) = (𝐸𝐼𝑧)) |
179 | 177, 178 | eleq12d 2853 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑧 → (𝐷 ∈ (𝐸𝐼𝑑) ↔ 𝐷 ∈ (𝐸𝐼𝑧))) |
180 | | oveq2 6930 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑧 → (𝐷 − 𝑑) = (𝐷 − 𝑧)) |
181 | | eqidd 2779 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑧 → (𝐵 − 𝐴) = (𝐵 − 𝐴)) |
182 | 180, 181 | eqeq12d 2793 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑧 → ((𝐷 − 𝑑) = (𝐵 − 𝐴) ↔ (𝐷 − 𝑧) = (𝐵 − 𝐴))) |
183 | 179, 182 | anbi12d 624 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑧 → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)))) |
184 | | biidd 254 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑧 → ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)) ↔ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)))) |
185 | 183, 184 | anbi12d 624 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑧 → (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))))) |
186 | | eqidd 2779 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑧 → (𝑥 − 𝑦) = (𝑥 − 𝑦)) |
187 | | oveq1 6929 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑧 → (𝑑 − 𝑓) = (𝑧 − 𝑓)) |
188 | 186, 187 | eqeq12d 2793 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑧 → ((𝑥 − 𝑦) = (𝑑 − 𝑓) ↔ (𝑥 − 𝑦) = (𝑧 − 𝑓))) |
189 | 185, 188 | 3anbi23d 1512 |
. . . . . . . . 9
⊢ (𝑑 = 𝑧 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑓)))) |
190 | | biidd 254 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑡 → ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)))) |
191 | | eqidd 2779 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑡 → 𝐹 = 𝐹) |
192 | | oveq2 6930 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑡 → (𝐸𝐼𝑓) = (𝐸𝐼𝑡)) |
193 | 191, 192 | eleq12d 2853 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑡 → (𝐹 ∈ (𝐸𝐼𝑓) ↔ 𝐹 ∈ (𝐸𝐼𝑡))) |
194 | | oveq2 6930 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑡 → (𝐹 − 𝑓) = (𝐹 − 𝑡)) |
195 | | eqidd 2779 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑡 → (𝐵 − 𝐶) = (𝐵 − 𝐶)) |
196 | 194, 195 | eqeq12d 2793 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑡 → ((𝐹 − 𝑓) = (𝐵 − 𝐶) ↔ (𝐹 − 𝑡) = (𝐵 − 𝐶))) |
197 | 193, 196 | anbi12d 624 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑡 → ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶)) ↔ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶)))) |
198 | 190, 197 | anbi12d 624 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑡 → (((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))))) |
199 | | eqidd 2779 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑡 → (𝑥 − 𝑦) = (𝑥 − 𝑦)) |
200 | | oveq2 6930 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑡 → (𝑧 − 𝑓) = (𝑧 − 𝑡)) |
201 | 199, 200 | eqeq12d 2793 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑡 → ((𝑥 − 𝑦) = (𝑧 − 𝑓) ↔ (𝑥 − 𝑦) = (𝑧 − 𝑡))) |
202 | 198, 201 | 3anbi23d 1512 |
. . . . . . . . 9
⊢ (𝑓 = 𝑡 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡)))) |
203 | 189, 202 | cbvrex2v 3376 |
. . . . . . . 8
⊢
(∃𝑑 ∈
𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)) ↔ ∃𝑧 ∈ 𝑃 ∃𝑡 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) |
204 | 176, 203 | sylib 210 |
. . . . . . 7
⊢
(((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → ∃𝑧 ∈ 𝑃 ∃𝑡 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 − 𝑧) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 − 𝑡) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑧 − 𝑡))) |
205 | 175, 204 | r19.29vva 3267 |
. . . . . 6
⊢
(((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
206 | 205 | adantl3r 740 |
. . . . 5
⊢
((((((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
207 | | simpr 479 |
. . . . . 6
⊢ (((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) → ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) |
208 | | eqidd 2779 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → 𝐴 = 𝐴) |
209 | | oveq2 6930 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → (𝐵𝐼𝑎) = (𝐵𝐼𝑥)) |
210 | 208, 209 | eleq12d 2853 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑥 → (𝐴 ∈ (𝐵𝐼𝑎) ↔ 𝐴 ∈ (𝐵𝐼𝑥))) |
211 | | oveq2 6930 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → (𝐴 − 𝑎) = (𝐴 − 𝑥)) |
212 | | eqidd 2779 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → (𝐸 − 𝐷) = (𝐸 − 𝐷)) |
213 | 211, 212 | eqeq12d 2793 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑥 → ((𝐴 − 𝑎) = (𝐸 − 𝐷) ↔ (𝐴 − 𝑥) = (𝐸 − 𝐷))) |
214 | 210, 213 | anbi12d 624 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ↔ (𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)))) |
215 | | biidd 254 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → ((𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)) ↔ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)))) |
216 | 214, 215 | anbi12d 624 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))))) |
217 | | oveq1 6929 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (𝑎 − 𝑐) = (𝑥 − 𝑐)) |
218 | | eqidd 2779 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (𝑑 − 𝑓) = (𝑑 − 𝑓)) |
219 | 217, 218 | eqeq12d 2793 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → ((𝑎 − 𝑐) = (𝑑 − 𝑓) ↔ (𝑥 − 𝑐) = (𝑑 − 𝑓))) |
220 | 216, 219 | 3anbi13d 1511 |
. . . . . . . 8
⊢ (𝑎 = 𝑥 → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓)))) |
221 | 220 | 2rexbidv 3242 |
. . . . . . 7
⊢ (𝑎 = 𝑥 → (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)) ↔ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓)))) |
222 | | biidd 254 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑦 → ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ↔ (𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)))) |
223 | | eqidd 2779 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑦 → 𝐶 = 𝐶) |
224 | | oveq2 6930 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑦 → (𝐵𝐼𝑐) = (𝐵𝐼𝑦)) |
225 | 223, 224 | eleq12d 2853 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑦 → (𝐶 ∈ (𝐵𝐼𝑐) ↔ 𝐶 ∈ (𝐵𝐼𝑦))) |
226 | | oveq2 6930 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑦 → (𝐶 − 𝑐) = (𝐶 − 𝑦)) |
227 | | eqidd 2779 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑦 → (𝐸 − 𝐹) = (𝐸 − 𝐹)) |
228 | 226, 227 | eqeq12d 2793 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑦 → ((𝐶 − 𝑐) = (𝐸 − 𝐹) ↔ (𝐶 − 𝑦) = (𝐸 − 𝐹))) |
229 | 225, 228 | anbi12d 624 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑦 → ((𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹)) ↔ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹)))) |
230 | 222, 229 | anbi12d 624 |
. . . . . . . . 9
⊢ (𝑐 = 𝑦 → (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))))) |
231 | | oveq2 6930 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑦 → (𝑥 − 𝑐) = (𝑥 − 𝑦)) |
232 | | eqidd 2779 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑦 → (𝑑 − 𝑓) = (𝑑 − 𝑓)) |
233 | 231, 232 | eqeq12d 2793 |
. . . . . . . . 9
⊢ (𝑐 = 𝑦 → ((𝑥 − 𝑐) = (𝑑 − 𝑓) ↔ (𝑥 − 𝑦) = (𝑑 − 𝑓))) |
234 | 230, 233 | 3anbi13d 1511 |
. . . . . . . 8
⊢ (𝑐 = 𝑦 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)))) |
235 | 234 | 2rexbidv 3242 |
. . . . . . 7
⊢ (𝑐 = 𝑦 → (∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑐) = (𝑑 − 𝑓)) ↔ ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓)))) |
236 | 221, 235 | cbvrex2v 3376 |
. . . . . 6
⊢
(∃𝑎 ∈
𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)) ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) |
237 | 207, 236 | sylib 210 |
. . . . 5
⊢ (((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 − 𝑥) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 − 𝑦) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑥 − 𝑦) = (𝑑 − 𝑓))) |
238 | 206, 237 | r19.29vva 3267 |
. . . 4
⊢ (((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸))) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
239 | 238 | anasss 460 |
. . 3
⊢ ((𝜑 ∧ (((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸)) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
240 | 117, 239 | sylan2b 587 |
. 2
⊢ ((𝜑 ∧ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓)))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
241 | 116, 240 | impbida 791 |
1
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵) ∧ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸) ∧ ∃𝑎 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 − 𝑎) = (𝐸 − 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 − 𝑐) = (𝐸 − 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 − 𝑑) = (𝐵 − 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝑎 − 𝑐) = (𝑑 − 𝑓))))) |