MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfcgra2 Structured version   Visualization version   GIF version

Theorem dfcgra2 28853
Description: This is the full statement of definition 11.2 of [Schwabhauser] p. 95. This proof serves to confirm that the definition we have chosen, df-cgra 28831 is indeed equivalent to the textbook's definition. (Contributed by Thierry Arnoux, 2-Aug-2020.)
Hypotheses
Ref Expression
dfcgra2.p 𝑃 = (Base‘𝐺)
dfcgra2.i 𝐼 = (Itv‘𝐺)
dfcgra2.m = (dist‘𝐺)
dfcgra2.g (𝜑𝐺 ∈ TarskiG)
dfcgra2.a (𝜑𝐴𝑃)
dfcgra2.b (𝜑𝐵𝑃)
dfcgra2.c (𝜑𝐶𝑃)
dfcgra2.d (𝜑𝐷𝑃)
dfcgra2.e (𝜑𝐸𝑃)
dfcgra2.f (𝜑𝐹𝑃)
Assertion
Ref Expression
dfcgra2 (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))))
Distinct variable groups:   ,𝑎,𝑐,𝑑,𝑓   𝐴,𝑎,𝑐,𝑑,𝑓   𝐵,𝑎,𝑐,𝑑,𝑓   𝐶,𝑎,𝑐,𝑑,𝑓   𝐷,𝑎,𝑐,𝑑,𝑓   𝐸,𝑎,𝑐,𝑑,𝑓   𝐹,𝑎,𝑐,𝑑,𝑓   𝐺,𝑎,𝑐,𝑑,𝑓   𝐼,𝑎,𝑐,𝑑,𝑓   𝑃,𝑎,𝑐,𝑑,𝑓   𝜑,𝑎,𝑐,𝑑,𝑓

