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

Theorem dfcgra2 27814
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 27792 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 2737 . . . . 5 (hlGβ€˜πΊ) = (hlGβ€˜πΊ)
4 dfcgra2.g . . . . . 6 (πœ‘ β†’ 𝐺 ∈ TarskiG)
54adantr 482 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐺 ∈ TarskiG)
6 dfcgra2.a . . . . . 6 (πœ‘ β†’ 𝐴 ∈ 𝑃)
76adantr 482 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐴 ∈ 𝑃)
8 dfcgra2.b . . . . . 6 (πœ‘ β†’ 𝐡 ∈ 𝑃)
98adantr 482 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐡 ∈ 𝑃)
10 dfcgra2.c . . . . . 6 (πœ‘ β†’ 𝐢 ∈ 𝑃)
1110adantr 482 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐢 ∈ 𝑃)
12 dfcgra2.d . . . . . 6 (πœ‘ β†’ 𝐷 ∈ 𝑃)
1312adantr 482 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐷 ∈ 𝑃)
14 dfcgra2.e . . . . . 6 (πœ‘ β†’ 𝐸 ∈ 𝑃)
1514adantr 482 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐸 ∈ 𝑃)
16 dfcgra2.f . . . . . 6 (πœ‘ β†’ 𝐹 ∈ 𝑃)
1716adantr 482 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐹 ∈ 𝑃)
18 simpr 486 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
191, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane1 27796 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐴 β‰  𝐡)
201, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane2 27797 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐡 β‰  𝐢)
2120necomd 3000 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐢 β‰  𝐡)
2219, 21jca 513 . . 3 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ (𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡))
231, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane3 27798 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐸 β‰  𝐷)
2423necomd 3000 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐷 β‰  𝐸)
251, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane4 27799 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐸 β‰  𝐹)
2625necomd 3000 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐹 β‰  𝐸)
2724, 26jca 513 . . 3 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))
28 simprl 770 . . . . . . . . 9 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))))
29 simprr 772 . . . . . . . . 9 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))
304ad6antr 735 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐺 ∈ TarskiG)
31 simp-5r 785 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž ∈ 𝑃)
328ad6antr 735 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐡 ∈ 𝑃)
33 simp-4r 783 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐 ∈ 𝑃)
34 simpllr 775 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑑 ∈ 𝑃)
3514ad6antr 735 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐸 ∈ 𝑃)
36 simplr 768 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑓 ∈ 𝑃)
3716ad6antr 735 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹 ∈ 𝑃)
3812ad6antr 735 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷 ∈ 𝑃)
3910ad6antr 735 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 ∈ 𝑃)
406ad6antr 735 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 ∈ 𝑃)
41 simp-6r 787 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
421, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41cgracom 27806 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ΄π΅πΆβ€βŸ©)
4328simplld 767 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 ∈ (π΅πΌπ‘Ž))
44 dfcgra2.m . . . . . . . . . . . . . . . . . 18 βˆ’ = (distβ€˜πΊ)
4519ad5antr 733 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 β‰  𝐡)
461, 44, 2, 30, 32, 40, 31, 43, 45tgbtwnne 27474 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐡 β‰  π‘Ž)
471, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45btwnhl1 27596 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴((hlGβ€˜πΊ)β€˜π΅)π‘Ž)
481, 2, 3, 40, 31, 32, 30, 47hlcomd 27588 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž((hlGβ€˜πΊ)β€˜π΅)𝐴)
491, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48cgrahl1 27800 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘Žπ΅πΆβ€βŸ©)
5028simprld 771 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 ∈ (𝐡𝐼𝑐))
5121ad5antr 733 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 β‰  𝐡)
521, 44, 2, 30, 32, 39, 33, 50, 51tgbtwnne 27474 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐡 β‰  𝑐)
531, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51btwnhl1 27596 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢((hlGβ€˜πΊ)β€˜π΅)𝑐)
541, 2, 3, 39, 33, 32, 30, 53hlcomd 27588 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐((hlGβ€˜πΊ)β€˜π΅)𝐢)
551, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54cgrahl2 27801 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘Žπ΅π‘β€βŸ©)
561, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55cgracom 27806 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ‘Žπ΅π‘β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
5729simplld 767 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷 ∈ (𝐸𝐼𝑑))
5824ad5antr 733 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷 β‰  𝐸)
591, 44, 2, 30, 35, 38, 34, 57, 58tgbtwnne 27474 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐸 β‰  𝑑)
601, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58btwnhl1 27596 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷((hlGβ€˜πΊ)β€˜πΈ)𝑑)
611, 2, 3, 38, 34, 35, 30, 60hlcomd 27588 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑑((hlGβ€˜πΊ)β€˜πΈ)𝐷)
621, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61cgrahl1 27800 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ‘Žπ΅π‘β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘‘πΈπΉβ€βŸ©)
6329simprld 771 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹 ∈ (𝐸𝐼𝑓))
6426ad5antr 733 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹 β‰  𝐸)
651, 44, 2, 30, 35, 37, 36, 63, 64tgbtwnne 27474 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐸 β‰  𝑓)
661, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64btwnhl1 27596 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹((hlGβ€˜πΊ)β€˜πΈ)𝑓)
671, 2, 3, 37, 36, 35, 30, 66hlcomd 27588 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑓((hlGβ€˜πΊ)β€˜πΈ)𝐹)
681, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67cgrahl2 27801 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ‘Žπ΅π‘β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘“β€βŸ©)
6946necomd 3000 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž β‰  𝐡)
701, 2, 3, 31, 40, 32, 30, 69hlid 27593 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž((hlGβ€˜πΊ)β€˜π΅)π‘Ž)
7152necomd 3000 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐 β‰  𝐡)
721, 2, 3, 33, 40, 32, 30, 71hlid 27593 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐((hlGβ€˜πΊ)β€˜π΅)𝑐)
731, 44, 2, 30, 32, 40, 31, 43tgbtwncom 27472 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 ∈ (π‘ŽπΌπ΅))
7428simplrd 769 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷))
751, 44, 2, 30, 40, 31, 35, 38, 74tgcgrcoml 27463 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (π‘Ž βˆ’ 𝐴) = (𝐸 βˆ’ 𝐷))
7629simplrd 769 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))
7776eqcomd 2743 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ 𝐴) = (𝐷 βˆ’ 𝑑))
781, 44, 2, 30, 32, 40, 38, 34, 77tgcgrcoml 27463 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐴 βˆ’ 𝐡) = (𝐷 βˆ’ 𝑑))
791, 44, 2, 30, 31, 40, 32, 35, 38, 34, 73, 57, 75, 78tgcgrextend 27469 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (π‘Ž βˆ’ 𝐡) = (𝐸 βˆ’ 𝑑))
801, 44, 2, 30, 31, 32, 35, 34, 79tgcgrcoml 27463 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝑑))
811, 44, 2, 30, 32, 39, 33, 50tgbtwncom 27472 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 ∈ (𝑐𝐼𝐡))
8228simprrd 773 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))
831, 44, 2, 30, 39, 33, 35, 37, 82tgcgrcoml 27463 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝑐 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐹))
8429simprrd 773 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))
8584eqcomd 2743 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ 𝐢) = (𝐹 βˆ’ 𝑓))
861, 44, 2, 30, 32, 39, 37, 36, 85tgcgrcoml 27463 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐢 βˆ’ 𝐡) = (𝐹 βˆ’ 𝑓))
871, 44, 2, 30, 33, 39, 32, 35, 37, 36, 81, 63, 83, 86tgcgrextend 27469 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝑐 βˆ’ 𝐡) = (𝐸 βˆ’ 𝑓))
881, 44, 2, 30, 33, 32, 35, 36, 87tgcgrcoml 27463 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ 𝑐) = (𝐸 βˆ’ 𝑓))
891, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 72, 80, 88cgracgr 27802 . . . . . . . . 9 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))
9028, 29, 893jca 1129 . . . . . . . 8 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
9190ex 414 . . . . . . 7 ((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) β†’ ((((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) β†’ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
9291reximdva 3166 . . . . . 6 (((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) β†’ (βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) β†’ βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
9392reximdva 3166 . . . . 5 ((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
9493imp 408 . . . 4 (((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
951, 44, 2, 4, 8, 6, 14, 12axtgsegcon 27448 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘Ž ∈ 𝑃 (𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)))
961, 44, 2, 4, 8, 10, 14, 16axtgsegcon 27448 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘ ∈ 𝑃 (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))
97 reeanv 3220 . . . . . . . 8 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ↔ (βˆƒπ‘Ž ∈ 𝑃 (𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ βˆƒπ‘ ∈ 𝑃 (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))))
9895, 96, 97sylanbrc 584 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))))
991, 44, 2, 4, 14, 12, 8, 6axtgsegcon 27448 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)))
1001, 44, 2, 4, 14, 16, 8, 10axtgsegcon 27448 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘“ ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))
101 reeanv 3220 . . . . . . . 8 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ↔ (βˆƒπ‘‘ ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ βˆƒπ‘“ ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))
10299, 100, 101sylanbrc 584 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))
10398, 102jca 513 . . . . . 6 (πœ‘ β†’ (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
104 r19.41vv 3218 . . . . . . . . 9 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))))
105 ancom 462 . . . . . . . . . 10 ((((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
1061052rexbii 3129 . . . . . . . . 9 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
107 ancom 462 . . . . . . . . 9 ((βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
108104, 106, 1073bitr3i 301 . . . . . . . 8 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
1091082rexbii 3129 . . . . . . 7 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
110 r19.41vv 3218 . . . . . . 7 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
111109, 110bitr2i 276 . . . . . 6 ((βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
112103, 111sylib 217 . . . . 5 (πœ‘ β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
113112adantr 482 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
11494, 113reximddv2 3207 . . 3 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
11522, 27, 1143jca 1129 . 2 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
116 df-3an 1090 . . 3 (((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) ↔ (((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸)) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
1174ad6antr 735 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐺 ∈ TarskiG)
11812ad6antr 735 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 ∈ 𝑃)
11914ad6antr 735 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐸 ∈ 𝑃)
12016ad6antr 735 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹 ∈ 𝑃)
1216ad6antr 735 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴 ∈ 𝑃)
1228ad6antr 735 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐡 ∈ 𝑃)
12310ad6antr 735 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 ∈ 𝑃)
124 simp-4r 783 . . . . . . . . . 10 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑦 ∈ 𝑃)
125 simp-5r 785 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ π‘₯ ∈ 𝑃)
126 simpllr 775 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑧 ∈ 𝑃)
127 simplr 768 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑑 ∈ 𝑃)
128 eqid 2737 . . . . . . . . . . . . . 14 (cgrGβ€˜πΊ) = (cgrGβ€˜πΊ)
129 simpr1 1195 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ ((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))))
130129simplld 767 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴 ∈ (𝐡𝐼π‘₯))
131 simpr2 1196 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))))
132131simplld 767 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 ∈ (𝐸𝐼𝑧))
1331, 44, 2, 117, 119, 118, 126, 132tgbtwncom 27472 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 ∈ (𝑧𝐼𝐸))
134131simplrd 769 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴))
135134eqcomd 2743 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝐴) = (𝐷 βˆ’ 𝑧))
1361, 44, 2, 117, 122, 121, 118, 126, 135tgcgrcomr 27462 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝐴) = (𝑧 βˆ’ 𝐷))
137129simplrd 769 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷))
1381, 44, 2, 117, 121, 125, 119, 118, 137tgcgrcomr 27462 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐴 βˆ’ π‘₯) = (𝐷 βˆ’ 𝐸))
1391, 44, 2, 117, 122, 121, 125, 126, 118, 119, 130, 133, 136, 138tgcgrextend 27469 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ π‘₯) = (𝑧 βˆ’ 𝐸))
1401, 44, 2, 117, 122, 125, 126, 119, 139tgcgrcoml 27463 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (π‘₯ βˆ’ 𝐡) = (𝑧 βˆ’ 𝐸))
141129simprld 771 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 ∈ (𝐡𝐼𝑦))
1421, 44, 2, 117, 122, 123, 124, 141tgbtwncom 27472 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 ∈ (𝑦𝐼𝐡))
143131simprld 771 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹 ∈ (𝐸𝐼𝑑))
144129simprrd 773 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))
1451, 44, 2, 117, 123, 124, 119, 120, 144tgcgrcoml 27463 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝑦 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐹))
146131simprrd 773 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))
147146eqcomd 2743 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝐢) = (𝐹 βˆ’ 𝑑))
1481, 44, 2, 117, 122, 123, 120, 127, 147tgcgrcoml 27463 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐢 βˆ’ 𝐡) = (𝐹 βˆ’ 𝑑))
1491, 44, 2, 117, 124, 123, 122, 119, 120, 127, 142, 143, 145, 148tgcgrextend 27469 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝑦 βˆ’ 𝐡) = (𝐸 βˆ’ 𝑑))
1501, 44, 2, 117, 124, 122, 119, 127, 149tgcgrcoml 27463 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝑦) = (𝐸 βˆ’ 𝑑))
151 simpr3 1197 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))
1521, 44, 2, 117, 125, 124, 126, 127, 151tgcgrcomlr 27464 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝑦 βˆ’ π‘₯) = (𝑑 βˆ’ 𝑧))
1531, 44, 128, 117, 125, 122, 124, 126, 119, 127, 140, 150, 152trgcgr 27500 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ‘₯π΅π‘¦β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘§πΈπ‘‘β€βŸ©)
154 simp-6r 787 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸)))
155154simprld 771 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 β‰  𝐸)
1561, 44, 2, 117, 119, 118, 126, 132, 155tgbtwnne 27474 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐸 β‰  𝑧)
1571, 2, 3, 119, 126, 118, 117, 122, 132, 156, 155btwnhl1 27596 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷((hlGβ€˜πΊ)β€˜πΈ)𝑧)
1581, 2, 3, 118, 126, 119, 117, 157hlcomd 27588 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑧((hlGβ€˜πΊ)β€˜πΈ)𝐷)
159154simprrd 773 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹 β‰  𝐸)
1601, 44, 2, 117, 119, 120, 127, 143, 159tgbtwnne 27474 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐸 β‰  𝑑)
1611, 2, 3, 119, 127, 120, 117, 122, 143, 160, 159btwnhl1 27596 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹((hlGβ€˜πΊ)β€˜πΈ)𝑑)
1621, 2, 3, 120, 127, 119, 117, 161hlcomd 27588 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑑((hlGβ€˜πΊ)β€˜πΈ)𝐹)
1631, 2, 3, 117, 125, 122, 124, 118, 119, 120, 126, 127, 153, 158, 162iscgrad 27795 . . . . . . . . . . . 12 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ‘₯π΅π‘¦β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
1641, 2, 117, 3, 125, 122, 124, 118, 119, 120, 163cgracom 27806 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘₯π΅π‘¦β€βŸ©)
165154simplld 767 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴 β‰  𝐡)
1661, 44, 2, 117, 122, 121, 125, 130, 165tgbtwnne 27474 . . . . . . . . . . . 12 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐡 β‰  π‘₯)
1671, 2, 3, 122, 125, 121, 117, 121, 130, 166, 165btwnhl1 27596 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴((hlGβ€˜πΊ)β€˜π΅)π‘₯)
1681, 2, 3, 117, 118, 119, 120, 125, 122, 124, 164, 121, 167cgrahl1 27800 . . . . . . . . . 10 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ΄π΅π‘¦β€βŸ©)
169154simplrd 769 . . . . . . . . . . . 12 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 β‰  𝐡)
1701, 44, 2, 117, 122, 123, 124, 141, 169tgbtwnne 27474 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐡 β‰  𝑦)
1711, 2, 3, 122, 124, 123, 117, 121, 141, 170, 169btwnhl1 27596 . . . . . . . . . 10 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢((hlGβ€˜πΊ)β€˜π΅)𝑦)
1721, 2, 3, 117, 118, 119, 120, 121, 122, 124, 168, 123, 171cgrahl2 27801 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ΄π΅πΆβ€βŸ©)
1731, 2, 117, 3, 118, 119, 120, 121, 122, 123, 172cgracom 27806 . . . . . . . 8 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
174173adantl3r 749 . . . . . . 7 ((((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
175 simpr 486 . . . . . . . 8 (((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
176 oveq2 7370 . . . . . . . . . . . . 13 (𝑑 = 𝑧 β†’ (𝐸𝐼𝑑) = (𝐸𝐼𝑧))
177176eleq2d 2824 . . . . . . . . . . . 12 (𝑑 = 𝑧 β†’ (𝐷 ∈ (𝐸𝐼𝑑) ↔ 𝐷 ∈ (𝐸𝐼𝑧)))
178 oveq2 7370 . . . . . . . . . . . . 13 (𝑑 = 𝑧 β†’ (𝐷 βˆ’ 𝑑) = (𝐷 βˆ’ 𝑧))
179178eqeq1d 2739 . . . . . . . . . . . 12 (𝑑 = 𝑧 β†’ ((𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴) ↔ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)))
180177, 179anbi12d 632 . . . . . . . . . . 11 (𝑑 = 𝑧 β†’ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴))))
181180anbi1d 631 . . . . . . . . . 10 (𝑑 = 𝑧 β†’ (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
182 oveq1 7369 . . . . . . . . . . 11 (𝑑 = 𝑧 β†’ (𝑑 βˆ’ 𝑓) = (𝑧 βˆ’ 𝑓))
183182eqeq2d 2748 . . . . . . . . . 10 (𝑑 = 𝑧 β†’ ((π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓)))
184181, 1833anbi23d 1440 . . . . . . . . 9 (𝑑 = 𝑧 β†’ ((((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓))))
185 oveq2 7370 . . . . . . . . . . . . 13 (𝑓 = 𝑑 β†’ (𝐸𝐼𝑓) = (𝐸𝐼𝑑))
186185eleq2d 2824 . . . . . . . . . . . 12 (𝑓 = 𝑑 β†’ (𝐹 ∈ (𝐸𝐼𝑓) ↔ 𝐹 ∈ (𝐸𝐼𝑑)))
187 oveq2 7370 . . . . . . . . . . . . 13 (𝑓 = 𝑑 β†’ (𝐹 βˆ’ 𝑓) = (𝐹 βˆ’ 𝑑))
188187eqeq1d 2739 . . . . . . . . . . . 12 (𝑓 = 𝑑 β†’ ((𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢) ↔ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢)))
189186, 188anbi12d 632 . . . . . . . . . . 11 (𝑓 = 𝑑 β†’ ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)) ↔ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))))
190189anbi2d 630 . . . . . . . . . 10 (𝑓 = 𝑑 β†’ (((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢)))))
191 oveq2 7370 . . . . . . . . . . 11 (𝑓 = 𝑑 β†’ (𝑧 βˆ’ 𝑓) = (𝑧 βˆ’ 𝑑))
192191eqeq2d 2748 . . . . . . . . . 10 (𝑓 = 𝑑 β†’ ((π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑)))
193190, 1923anbi23d 1440 . . . . . . . . 9 (𝑓 = 𝑑 β†’ ((((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))))
194184, 193cbvrex2vw 3231 . . . . . . . 8 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑)))
195175, 194sylib 217 . . . . . . 7 (((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑)))
196174, 195r19.29vva 3208 . . . . . 6 (((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
197196adantl3r 749 . . . . 5 ((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
198 simpr 486 . . . . . 6 (((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
199 oveq2 7370 . . . . . . . . . . . 12 (π‘Ž = π‘₯ β†’ (π΅πΌπ‘Ž) = (𝐡𝐼π‘₯))
200199eleq2d 2824 . . . . . . . . . . 11 (π‘Ž = π‘₯ β†’ (𝐴 ∈ (π΅πΌπ‘Ž) ↔ 𝐴 ∈ (𝐡𝐼π‘₯)))
201 oveq2 7370 . . . . . . . . . . . 12 (π‘Ž = π‘₯ β†’ (𝐴 βˆ’ π‘Ž) = (𝐴 βˆ’ π‘₯))
202201eqeq1d 2739 . . . . . . . . . . 11 (π‘Ž = π‘₯ β†’ ((𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷) ↔ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)))
203200, 202anbi12d 632 . . . . . . . . . 10 (π‘Ž = π‘₯ β†’ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ↔ (𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷))))
204203anbi1d 631 . . . . . . . . 9 (π‘Ž = π‘₯ β†’ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ↔ ((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))))
205 oveq1 7369 . . . . . . . . . 10 (π‘Ž = π‘₯ β†’ (π‘Ž βˆ’ 𝑐) = (π‘₯ βˆ’ 𝑐))
206205eqeq1d 2739 . . . . . . . . 9 (π‘Ž = π‘₯ β†’ ((π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
207204, 2063anbi13d 1439 . . . . . . . 8 (π‘Ž = π‘₯ β†’ ((((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
2082072rexbidv 3214 . . . . . . 7 (π‘Ž = π‘₯ β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
209 oveq2 7370 . . . . . . . . . . . 12 (𝑐 = 𝑦 β†’ (𝐡𝐼𝑐) = (𝐡𝐼𝑦))
210209eleq2d 2824 . . . . . . . . . . 11 (𝑐 = 𝑦 β†’ (𝐢 ∈ (𝐡𝐼𝑐) ↔ 𝐢 ∈ (𝐡𝐼𝑦)))
211 oveq2 7370 . . . . . . . . . . . 12 (𝑐 = 𝑦 β†’ (𝐢 βˆ’ 𝑐) = (𝐢 βˆ’ 𝑦))
212211eqeq1d 2739 . . . . . . . . . . 11 (𝑐 = 𝑦 β†’ ((𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹) ↔ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹)))
213210, 212anbi12d 632 . . . . . . . . . 10 (𝑐 = 𝑦 β†’ ((𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)) ↔ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))))
214213anbi2d 630 . . . . . . . . 9 (𝑐 = 𝑦 β†’ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ↔ ((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹)))))
215 oveq2 7370 . . . . . . . . . 10 (𝑐 = 𝑦 β†’ (π‘₯ βˆ’ 𝑐) = (π‘₯ βˆ’ 𝑦))
216215eqeq1d 2739 . . . . . . . . 9 (𝑐 = 𝑦 β†’ ((π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
217214, 2163anbi13d 1439 . . . . . . . 8 (𝑐 = 𝑦 β†’ ((((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))))
2182172rexbidv 3214 . . . . . . 7 (𝑐 = 𝑦 β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))))
219208, 218cbvrex2vw 3231 . . . . . 6 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
220198, 219sylib 217 . . . . 5 (((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
221197, 220r19.29vva 3208 . . . 4 (((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
222221anasss 468 . . 3 ((πœ‘ ∧ (((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸)) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
223116, 222sylan2b 595 . 2 ((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
224115, 223impbida 800 1 (πœ‘ β†’ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ© ↔ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆƒwrex 3074   class class class wbr 5110  β€˜cfv 6501  (class class class)co 7362  βŸ¨β€œcs3 14738  Basecbs 17090  distcds 17149  TarskiGcstrkg 27411  Itvcitv 27417  cgrGccgrg 27494  hlGchlg 27584  cgrAccgra 27791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-xnn0 12493  df-z 12507  df-uz 12771  df-fz 13432  df-fzo 13575  df-hash 14238  df-word 14410  df-concat 14466  df-s1 14491  df-s2 14744  df-s3 14745  df-trkgc 27432  df-trkgb 27433  df-trkgcb 27434  df-trkg 27437  df-cgrg 27495  df-leg 27567  df-hlg 27585  df-cgra 27792
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator