Step | Hyp | Ref
| Expression |
1 | | iscgra.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
2 | | iscgra.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
3 | | iscgra.k |
. . 3
⊢ 𝐾 = (hlG‘𝐺) |
4 | | iscgra.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | | iscgra.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
6 | | iscgra.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
7 | | iscgra.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
8 | | iscgra.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
9 | | iscgra.e |
. . 3
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
10 | | iscgra.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | iscgra 27170 |
. 2
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ∃𝑦 ∈ 𝑃 ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹))) |
12 | 9 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝐸 ∈ 𝑃) |
13 | 6 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝐵 ∈ 𝑃) |
14 | 5 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝐴 ∈ 𝑃) |
15 | 4 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝐺 ∈ TarskiG) |
16 | 8 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝐷 ∈ 𝑃) |
17 | | iscgra1.m |
. . . . . . . 8
⊢ − =
(dist‘𝐺) |
18 | | simpllr 773 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝑦 ∈ 𝑃) |
19 | | simpr2 1194 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝑦(𝐾‘𝐸)𝐷) |
20 | 1, 2, 3, 18, 16, 12, 15, 19 | hlne2 26967 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝐷 ≠ 𝐸) |
21 | | iscgra1.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
22 | 21 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝐴 ≠ 𝐵) |
23 | 22 | necomd 2999 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝐵 ≠ 𝐴) |
24 | 1, 2, 3, 16, 12, 12, 15, 20 | hlid 26970 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝐷(𝐾‘𝐸)𝐷) |
25 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
26 | 7 | ad3antrrr 727 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝐶 ∈ 𝑃) |
27 | | simplr 766 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝑥 ∈ 𝑃) |
28 | | simpr1 1193 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉) |
29 | 1, 17, 2, 25, 15, 14, 13, 26, 18, 12, 27, 28 | cgr3simp1 26881 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → (𝐴 − 𝐵) = (𝑦 − 𝐸)) |
30 | 29 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → (𝑦 − 𝐸) = (𝐴 − 𝐵)) |
31 | 1, 17, 2, 15, 18, 12, 14, 13, 30 | tgcgrcomlr 26841 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → (𝐸 − 𝑦) = (𝐵 − 𝐴)) |
32 | | iscgra1.2 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
33 | 32 | ad3antrrr 727 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) |
34 | 33 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → (𝐷 − 𝐸) = (𝐴 − 𝐵)) |
35 | 1, 17, 2, 15, 16, 12, 14, 13, 34 | tgcgrcomlr 26841 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → (𝐸 − 𝐷) = (𝐵 − 𝐴)) |
36 | 1, 2, 3, 12, 13, 14, 15, 16, 17, 20, 23, 18, 16, 19, 24, 31, 35 | hlcgreulem 26978 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝑦 = 𝐷) |
37 | | simpr3 1195 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → 𝑥(𝐾‘𝐸)𝐹) |
38 | 36, 28, 37 | jca32 516 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) → (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) |
39 | | simprrl 778 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉) |
40 | | simprl 768 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) → 𝑦 = 𝐷) |
41 | 8 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) → 𝐷 ∈ 𝑃) |
42 | 9 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) → 𝐸 ∈ 𝑃) |
43 | 4 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) → 𝐺 ∈ TarskiG) |
44 | 1, 17, 2, 4, 5, 6, 8, 9, 32, 21 | tgcgrneq 26844 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ≠ 𝐸) |
45 | 44 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) → 𝐷 ≠ 𝐸) |
46 | 1, 2, 3, 41, 41, 42, 43, 45 | hlid 26970 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) → 𝐷(𝐾‘𝐸)𝐷) |
47 | 40, 46 | eqbrtrd 5096 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) → 𝑦(𝐾‘𝐸)𝐷) |
48 | | simprrr 779 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) → 𝑥(𝐾‘𝐸)𝐹) |
49 | 39, 47, 48 | 3jca 1127 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) ∧ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹)) |
50 | 38, 49 | impbida 798 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑃) ∧ 𝑥 ∈ 𝑃) → ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹) ↔ (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹)))) |
51 | 50 | rexbidva 3225 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑃) → (∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹) ↔ ∃𝑥 ∈ 𝑃 (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹)))) |
52 | | r19.42v 3279 |
. . . 4
⊢
(∃𝑥 ∈
𝑃 (𝑦 = 𝐷 ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹)) ↔ (𝑦 = 𝐷 ∧ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) |
53 | 51, 52 | bitrdi 287 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑃) → (∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹) ↔ (𝑦 = 𝐷 ∧ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹)))) |
54 | 53 | rexbidva 3225 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ 𝑃 ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑦(𝐾‘𝐸)𝐷 ∧ 𝑥(𝐾‘𝐸)𝐹) ↔ ∃𝑦 ∈ 𝑃 (𝑦 = 𝐷 ∧ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹)))) |
55 | | id 22 |
. . . . . . . 8
⊢ (𝑦 = 𝐷 → 𝑦 = 𝐷) |
56 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑦 = 𝐷 → 𝐸 = 𝐸) |
57 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑦 = 𝐷 → 𝑥 = 𝑥) |
58 | 55, 56, 57 | s3eqd 14577 |
. . . . . . 7
⊢ (𝑦 = 𝐷 → 〈“𝑦𝐸𝑥”〉 = 〈“𝐷𝐸𝑥”〉) |
59 | 58 | breq2d 5086 |
. . . . . 6
⊢ (𝑦 = 𝐷 → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ↔ 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑥”〉)) |
60 | 59 | anbi1d 630 |
. . . . 5
⊢ (𝑦 = 𝐷 → ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹) ↔ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) |
61 | 60 | rexbidv 3226 |
. . . 4
⊢ (𝑦 = 𝐷 → (∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹) ↔ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) |
62 | 61 | ceqsrexv 3585 |
. . 3
⊢ (𝐷 ∈ 𝑃 → (∃𝑦 ∈ 𝑃 (𝑦 = 𝐷 ∧ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹)) ↔ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) |
63 | 8, 62 | syl 17 |
. 2
⊢ (𝜑 → (∃𝑦 ∈ 𝑃 (𝑦 = 𝐷 ∧ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑦𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹)) ↔ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) |
64 | 11, 54, 63 | 3bitrd 305 |
1
⊢ (𝜑 → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝐹))) |