Proof of Theorem dfcgra2
Dummy variables 𝑡 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfcgra2.p . . . . 5 𝑃 = (Base‘𝐺)
2 dfcgra2.i . . . . 5 𝐼 = (Itv‘𝐺)
3 eqid 2735 . . . . 5 (hlG‘𝐺) = (hlG‘𝐺)
4 dfcgra2.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
54adantr 480 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐺 ∈ TarskiG)
6 dfcgra2.a . . . . . 6 (𝜑𝐴𝑃)
76adantr 480 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴𝑃)
8 dfcgra2.b . . . . . 6 (𝜑𝐵𝑃)
98adantr 480 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵𝑃)
10 dfcgra2.c . . . . . 6 (𝜑𝐶𝑃)
1110adantr 480 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶𝑃)
12 dfcgra2.d . . . . . 6 (𝜑𝐷𝑃)
1312adantr 480 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷𝑃)
14 dfcgra2.e . . . . . 6 (𝜑𝐸𝑃)
1514adantr 480 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝑃)
16 dfcgra2.f . . . . . 6 (𝜑𝐹𝑃)
1716adantr 480 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹𝑃)
18 simpr 484 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
191, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane1 28835 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴𝐵)
201, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane2 28836 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵𝐶)
2120necomd 2994 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶𝐵)
2219, 21jca 511 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐴𝐵𝐶𝐵))
231, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane3 28837 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝐷)
2423necomd 2994 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷𝐸)
251, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane4 28838 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝐹)
2625necomd 2994 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹𝐸)
2724, 26jca 511 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐷𝐸𝐹𝐸))
28 simprl 771 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
29 simprr 773 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
304ad6antr 736 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐺 ∈ TarskiG)
31 simp-5r 786 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎𝑃)
328ad6antr 736 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑃)
33 simp-4r 784 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐𝑃)
34 simpllr 776 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑑𝑃)
3514ad6antr 736 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑃)
36 simplr 769 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑓𝑃)
3716ad6antr 736 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹𝑃)
3812ad6antr 736 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷𝑃)
3910ad6antr 736 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶𝑃)
406ad6antr 736 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴𝑃)
41 simp-6r 788 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
421, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41cgracom 28845 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
4328simplld 768 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴 ∈ (𝐵𝐼𝑎))
44 dfcgra2.m . . . . . . . . . . . . . . . . . 18 = (dist‘𝐺)
4519ad5antr 734 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴𝐵)
461, 44, 2, 30, 32, 40, 31, 43, 45tgbtwnne 28513 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑎)
471, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45btwnhl1 28635 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴((hlG‘𝐺)‘𝐵)𝑎)
481, 2, 3, 40, 31, 32, 30, 47hlcomd 28627 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝐴)
491, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48cgrahl1 28839 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝐶”⟩)
5028simprld 772 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶 ∈ (𝐵𝐼𝑐))
5121ad5antr 734 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶𝐵)
521, 44, 2, 30, 32, 39, 33, 50, 51tgbtwnne 28513 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑐)
531, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51btwnhl1 28635 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶((hlG‘𝐺)‘𝐵)𝑐)
541, 2, 3, 39, 33, 32, 30, 53hlcomd 28627 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝐶)
551, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54cgrahl2 28840 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝑐”⟩)
561, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55cgracom 28845 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
5729simplld 768 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷 ∈ (𝐸𝐼𝑑))
5824ad5antr 734 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷𝐸)
591, 44, 2, 30, 35, 38, 34, 57, 58tgbtwnne 28513 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑑)
601, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58btwnhl1 28635 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷((hlG‘𝐺)‘𝐸)𝑑)
611, 2, 3, 38, 34, 35, 30, 60hlcomd 28627 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑑((hlG‘𝐺)‘𝐸)𝐷)
621, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61cgrahl1 28839 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝐹”⟩)
6329simprld 772 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹 ∈ (𝐸𝐼𝑓))
6426ad5antr 734 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹𝐸)
651, 44, 2, 30, 35, 37, 36, 63, 64tgbtwnne 28513 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑓)
661, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64btwnhl1 28635 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹((hlG‘𝐺)‘𝐸)𝑓)
671, 2, 3, 37, 36, 35, 30, 66hlcomd 28627 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑓((hlG‘𝐺)‘𝐸)𝐹)
681, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67cgrahl2 28840 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝑓”⟩)
6946necomd 2994 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎𝐵)
701, 2, 3, 31, 40, 32, 30, 69hlid 28632 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝑎)
7152necomd 2994 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐𝐵)
721, 2, 3, 33, 40, 32, 30, 71hlid 28632 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝑐)
731, 44, 2, 30, 32, 40, 31, 43tgbtwncom 28511 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴 ∈ (𝑎𝐼𝐵))
7428simplrd 770 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐴 𝑎) = (𝐸 𝐷))
751, 44, 2, 30, 40, 31, 35, 38, 74tgcgrcoml 28502 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝐴) = (𝐸 𝐷))
7629simplrd 770 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐷 𝑑) = (𝐵 𝐴))
7776eqcomd 2741 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝐴) = (𝐷 𝑑))
781, 44, 2, 30, 32, 40, 38, 34, 77tgcgrcoml 28502 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐴 𝐵) = (𝐷 𝑑))
791, 44, 2, 30, 31, 40, 32, 35, 38, 34, 73, 57, 75, 78tgcgrextend 28508 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝐵) = (𝐸 𝑑))
801, 44, 2, 30, 31, 32, 35, 34, 79tgcgrcoml 28502 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝑎) = (𝐸 𝑑))
811, 44, 2, 30, 32, 39, 33, 50tgbtwncom 28511 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶 ∈ (𝑐𝐼𝐵))
8228simprrd 774 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐶 𝑐) = (𝐸 𝐹))
831, 44, 2, 30, 39, 33, 35, 37, 82tgcgrcoml 28502 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑐 𝐶) = (𝐸 𝐹))
8429simprrd 774 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐹 𝑓) = (𝐵 𝐶))
8584eqcomd 2741 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝐶) = (𝐹 𝑓))
861, 44, 2, 30, 32, 39, 37, 36, 85tgcgrcoml 28502 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐶 𝐵) = (𝐹 𝑓))
871, 44, 2, 30, 33, 39, 32, 35, 37, 36, 81, 63, 83, 86tgcgrextend 28508 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑐 𝐵) = (𝐸 𝑓))
881, 44, 2, 30, 33, 32, 35, 36, 87tgcgrcoml 28502 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝑐) = (𝐸 𝑓))
891, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 72, 80, 88cgracgr 28841 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝑐) = (𝑑 𝑓))
9028, 29, 893jca 1127 . . . . . . . 8 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
9190ex 412 . . . . . . 7 ((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9291reximdva 3166 . . . . . 6 (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → (∃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → ∃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9392reximdva 3166 . . . . 5 ((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9493imp 406 . . . 4 (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
951, 44, 2, 4, 8, 6, 14, 12axtgsegcon 28487 . . . . . . . 8 (𝜑 → ∃𝑎𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)))
961, 44, 2, 4, 8, 10, 14, 16axtgsegcon 28487 . . . . . . . 8 (𝜑 → ∃𝑐𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))
97 reeanv 3227 . . . . . . . 8 (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ (∃𝑎𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ ∃𝑐𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
9895, 96, 97sylanbrc 583 . . . . . . 7 (𝜑 → ∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
991, 44, 2, 4, 14, 12, 8, 6axtgsegcon 28487 . . . . . . . 8 (𝜑 → ∃𝑑𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)))
1001, 44, 2, 4, 14, 16, 8, 10axtgsegcon 28487 . . . . . . . 8 (𝜑 → ∃𝑓𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))
101 reeanv 3227 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ (∃𝑑𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ ∃𝑓𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
10299, 100, 101sylanbrc 583 . . . . . . 7 (𝜑 → ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
10398, 102jca 511 . . . . . 6 (𝜑 → (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
104 r19.41vv 3225 . . . . . . . . 9 (∃𝑑𝑃𝑓𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))))
105 ancom 460 . . . . . . . . . 10 ((((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
1061052rexbii 3127 . . . . . . . . 9 (∃𝑑𝑃𝑓𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
107 ancom 460 . . . . . . . . 9 ((∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
108104, 106, 1073bitr3i 301 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
1091082rexbii 3127 . . . . . . 7 (∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ ∃𝑎𝑃𝑐𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
110 r19.41vv 3225 . . . . . . 7 (∃𝑎𝑃𝑐𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
111109, 110bitr2i 276 . . . . . 6 ((∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
112103, 111sylib 218 . . . . 5 (𝜑 → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
113112adantr 480 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
11494, 113reximddv2 3213 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
11522, 27, 1143jca 1127 . 2 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
116 df-3an 1088 . . 3 (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) ↔ (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
1174ad6antr 736 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐺 ∈ TarskiG)
11812ad6antr 736 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷𝑃)
11914ad6antr 736 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑃)
12016ad6antr 736 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹𝑃)
1216ad6antr 736 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴𝑃)
1228ad6antr 736 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑃)
12310ad6antr 736 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶𝑃)
124 simp-4r 784 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑦𝑃)
125 simp-5r 786 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑥𝑃)
126 simpllr 776 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑧𝑃)
127 simplr 769 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑡𝑃)
128 eqid 2735 . . . . . . . . . . . . . 14 (cgrG‘𝐺) = (cgrG‘𝐺)
129 simpr1 1193 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))))
130129simplld 768 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴 ∈ (𝐵𝐼𝑥))
131 simpr2 1194 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))))
132131simplld 768 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷 ∈ (𝐸𝐼𝑧))
1331, 44, 2, 117, 119, 118, 126, 132tgbtwncom 28511 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷 ∈ (𝑧𝐼𝐸))
134131simplrd 770 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐷 𝑧) = (𝐵 𝐴))
135134eqcomd 2741 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐴) = (𝐷 𝑧))
1361, 44, 2, 117, 122, 121, 118, 126, 135tgcgrcomr 28501 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐴) = (𝑧 𝐷))
137129simplrd 770 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐴 𝑥) = (𝐸 𝐷))
1381, 44, 2, 117, 121, 125, 119, 118, 137tgcgrcomr 28501 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐴 𝑥) = (𝐷 𝐸))
1391, 44, 2, 117, 122, 121, 125, 126, 118, 119, 130, 133, 136, 138tgcgrextend 28508 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝑥) = (𝑧 𝐸))
1401, 44, 2, 117, 122, 125, 126, 119, 139tgcgrcoml 28502 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑥 𝐵) = (𝑧 𝐸))
141129simprld 772 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶 ∈ (𝐵𝐼𝑦))
1421, 44, 2, 117, 122, 123, 124, 141tgbtwncom 28511 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶 ∈ (𝑦𝐼𝐵))
143131simprld 772 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹 ∈ (𝐸𝐼𝑡))
144129simprrd 774 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐶 𝑦) = (𝐸 𝐹))
1451, 44, 2, 117, 123, 124, 119, 120, 144tgcgrcoml 28502 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝐶) = (𝐸 𝐹))
146131simprrd 774 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐹 𝑡) = (𝐵 𝐶))
147146eqcomd 2741 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐶) = (𝐹 𝑡))
1481, 44, 2, 117, 122, 123, 120, 127, 147tgcgrcoml 28502 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐶 𝐵) = (𝐹 𝑡))
1491, 44, 2, 117, 124, 123, 122, 119, 120, 127, 142, 143, 145, 148tgcgrextend 28508 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝐵) = (𝐸 𝑡))
1501, 44, 2, 117, 124, 122, 119, 127, 149tgcgrcoml 28502 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝑦) = (𝐸 𝑡))
151 simpr3 1195 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑥 𝑦) = (𝑧 𝑡))
1521, 44, 2, 117, 125, 124, 126, 127, 151tgcgrcomlr 28503 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝑥) = (𝑡 𝑧))
1531, 44, 128, 117, 125, 122, 124, 126, 119, 127, 140, 150, 152trgcgr 28539 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrG‘𝐺)⟨“𝑧𝐸𝑡”⟩)
154 simp-6r 788 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)))
155154simprld 772 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷𝐸)
1561, 44, 2, 117, 119, 118, 126, 132, 155tgbtwnne 28513 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑧)
1571, 2, 3, 119, 126, 118, 117, 122, 132, 156, 155btwnhl1 28635 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷((hlG‘𝐺)‘𝐸)𝑧)
1581, 2, 3, 118, 126, 119, 117, 157hlcomd 28627 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑧((hlG‘𝐺)‘𝐸)𝐷)
159154simprrd 774 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹𝐸)
1601, 44, 2, 117, 119, 120, 127, 143, 159tgbtwnne 28513 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑡)
1611, 2, 3, 119, 127, 120, 117, 122, 143, 160, 159btwnhl1 28635 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹((hlG‘𝐺)‘𝐸)𝑡)
1621, 2, 3, 120, 127, 119, 117, 161hlcomd 28627 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑡((hlG‘𝐺)‘𝐸)𝐹)
1631, 2, 3, 117, 125, 122, 124, 118, 119, 120, 126, 127, 153, 158, 162iscgrad 28834 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
1641, 2, 117, 3, 125, 122, 124, 118, 119, 120, 163cgracom 28845 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑥𝐵𝑦”⟩)
165154simplld 768 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴𝐵)
1661, 44, 2, 117, 122, 121, 125, 130, 165tgbtwnne 28513 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑥)
1671, 2, 3, 122, 125, 121, 117, 121, 130, 166, 165btwnhl1 28635 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴((hlG‘𝐺)‘𝐵)𝑥)
1681, 2, 3, 117, 118, 119, 120, 125, 122, 124, 164, 121, 167cgrahl1 28839 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝑦”⟩)
169154simplrd 770 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶𝐵)
1701, 44, 2, 117, 122, 123, 124, 141, 169tgbtwnne 28513 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑦)
1711, 2, 3, 122, 124, 123, 117, 121, 141, 170, 169btwnhl1 28635 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶((hlG‘𝐺)‘𝐵)𝑦)
1721, 2, 3, 117, 118, 119, 120, 121, 122, 124, 168, 123, 171cgrahl2 28840 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
1731, 2, 117, 3, 118, 119, 120, 121, 122, 123, 172cgracom 28845 . . . . . . . 8 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
174173adantl3r 750 . . . . . . 7 ((((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
175 simpr 484 . . . . . . . 8 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
176 oveq2 7439 . . . . . . . . . . . . 13 (𝑑 = 𝑧 → (𝐸𝐼𝑑) = (𝐸𝐼𝑧))
177176eleq2d 2825 . . . . . . . . . . . 12 (𝑑 = 𝑧 → (𝐷 ∈ (𝐸𝐼𝑑) ↔ 𝐷 ∈ (𝐸𝐼𝑧)))
178 oveq2 7439 . . . . . . . . . . . . 13 (𝑑 = 𝑧 → (𝐷 𝑑) = (𝐷 𝑧))
179178eqeq1d 2737 . . . . . . . . . . . 12 (𝑑 = 𝑧 → ((𝐷 𝑑) = (𝐵 𝐴) ↔ (𝐷 𝑧) = (𝐵 𝐴)))
180177, 179anbi12d 632 . . . . . . . . . . 11 (𝑑 = 𝑧 → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴))))
181180anbi1d 631 . . . . . . . . . 10 (𝑑 = 𝑧 → (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
182 oveq1 7438 . . . . . . . . . . 11 (𝑑 = 𝑧 → (𝑑 𝑓) = (𝑧 𝑓))
183182eqeq2d 2746 . . . . . . . . . 10 (𝑑 = 𝑧 → ((𝑥 𝑦) = (𝑑 𝑓) ↔ (𝑥 𝑦) = (𝑧 𝑓)))
184181, 1833anbi23d 1438 . . . . . . . . 9 (𝑑 = 𝑧 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑓))))
185 oveq2 7439 . . . . . . . . . . . . 13 (𝑓 = 𝑡 → (𝐸𝐼𝑓) = (𝐸𝐼𝑡))
186185eleq2d 2825 . . . . . . . . . . . 12 (𝑓 = 𝑡 → (𝐹 ∈ (𝐸𝐼𝑓) ↔ 𝐹 ∈ (𝐸𝐼𝑡)))
187 oveq2 7439 . . . . . . . . . . . . 13 (𝑓 = 𝑡 → (𝐹 𝑓) = (𝐹 𝑡))
188187eqeq1d 2737 . . . . . . . . . . . 12 (𝑓 = 𝑡 → ((𝐹 𝑓) = (𝐵 𝐶) ↔ (𝐹 𝑡) = (𝐵 𝐶)))
189186, 188anbi12d 632 . . . . . . . . . . 11 (𝑓 = 𝑡 → ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)) ↔ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))))
190189anbi2d 630 . . . . . . . . . 10 (𝑓 = 𝑡 → (((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶)))))
191 oveq2 7439 . . . . . . . . . . 11 (𝑓 = 𝑡 → (𝑧 𝑓) = (𝑧 𝑡))
192191eqeq2d 2746 . . . . . . . . . 10 (𝑓 = 𝑡 → ((𝑥 𝑦) = (𝑧 𝑓) ↔ (𝑥 𝑦) = (𝑧 𝑡)))
193190, 1923anbi23d 1438 . . . . . . . . 9 (𝑓 = 𝑡 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))))
194184, 193cbvrex2vw 3240 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)) ↔ ∃𝑧𝑃𝑡𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡)))
195175, 194sylib 218 . . . . . . 7 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ∃𝑧𝑃𝑡𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡)))
196174, 195r19.29vva 3214 . . . . . 6 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
197196adantl3r 750 . . . . 5 ((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
198 simpr 484 . . . . . 6 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
199 oveq2 7439 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝐵𝐼𝑎) = (𝐵𝐼𝑥))
200199eleq2d 2825 . . . . . . . . . . 11 (𝑎 = 𝑥 → (𝐴 ∈ (𝐵𝐼𝑎) ↔ 𝐴 ∈ (𝐵𝐼𝑥)))
201 oveq2 7439 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝐴 𝑎) = (𝐴 𝑥))
202201eqeq1d 2737 . . . . . . . . . . 11 (𝑎 = 𝑥 → ((𝐴 𝑎) = (𝐸 𝐷) ↔ (𝐴 𝑥) = (𝐸 𝐷)))
203200, 202anbi12d 632 . . . . . . . . . 10 (𝑎 = 𝑥 → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ↔ (𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷))))
204203anbi1d 631 . . . . . . . . 9 (𝑎 = 𝑥 → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))))
205 oveq1 7438 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑎 𝑐) = (𝑥 𝑐))
206205eqeq1d 2737 . . . . . . . . 9 (𝑎 = 𝑥 → ((𝑎 𝑐) = (𝑑 𝑓) ↔ (𝑥 𝑐) = (𝑑 𝑓)))
207204, 2063anbi13d 1437 . . . . . . . 8 (𝑎 = 𝑥 → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓))))
2082072rexbidv 3220 . . . . . . 7 (𝑎 = 𝑥 → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓))))
209 oveq2 7439 . . . . . . . . . . . 12 (𝑐 = 𝑦 → (𝐵𝐼𝑐) = (𝐵𝐼𝑦))
210209eleq2d 2825 . . . . . . . . . . 11 (𝑐 = 𝑦 → (𝐶 ∈ (𝐵𝐼𝑐) ↔ 𝐶 ∈ (𝐵𝐼𝑦)))
211 oveq2 7439 . . . . . . . . . . . 12 (𝑐 = 𝑦 → (𝐶 𝑐) = (𝐶 𝑦))
212211eqeq1d 2737 . . . . . . . . . . 11 (𝑐 = 𝑦 → ((𝐶 𝑐) = (𝐸 𝐹) ↔ (𝐶 𝑦) = (𝐸 𝐹)))
213210, 212anbi12d 632 . . . . . . . . . 10 (𝑐 = 𝑦 → ((𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)) ↔ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))))
214213anbi2d 630 . . . . . . . . 9 (𝑐 = 𝑦 → (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹)))))
215 oveq2 7439 . . . . . . . . . 10 (𝑐 = 𝑦 → (𝑥 𝑐) = (𝑥 𝑦))
216215eqeq1d 2737 . . . . . . . . 9 (𝑐 = 𝑦 → ((𝑥 𝑐) = (𝑑 𝑓) ↔ (𝑥 𝑦) = (𝑑 𝑓)))
217214, 2163anbi13d 1437 . . . . . . . 8 (𝑐 = 𝑦 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))))
2182172rexbidv 3220 . . . . . . 7 (𝑐 = 𝑦 → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓)) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))))
219208, 218cbvrex2vw 3240 . . . . . 6 (∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ ∃𝑥𝑃𝑦𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
220198, 219sylib 218 . . . . 5 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ∃𝑥𝑃𝑦𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
221197, 220r19.29vva 3214 . . . 4 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
222221anasss 466 . . 3 ((𝜑 ∧ (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
223116, 222sylan2b 594 . 2 ((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
224115, 223impbida 801 1 (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wne 2938  wrex 3068   class class class wbr 5148  cfv 6563  (class class class)co 7431  ⟨“cs3 14878  Basecbs 17245  distcds 17307  TarskiGcstrkg 28450  Itvcitv 28456  cgrGccgrg 28533  hlGchlg 28623  cgrAccgra 28830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-oadd 8509  df-er 8744  df-map 8867  df-pm 8868  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-dju 9939  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-xnn0 12598  df-z 12612  df-uz 12877  df-fz 13545  df-fzo 13692  df-hash 14367  df-word 14550  df-concat 14606  df-s1 14631  df-s2 14884  df-s3 14885  df-trkgc 28471  df-trkgb 28472  df-trkgcb 28473  df-trkg 28476  df-cgrg 28534  df-leg 28606  df-hlg 28624  df-cgra 28831
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator