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

Theorem dfcgra2 27187
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 27165 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 2740 . . . . 5 (hlG‘𝐺) = (hlG‘𝐺)
4 dfcgra2.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
54adantr 481 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐺 ∈ TarskiG)
6 dfcgra2.a . . . . . 6 (𝜑𝐴𝑃)
76adantr 481 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴𝑃)
8 dfcgra2.b . . . . . 6 (𝜑𝐵𝑃)
98adantr 481 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵𝑃)
10 dfcgra2.c . . . . . 6 (𝜑𝐶𝑃)
1110adantr 481 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶𝑃)
12 dfcgra2.d . . . . . 6 (𝜑𝐷𝑃)
1312adantr 481 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷𝑃)
14 dfcgra2.e . . . . . 6 (𝜑𝐸𝑃)
1514adantr 481 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝑃)
16 dfcgra2.f . . . . . 6 (𝜑𝐹𝑃)
1716adantr 481 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹𝑃)
18 simpr 485 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
191, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane1 27169 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐴𝐵)
201, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane2 27170 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐵𝐶)
2120necomd 3001 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐶𝐵)
2219, 21jca 512 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐴𝐵𝐶𝐵))
231, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane3 27171 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝐷)
2423necomd 3001 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐷𝐸)
251, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane4 27172 . . . . 5 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐸𝐹)
2625necomd 3001 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → 𝐹𝐸)
2724, 26jca 512 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → (𝐷𝐸𝐹𝐸))
28 simprl 768 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
29 simprr 770 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
304ad6antr 733 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐺 ∈ TarskiG)
31 simp-5r 783 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎𝑃)
328ad6antr 733 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑃)
33 simp-4r 781 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐𝑃)
34 simpllr 773 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑑𝑃)
3514ad6antr 733 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑃)
36 simplr 766 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑓𝑃)
3716ad6antr 733 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹𝑃)
3812ad6antr 733 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷𝑃)
3910ad6antr 733 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶𝑃)
406ad6antr 733 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴𝑃)
41 simp-6r 785 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
421, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41cgracom 27179 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
4328simplld 765 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴 ∈ (𝐵𝐼𝑎))
44 dfcgra2.m . . . . . . . . . . . . . . . . . 18 = (dist‘𝐺)
4519ad5antr 731 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴𝐵)
461, 44, 2, 30, 32, 40, 31, 43, 45tgbtwnne 26847 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑎)
471, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45btwnhl1 26969 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴((hlG‘𝐺)‘𝐵)𝑎)
481, 2, 3, 40, 31, 32, 30, 47hlcomd 26961 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝐴)
491, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48cgrahl1 27173 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝐶”⟩)
5028simprld 769 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶 ∈ (𝐵𝐼𝑐))
5121ad5antr 731 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶𝐵)
521, 44, 2, 30, 32, 39, 33, 50, 51tgbtwnne 26847 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐵𝑐)
531, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51btwnhl1 26969 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶((hlG‘𝐺)‘𝐵)𝑐)
541, 2, 3, 39, 33, 32, 30, 53hlcomd 26961 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝐶)
551, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54cgrahl2 27174 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑎𝐵𝑐”⟩)
561, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55cgracom 27179 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
5729simplld 765 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷 ∈ (𝐸𝐼𝑑))
5824ad5antr 731 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷𝐸)
591, 44, 2, 30, 35, 38, 34, 57, 58tgbtwnne 26847 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑑)
601, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58btwnhl1 26969 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐷((hlG‘𝐺)‘𝐸)𝑑)
611, 2, 3, 38, 34, 35, 30, 60hlcomd 26961 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑑((hlG‘𝐺)‘𝐸)𝐷)
621, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61cgrahl1 27173 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝐹”⟩)
6329simprld 769 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹 ∈ (𝐸𝐼𝑓))
6426ad5antr 731 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹𝐸)
651, 44, 2, 30, 35, 37, 36, 63, 64tgbtwnne 26847 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐸𝑓)
661, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64btwnhl1 26969 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐹((hlG‘𝐺)‘𝐸)𝑓)
671, 2, 3, 37, 36, 35, 30, 66hlcomd 26961 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑓((hlG‘𝐺)‘𝐸)𝐹)
681, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67cgrahl2 27174 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ⟨“𝑎𝐵𝑐”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝑓”⟩)
6946necomd 3001 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎𝐵)
701, 2, 3, 31, 40, 32, 30, 69hlid 26966 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑎((hlG‘𝐺)‘𝐵)𝑎)
7152necomd 3001 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐𝐵)
721, 2, 3, 33, 40, 32, 30, 71hlid 26966 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝑐((hlG‘𝐺)‘𝐵)𝑐)
731, 44, 2, 30, 32, 40, 31, 43tgbtwncom 26845 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐴 ∈ (𝑎𝐼𝐵))
7428simplrd 767 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐴 𝑎) = (𝐸 𝐷))
751, 44, 2, 30, 40, 31, 35, 38, 74tgcgrcoml 26836 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝐴) = (𝐸 𝐷))
7629simplrd 767 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐷 𝑑) = (𝐵 𝐴))
7776eqcomd 2746 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝐴) = (𝐷 𝑑))
781, 44, 2, 30, 32, 40, 38, 34, 77tgcgrcoml 26836 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐴 𝐵) = (𝐷 𝑑))
791, 44, 2, 30, 31, 40, 32, 35, 38, 34, 73, 57, 75, 78tgcgrextend 26842 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝐵) = (𝐸 𝑑))
801, 44, 2, 30, 31, 32, 35, 34, 79tgcgrcoml 26836 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝑎) = (𝐸 𝑑))
811, 44, 2, 30, 32, 39, 33, 50tgbtwncom 26845 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → 𝐶 ∈ (𝑐𝐼𝐵))
8228simprrd 771 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐶 𝑐) = (𝐸 𝐹))
831, 44, 2, 30, 39, 33, 35, 37, 82tgcgrcoml 26836 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑐 𝐶) = (𝐸 𝐹))
8429simprrd 771 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐹 𝑓) = (𝐵 𝐶))
8584eqcomd 2746 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝐶) = (𝐹 𝑓))
861, 44, 2, 30, 32, 39, 37, 36, 85tgcgrcoml 26836 . . . . . . . . . . . 12 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐶 𝐵) = (𝐹 𝑓))
871, 44, 2, 30, 33, 39, 32, 35, 37, 36, 81, 63, 83, 86tgcgrextend 26842 . . . . . . . . . . 11 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑐 𝐵) = (𝐸 𝑓))
881, 44, 2, 30, 33, 32, 35, 36, 87tgcgrcoml 26836 . . . . . . . . . 10 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝐵 𝑐) = (𝐸 𝑓))
891, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 72, 80, 88cgracgr 27175 . . . . . . . . 9 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (𝑎 𝑐) = (𝑑 𝑓))
9028, 29, 893jca 1127 . . . . . . . 8 (((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
9190ex 413 . . . . . . 7 ((((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) ∧ 𝑓𝑃) → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9291reximdva 3205 . . . . . 6 (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ 𝑑𝑃) → (∃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → ∃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9392reximdva 3205 . . . . 5 ((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
9493imp 407 . . . 4 (((((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) ∧ 𝑎𝑃) ∧ 𝑐𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
951, 44, 2, 4, 8, 6, 14, 12axtgsegcon 26821 . . . . . . . 8 (𝜑 → ∃𝑎𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)))
961, 44, 2, 4, 8, 10, 14, 16axtgsegcon 26821 . . . . . . . 8 (𝜑 → ∃𝑐𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))
97 reeanv 3295 . . . . . . . 8 (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ (∃𝑎𝑃 (𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ ∃𝑐𝑃 (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
9895, 96, 97sylanbrc 583 . . . . . . 7 (𝜑 → ∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))))
991, 44, 2, 4, 14, 12, 8, 6axtgsegcon 26821 . . . . . . . 8 (𝜑 → ∃𝑑𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)))
1001, 44, 2, 4, 14, 16, 8, 10axtgsegcon 26821 . . . . . . . 8 (𝜑 → ∃𝑓𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))
101 reeanv 3295 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ (∃𝑑𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ ∃𝑓𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
10299, 100, 101sylanbrc 583 . . . . . . 7 (𝜑 → ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))))
10398, 102jca 512 . . . . . 6 (𝜑 → (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
104 r19.41vv 3278 . . . . . . . . 9 (∃𝑑𝑃𝑓𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))))
105 ancom 461 . . . . . . . . . 10 ((((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
1061052rexbii 3181 . . . . . . . . 9 (∃𝑑𝑃𝑓𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
107 ancom 461 . . . . . . . . 9 ((∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
108104, 106, 1073bitr3i 301 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
1091082rexbii 3181 . . . . . . 7 (∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ ∃𝑎𝑃𝑐𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
110 r19.41vv 3278 . . . . . . 7 (∃𝑎𝑃𝑐𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ (∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
111109, 110bitr2i 275 . . . . . 6 ((∃𝑎𝑃𝑐𝑃 ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ∃𝑑𝑃𝑓𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))) ↔ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
112103, 111sylib 217 . . . . 5 (𝜑 → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
113112adantr 481 . . . 4 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
11494, 113reximddv2 3209 . . 3 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
11522, 27, 1143jca 1127 . 2 ((𝜑 ∧ ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩) → ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
116 df-3an 1088 . . 3 (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) ↔ (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))))
1174ad6antr 733 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐺 ∈ TarskiG)
11812ad6antr 733 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷𝑃)
11914ad6antr 733 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑃)
12016ad6antr 733 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹𝑃)
1216ad6antr 733 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴𝑃)
1228ad6antr 733 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑃)
12310ad6antr 733 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶𝑃)
124 simp-4r 781 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑦𝑃)
125 simp-5r 783 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑥𝑃)
126 simpllr 773 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑧𝑃)
127 simplr 766 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑡𝑃)
128 eqid 2740 . . . . . . . . . . . . . 14 (cgrG‘𝐺) = (cgrG‘𝐺)
129 simpr1 1193 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))))
130129simplld 765 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴 ∈ (𝐵𝐼𝑥))
131 simpr2 1194 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))))
132131simplld 765 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷 ∈ (𝐸𝐼𝑧))
1331, 44, 2, 117, 119, 118, 126, 132tgbtwncom 26845 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷 ∈ (𝑧𝐼𝐸))
134131simplrd 767 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐷 𝑧) = (𝐵 𝐴))
135134eqcomd 2746 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐴) = (𝐷 𝑧))
1361, 44, 2, 117, 122, 121, 118, 126, 135tgcgrcomr 26835 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐴) = (𝑧 𝐷))
137129simplrd 767 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐴 𝑥) = (𝐸 𝐷))
1381, 44, 2, 117, 121, 125, 119, 118, 137tgcgrcomr 26835 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐴 𝑥) = (𝐷 𝐸))
1391, 44, 2, 117, 122, 121, 125, 126, 118, 119, 130, 133, 136, 138tgcgrextend 26842 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝑥) = (𝑧 𝐸))
1401, 44, 2, 117, 122, 125, 126, 119, 139tgcgrcoml 26836 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑥 𝐵) = (𝑧 𝐸))
141129simprld 769 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶 ∈ (𝐵𝐼𝑦))
1421, 44, 2, 117, 122, 123, 124, 141tgbtwncom 26845 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶 ∈ (𝑦𝐼𝐵))
143131simprld 769 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹 ∈ (𝐸𝐼𝑡))
144129simprrd 771 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐶 𝑦) = (𝐸 𝐹))
1451, 44, 2, 117, 123, 124, 119, 120, 144tgcgrcoml 26836 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝐶) = (𝐸 𝐹))
146131simprrd 771 . . . . . . . . . . . . . . . . . 18 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐹 𝑡) = (𝐵 𝐶))
147146eqcomd 2746 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝐶) = (𝐹 𝑡))
1481, 44, 2, 117, 122, 123, 120, 127, 147tgcgrcoml 26836 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐶 𝐵) = (𝐹 𝑡))
1491, 44, 2, 117, 124, 123, 122, 119, 120, 127, 142, 143, 145, 148tgcgrextend 26842 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝐵) = (𝐸 𝑡))
1501, 44, 2, 117, 124, 122, 119, 127, 149tgcgrcoml 26836 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝐵 𝑦) = (𝐸 𝑡))
151 simpr3 1195 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑥 𝑦) = (𝑧 𝑡))
1521, 44, 2, 117, 125, 124, 126, 127, 151tgcgrcomlr 26837 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → (𝑦 𝑥) = (𝑡 𝑧))
1531, 44, 128, 117, 125, 122, 124, 126, 119, 127, 140, 150, 152trgcgr 26873 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrG‘𝐺)⟨“𝑧𝐸𝑡”⟩)
154 simp-6r 785 . . . . . . . . . . . . . . . . 17 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)))
155154simprld 769 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷𝐸)
1561, 44, 2, 117, 119, 118, 126, 132, 155tgbtwnne 26847 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑧)
1571, 2, 3, 119, 126, 118, 117, 122, 132, 156, 155btwnhl1 26969 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐷((hlG‘𝐺)‘𝐸)𝑧)
1581, 2, 3, 118, 126, 119, 117, 157hlcomd 26961 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑧((hlG‘𝐺)‘𝐸)𝐷)
159154simprrd 771 . . . . . . . . . . . . . . . 16 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹𝐸)
1601, 44, 2, 117, 119, 120, 127, 143, 159tgbtwnne 26847 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐸𝑡)
1611, 2, 3, 119, 127, 120, 117, 122, 143, 160, 159btwnhl1 26969 . . . . . . . . . . . . . 14 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐹((hlG‘𝐺)‘𝐸)𝑡)
1621, 2, 3, 120, 127, 119, 117, 161hlcomd 26961 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝑡((hlG‘𝐺)‘𝐸)𝐹)
1631, 2, 3, 117, 125, 122, 124, 118, 119, 120, 126, 127, 153, 158, 162iscgrad 27168 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝑥𝐵𝑦”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
1641, 2, 117, 3, 125, 122, 124, 118, 119, 120, 163cgracom 27179 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝑥𝐵𝑦”⟩)
165154simplld 765 . . . . . . . . . . . . 13 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴𝐵)
1661, 44, 2, 117, 122, 121, 125, 130, 165tgbtwnne 26847 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑥)
1671, 2, 3, 122, 125, 121, 117, 121, 130, 166, 165btwnhl1 26969 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐴((hlG‘𝐺)‘𝐵)𝑥)
1681, 2, 3, 117, 118, 119, 120, 125, 122, 124, 164, 121, 167cgrahl1 27173 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝑦”⟩)
169154simplrd 767 . . . . . . . . . . . 12 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶𝐵)
1701, 44, 2, 117, 122, 123, 124, 141, 169tgbtwnne 26847 . . . . . . . . . . 11 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐵𝑦)
1711, 2, 3, 122, 124, 123, 117, 121, 141, 170, 169btwnhl1 26969 . . . . . . . . . 10 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → 𝐶((hlG‘𝐺)‘𝐵)𝑦)
1721, 2, 3, 117, 118, 119, 120, 121, 122, 124, 168, 123, 171cgrahl2 27174 . . . . . . . . 9 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
1731, 2, 117, 3, 118, 119, 120, 121, 122, 123, 172cgracom 27179 . . . . . . . 8 (((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
174173adantl3r 747 . . . . . . 7 ((((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) ∧ 𝑧𝑃) ∧ 𝑡𝑃) ∧ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
175 simpr 485 . . . . . . . 8 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
176 oveq2 7277 . . . . . . . . . . . . 13 (𝑑 = 𝑧 → (𝐸𝐼𝑑) = (𝐸𝐼𝑧))
177176eleq2d 2826 . . . . . . . . . . . 12 (𝑑 = 𝑧 → (𝐷 ∈ (𝐸𝐼𝑑) ↔ 𝐷 ∈ (𝐸𝐼𝑧)))
178 oveq2 7277 . . . . . . . . . . . . 13 (𝑑 = 𝑧 → (𝐷 𝑑) = (𝐷 𝑧))
179178eqeq1d 2742 . . . . . . . . . . . 12 (𝑑 = 𝑧 → ((𝐷 𝑑) = (𝐵 𝐴) ↔ (𝐷 𝑧) = (𝐵 𝐴)))
180177, 179anbi12d 631 . . . . . . . . . . 11 (𝑑 = 𝑧 → ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴))))
181180anbi1d 630 . . . . . . . . . 10 (𝑑 = 𝑧 → (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)))))
182 oveq1 7276 . . . . . . . . . . 11 (𝑑 = 𝑧 → (𝑑 𝑓) = (𝑧 𝑓))
183182eqeq2d 2751 . . . . . . . . . 10 (𝑑 = 𝑧 → ((𝑥 𝑦) = (𝑑 𝑓) ↔ (𝑥 𝑦) = (𝑧 𝑓)))
184181, 1833anbi23d 1438 . . . . . . . . 9 (𝑑 = 𝑧 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑓))))
185 oveq2 7277 . . . . . . . . . . . . 13 (𝑓 = 𝑡 → (𝐸𝐼𝑓) = (𝐸𝐼𝑡))
186185eleq2d 2826 . . . . . . . . . . . 12 (𝑓 = 𝑡 → (𝐹 ∈ (𝐸𝐼𝑓) ↔ 𝐹 ∈ (𝐸𝐼𝑡)))
187 oveq2 7277 . . . . . . . . . . . . 13 (𝑓 = 𝑡 → (𝐹 𝑓) = (𝐹 𝑡))
188187eqeq1d 2742 . . . . . . . . . . . 12 (𝑓 = 𝑡 → ((𝐹 𝑓) = (𝐵 𝐶) ↔ (𝐹 𝑡) = (𝐵 𝐶)))
189186, 188anbi12d 631 . . . . . . . . . . 11 (𝑓 = 𝑡 → ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶)) ↔ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))))
190189anbi2d 629 . . . . . . . . . 10 (𝑓 = 𝑡 → (((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶)))))
191 oveq2 7277 . . . . . . . . . . 11 (𝑓 = 𝑡 → (𝑧 𝑓) = (𝑧 𝑡))
192191eqeq2d 2751 . . . . . . . . . 10 (𝑓 = 𝑡 → ((𝑥 𝑦) = (𝑧 𝑓) ↔ (𝑥 𝑦) = (𝑧 𝑡)))
193190, 1923anbi23d 1438 . . . . . . . . 9 (𝑓 = 𝑡 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡))))
194184, 193cbvrex2vw 3395 . . . . . . . 8 (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)) ↔ ∃𝑧𝑃𝑡𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡)))
195175, 194sylib 217 . . . . . . 7 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ∃𝑧𝑃𝑡𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 𝑧) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑡) ∧ (𝐹 𝑡) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑧 𝑡)))
196174, 195r19.29vva 3266 . . . . . 6 (((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
197196adantl3r 747 . . . . 5 ((((((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
198 simpr 485 . . . . . 6 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))
199 oveq2 7277 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝐵𝐼𝑎) = (𝐵𝐼𝑥))
200199eleq2d 2826 . . . . . . . . . . 11 (𝑎 = 𝑥 → (𝐴 ∈ (𝐵𝐼𝑎) ↔ 𝐴 ∈ (𝐵𝐼𝑥)))
201 oveq2 7277 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝐴 𝑎) = (𝐴 𝑥))
202201eqeq1d 2742 . . . . . . . . . . 11 (𝑎 = 𝑥 → ((𝐴 𝑎) = (𝐸 𝐷) ↔ (𝐴 𝑥) = (𝐸 𝐷)))
203200, 202anbi12d 631 . . . . . . . . . 10 (𝑎 = 𝑥 → ((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ↔ (𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷))))
204203anbi1d 630 . . . . . . . . 9 (𝑎 = 𝑥 → (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)))))
205 oveq1 7276 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑎 𝑐) = (𝑥 𝑐))
206205eqeq1d 2742 . . . . . . . . 9 (𝑎 = 𝑥 → ((𝑎 𝑐) = (𝑑 𝑓) ↔ (𝑥 𝑐) = (𝑑 𝑓)))
207204, 2063anbi13d 1437 . . . . . . . 8 (𝑎 = 𝑥 → ((((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓))))
2082072rexbidv 3231 . . . . . . 7 (𝑎 = 𝑥 → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓))))
209 oveq2 7277 . . . . . . . . . . . 12 (𝑐 = 𝑦 → (𝐵𝐼𝑐) = (𝐵𝐼𝑦))
210209eleq2d 2826 . . . . . . . . . . 11 (𝑐 = 𝑦 → (𝐶 ∈ (𝐵𝐼𝑐) ↔ 𝐶 ∈ (𝐵𝐼𝑦)))
211 oveq2 7277 . . . . . . . . . . . 12 (𝑐 = 𝑦 → (𝐶 𝑐) = (𝐶 𝑦))
212211eqeq1d 2742 . . . . . . . . . . 11 (𝑐 = 𝑦 → ((𝐶 𝑐) = (𝐸 𝐹) ↔ (𝐶 𝑦) = (𝐸 𝐹)))
213210, 212anbi12d 631 . . . . . . . . . 10 (𝑐 = 𝑦 → ((𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹)) ↔ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))))
214213anbi2d 629 . . . . . . . . 9 (𝑐 = 𝑦 → (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ↔ ((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹)))))
215 oveq2 7277 . . . . . . . . . 10 (𝑐 = 𝑦 → (𝑥 𝑐) = (𝑥 𝑦))
216215eqeq1d 2742 . . . . . . . . 9 (𝑐 = 𝑦 → ((𝑥 𝑐) = (𝑑 𝑓) ↔ (𝑥 𝑦) = (𝑑 𝑓)))
217214, 2163anbi13d 1437 . . . . . . . 8 (𝑐 = 𝑦 → ((((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓)) ↔ (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))))
2182172rexbidv 3231 . . . . . . 7 (𝑐 = 𝑦 → (∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑐) = (𝑑 𝑓)) ↔ ∃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓))))
219208, 218cbvrex2vw 3395 . . . . . 6 (∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)) ↔ ∃𝑥𝑃𝑦𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
220198, 219sylib 217 . . . . 5 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ∃𝑥𝑃𝑦𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑥) ∧ (𝐴 𝑥) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑦) ∧ (𝐶 𝑦) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑥 𝑦) = (𝑑 𝑓)))
221197, 220r19.29vva 3266 . . . 4 (((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸))) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
222221anasss 467 . . 3 ((𝜑 ∧ (((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸)) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
223116, 222sylan2b 594 . 2 ((𝜑 ∧ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
224115, 223impbida 798 1 (𝜑 → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩ ↔ ((𝐴𝐵𝐶𝐵) ∧ (𝐷𝐸𝐹𝐸) ∧ ∃𝑎𝑃𝑐𝑃𝑑𝑃𝑓𝑃 (((𝐴 ∈ (𝐵𝐼𝑎) ∧ (𝐴 𝑎) = (𝐸 𝐷)) ∧ (𝐶 ∈ (𝐵𝐼𝑐) ∧ (𝐶 𝑐) = (𝐸 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 𝑑) = (𝐵 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 𝑓) = (𝐵 𝐶))) ∧ (𝑎 𝑐) = (𝑑 𝑓)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1542  wcel 2110  wne 2945  wrex 3067   class class class wbr 5079  cfv 6431  (class class class)co 7269  ⟨“cs3 14551  Basecbs 16908  distcds 16967  TarskiGcstrkg 26784  Itvcitv 26790  cgrGccgrg 26867  hlGchlg 26957  cgrAccgra 27164
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580  ax-cnex 10926  ax-resscn 10927  ax-1cn 10928  ax-icn 10929  ax-addcl 10930  ax-addrcl 10931  ax-mulcl 10932  ax-mulrcl 10933  ax-mulcom 10934  ax-addass 10935  ax-mulass 10936  ax-distr 10937  ax-i2m1 10938  ax-1ne0 10939  ax-1rid 10940  ax-rnegex 10941  ax-rrecex 10942  ax-cnre 10943  ax-pre-lttri 10944  ax-pre-lttrn 10945  ax-pre-ltadd 10946  ax-pre-mulgt0 10947
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4846  df-int 4886  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6200  df-ord 6267  df-on 6268  df-lim 6269  df-suc 6270  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-om 7705  df-1st 7822  df-2nd 7823  df-frecs 8086  df-wrecs 8117  df-recs 8191  df-rdg 8230  df-1o 8286  df-oadd 8290  df-er 8479  df-map 8598  df-pm 8599  df-en 8715  df-dom 8716  df-sdom 8717  df-fin 8718  df-dju 9658  df-card 9696  df-pnf 11010  df-mnf 11011  df-xr 11012  df-ltxr 11013  df-le 11014  df-sub 11205  df-neg 11206  df-nn 11972  df-2 12034  df-3 12035  df-n0 12232  df-xnn0 12304  df-z 12318  df-uz 12580  df-fz 13237  df-fzo 13380  df-hash 14041  df-word 14214  df-concat 14270  df-s1 14297  df-s2 14557  df-s3 14558  df-trkgc 26805  df-trkgb 26806  df-trkgcb 26807  df-trkg 26810  df-cgrg 26868  df-leg 26940  df-hlg 26958  df-cgra 27165
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator