Step | Hyp | Ref
| Expression |
1 | | dfcgra2.p |
. . 3
⊢ 𝑃 = (Base‘𝐺) |
2 | | dfcgra2.i |
. . 3
⊢ 𝐼 = (Itv‘𝐺) |
3 | | eqid 2738 |
. . 3
⊢
(hlG‘𝐺) =
(hlG‘𝐺) |
4 | | dfcgra2.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | 4 | ad3antrrr 727 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐺 ∈ TarskiG) |
6 | | sacgr.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑃) |
7 | 6 | ad3antrrr 727 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝑋 ∈ 𝑃) |
8 | | dfcgra2.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
9 | 8 | ad3antrrr 727 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐵 ∈ 𝑃) |
10 | | dfcgra2.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
11 | 10 | ad3antrrr 727 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐶 ∈ 𝑃) |
12 | | sacgr.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑃) |
13 | 12 | ad3antrrr 727 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝑌 ∈ 𝑃) |
14 | | dfcgra2.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
15 | 14 | ad3antrrr 727 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐸 ∈ 𝑃) |
16 | | dfcgra2.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
17 | 16 | ad3antrrr 727 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐹 ∈ 𝑃) |
18 | | dfcgra2.m |
. . . 4
⊢ − =
(dist‘𝐺) |
19 | | eqid 2738 |
. . . 4
⊢
(LineG‘𝐺) =
(LineG‘𝐺) |
20 | | eqid 2738 |
. . . 4
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
21 | | eqid 2738 |
. . . 4
⊢
((pInvG‘𝐺)‘𝐸) = ((pInvG‘𝐺)‘𝐸) |
22 | | simpllr 773 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝑥 ∈ 𝑃) |
23 | 1, 18, 2, 19, 20, 5, 15, 21, 22 | mircl 27022 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → (((pInvG‘𝐺)‘𝐸)‘𝑥) ∈ 𝑃) |
24 | | simplr 766 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝑦 ∈ 𝑃) |
25 | | eqid 2738 |
. . . . . . 7
⊢
((pInvG‘𝐺)‘𝐵) = ((pInvG‘𝐺)‘𝐵) |
26 | 1, 18, 2, 19, 20, 4, 8, 25, 6 | mirmir 27023 |
. . . . . 6
⊢ (𝜑 → (((pInvG‘𝐺)‘𝐵)‘(((pInvG‘𝐺)‘𝐵)‘𝑋)) = 𝑋) |
27 | | eqidd 2739 |
. . . . . 6
⊢ (𝜑 → 𝐵 = 𝐵) |
28 | | eqidd 2739 |
. . . . . 6
⊢ (𝜑 → 𝐶 = 𝐶) |
29 | 26, 27, 28 | s3eqd 14577 |
. . . . 5
⊢ (𝜑 →
〈“(((pInvG‘𝐺)‘𝐵)‘(((pInvG‘𝐺)‘𝐵)‘𝑋))𝐵𝐶”〉 = 〈“𝑋𝐵𝐶”〉) |
30 | 29 | ad3antrrr 727 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 〈“(((pInvG‘𝐺)‘𝐵)‘(((pInvG‘𝐺)‘𝐵)‘𝑋))𝐵𝐶”〉 = 〈“𝑋𝐵𝐶”〉) |
31 | | eqid 2738 |
. . . . 5
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) |
32 | 1, 18, 2, 19, 20, 4, 8, 25, 6 | mircl 27022 |
. . . . . 6
⊢ (𝜑 → (((pInvG‘𝐺)‘𝐵)‘𝑋) ∈ 𝑃) |
33 | 32 | ad3antrrr 727 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → (((pInvG‘𝐺)‘𝐵)‘𝑋) ∈ 𝑃) |
34 | | sacgr.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ≠ 𝑋) |
35 | 34 | necomd 2999 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≠ 𝐵) |
36 | 1, 18, 2, 19, 20, 4, 8, 25, 6,
35 | mirne 27028 |
. . . . . 6
⊢ (𝜑 → (((pInvG‘𝐺)‘𝐵)‘𝑋) ≠ 𝐵) |
37 | 36 | ad3antrrr 727 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → (((pInvG‘𝐺)‘𝐵)‘𝑋) ≠ 𝐵) |
38 | | simpr1 1193 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉) |
39 | 1, 18, 2, 19, 20, 5, 31, 25, 21, 33, 9, 22, 15, 11, 24, 37, 38 | mirtrcgr 27044 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 〈“(((pInvG‘𝐺)‘𝐵)‘(((pInvG‘𝐺)‘𝐵)‘𝑋))𝐵𝐶”〉(cgrG‘𝐺)〈“(((pInvG‘𝐺)‘𝐸)‘𝑥)𝐸𝑦”〉) |
40 | 30, 39 | eqbrtrrd 5098 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 〈“𝑋𝐵𝐶”〉(cgrG‘𝐺)〈“(((pInvG‘𝐺)‘𝐸)‘𝑥)𝐸𝑦”〉) |
41 | | sacgr.5 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ≠ 𝑌) |
42 | 41 | ad3antrrr 727 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐸 ≠ 𝑌) |
43 | 42 | necomd 2999 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝑌 ≠ 𝐸) |
44 | | dfcgra2.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
45 | 44 | ad3antrrr 727 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐷 ∈ 𝑃) |
46 | | simpr2 1194 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝑥((hlG‘𝐺)‘𝐸)𝐷) |
47 | 1, 2, 3, 22, 45, 15, 5, 46 | hlne1 26966 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝑥 ≠ 𝐸) |
48 | 1, 18, 2, 19, 20, 5, 15, 21, 22, 47 | mirne 27028 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → (((pInvG‘𝐺)‘𝐸)‘𝑥) ≠ 𝐸) |
49 | 1, 2, 3, 22, 45, 15, 5, 46 | hlcomd 26965 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐷((hlG‘𝐺)‘𝐸)𝑥) |
50 | | sacgr.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝑌)) |
51 | 50 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐸 ∈ (𝐷𝐼𝑌)) |
52 | 1, 2, 3, 45, 22, 13, 5, 15, 49, 51 | btwnhl 26975 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐸 ∈ (𝑥𝐼𝑌)) |
53 | 1, 18, 2, 5, 22, 15, 13, 52 | tgbtwncom 26849 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐸 ∈ (𝑌𝐼𝑥)) |
54 | 1, 18, 2, 19, 20, 5, 15, 21, 22 | mirmir 27023 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → (((pInvG‘𝐺)‘𝐸)‘(((pInvG‘𝐺)‘𝐸)‘𝑥)) = 𝑥) |
55 | 54 | oveq2d 7291 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → (𝑌𝐼(((pInvG‘𝐺)‘𝐸)‘(((pInvG‘𝐺)‘𝐸)‘𝑥))) = (𝑌𝐼𝑥)) |
56 | 53, 55 | eleqtrrd 2842 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝐸 ∈ (𝑌𝐼(((pInvG‘𝐺)‘𝐸)‘(((pInvG‘𝐺)‘𝐸)‘𝑥)))) |
57 | 1, 18, 2, 19, 20, 5, 21, 3, 15, 13, 23, 15, 43, 48, 56 | mirhl2 27042 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝑌((hlG‘𝐺)‘𝐸)(((pInvG‘𝐺)‘𝐸)‘𝑥)) |
58 | 1, 2, 3, 13, 23, 15, 5, 57 | hlcomd 26965 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → (((pInvG‘𝐺)‘𝐸)‘𝑥)((hlG‘𝐺)‘𝐸)𝑌) |
59 | | simpr3 1195 |
. . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 𝑦((hlG‘𝐺)‘𝐸)𝐹) |
60 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 23, 24, 40, 58, 59 | iscgrad 27172 |
. 2
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) → 〈“𝑋𝐵𝐶”〉(cgrA‘𝐺)〈“𝑌𝐸𝐹”〉) |
61 | | dfcgra2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
62 | | sacgr.1 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
63 | 1, 2, 3, 4, 61, 8,
10, 44, 14, 16, 62 | cgrane2 27174 |
. . . . . 6
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
64 | 1, 2, 4, 3, 32, 8,
10, 36, 63 | cgraid 27180 |
. . . . 5
⊢ (𝜑 →
〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrA‘𝐺)〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉) |
65 | 1, 2, 3, 4, 61, 8,
10, 44, 14, 16, 62 | cgrane1 27173 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
66 | | sacgr.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝑋)) |
67 | 26 | oveq2d 7291 |
. . . . . . 7
⊢ (𝜑 → (𝐴𝐼(((pInvG‘𝐺)‘𝐵)‘(((pInvG‘𝐺)‘𝐵)‘𝑋))) = (𝐴𝐼𝑋)) |
68 | 66, 67 | eleqtrrd 2842 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼(((pInvG‘𝐺)‘𝐵)‘(((pInvG‘𝐺)‘𝐵)‘𝑋)))) |
69 | 1, 18, 2, 19, 20, 4, 25, 3, 8,
61, 32, 61, 65, 36, 68 | mirhl2 27042 |
. . . . 5
⊢ (𝜑 → 𝐴((hlG‘𝐺)‘𝐵)(((pInvG‘𝐺)‘𝐵)‘𝑋)) |
70 | 1, 2, 3, 4, 32, 8,
10, 32, 8, 10, 64, 61, 69 | cgrahl1 27177 |
. . . 4
⊢ (𝜑 →
〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrA‘𝐺)〈“𝐴𝐵𝐶”〉) |
71 | 1, 2, 4, 3, 32, 8,
10, 61, 8, 10, 70, 44, 14, 16, 62 | cgratr 27184 |
. . 3
⊢ (𝜑 →
〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
72 | 1, 2, 3, 4, 32, 8,
10, 44, 14, 16 | iscgra 27170 |
. . 3
⊢ (𝜑 →
(〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉 ↔ ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹))) |
73 | 71, 72 | mpbid 231 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 (〈“(((pInvG‘𝐺)‘𝐵)‘𝑋)𝐵𝐶”〉(cgrG‘𝐺)〈“𝑥𝐸𝑦”〉 ∧ 𝑥((hlG‘𝐺)‘𝐸)𝐷 ∧ 𝑦((hlG‘𝐺)‘𝐸)𝐹)) |
74 | 60, 73 | r19.29vva 3266 |
1
⊢ (𝜑 → 〈“𝑋𝐵𝐶”〉(cgrA‘𝐺)〈“𝑌𝐸𝐹”〉) |