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

Theorem dfcgra2 28654
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 28632 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 2728 . . . . 5 (hlGβ€˜πΊ) = (hlGβ€˜πΊ)
4 dfcgra2.g . . . . . 6 (πœ‘ β†’ 𝐺 ∈ TarskiG)
54adantr 479 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐺 ∈ TarskiG)
6 dfcgra2.a . . . . . 6 (πœ‘ β†’ 𝐴 ∈ 𝑃)
76adantr 479 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐴 ∈ 𝑃)
8 dfcgra2.b . . . . . 6 (πœ‘ β†’ 𝐡 ∈ 𝑃)
98adantr 479 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐡 ∈ 𝑃)
10 dfcgra2.c . . . . . 6 (πœ‘ β†’ 𝐢 ∈ 𝑃)
1110adantr 479 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐢 ∈ 𝑃)
12 dfcgra2.d . . . . . 6 (πœ‘ β†’ 𝐷 ∈ 𝑃)
1312adantr 479 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐷 ∈ 𝑃)
14 dfcgra2.e . . . . . 6 (πœ‘ β†’ 𝐸 ∈ 𝑃)
1514adantr 479 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐸 ∈ 𝑃)
16 dfcgra2.f . . . . . 6 (πœ‘ β†’ 𝐹 ∈ 𝑃)
1716adantr 479 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐹 ∈ 𝑃)
18 simpr 483 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
191, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane1 28636 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐴 β‰  𝐡)
201, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane2 28637 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐡 β‰  𝐢)
2120necomd 2993 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐢 β‰  𝐡)
2219, 21jca 510 . . 3 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ (𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡))
231, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane3 28638 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐸 β‰  𝐷)
2423necomd 2993 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐷 β‰  𝐸)
251, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane4 28639 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐸 β‰  𝐹)
2625necomd 2993 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐹 β‰  𝐸)
2724, 26jca 510 . . 3 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))
28 simprl 769 . . . . . . . . 9 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))))
29 simprr 771 . . . . . . . . 9 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))
304ad6antr 734 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐺 ∈ TarskiG)
31 simp-5r 784 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž ∈ 𝑃)
328ad6antr 734 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐡 ∈ 𝑃)
33 simp-4r 782 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐 ∈ 𝑃)
34 simpllr 774 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑑 ∈ 𝑃)
3514ad6antr 734 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐸 ∈ 𝑃)
36 simplr 767 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑓 ∈ 𝑃)
3716ad6antr 734 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹 ∈ 𝑃)
3812ad6antr 734 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷 ∈ 𝑃)
3910ad6antr 734 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 ∈ 𝑃)
406ad6antr 734 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 ∈ 𝑃)
41 simp-6r 786 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
421, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41cgracom 28646 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ΄π΅πΆβ€βŸ©)
4328simplld 766 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 ∈ (π΅πΌπ‘Ž))
44 dfcgra2.m . . . . . . . . . . . . . . . . . 18 βˆ’ = (distβ€˜πΊ)
4519ad5antr 732 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 β‰  𝐡)
461, 44, 2, 30, 32, 40, 31, 43, 45tgbtwnne 28314 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐡 β‰  π‘Ž)
471, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45btwnhl1 28436 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴((hlGβ€˜πΊ)β€˜π΅)π‘Ž)
481, 2, 3, 40, 31, 32, 30, 47hlcomd 28428 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž((hlGβ€˜πΊ)β€˜π΅)𝐴)
491, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48cgrahl1 28640 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘Žπ΅πΆβ€βŸ©)
5028simprld 770 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 ∈ (𝐡𝐼𝑐))
5121ad5antr 732 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 β‰  𝐡)
521, 44, 2, 30, 32, 39, 33, 50, 51tgbtwnne 28314 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐡 β‰  𝑐)
531, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51btwnhl1 28436 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢((hlGβ€˜πΊ)β€˜π΅)𝑐)
541, 2, 3, 39, 33, 32, 30, 53hlcomd 28428 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐((hlGβ€˜πΊ)β€˜π΅)𝐢)
551, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54cgrahl2 28641 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘Žπ΅π‘β€βŸ©)
561, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55cgracom 28646 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ‘Žπ΅π‘β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
5729simplld 766 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷 ∈ (𝐸𝐼𝑑))
5824ad5antr 732 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷 β‰  𝐸)
591, 44, 2, 30, 35, 38, 34, 57, 58tgbtwnne 28314 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐸 β‰  𝑑)
601, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58btwnhl1 28436 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷((hlGβ€˜πΊ)β€˜πΈ)𝑑)
611, 2, 3, 38, 34, 35, 30, 60hlcomd 28428 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑑((hlGβ€˜πΊ)β€˜πΈ)𝐷)
621, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61cgrahl1 28640 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ‘Žπ΅π‘β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘‘πΈπΉβ€βŸ©)
6329simprld 770 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹 ∈ (𝐸𝐼𝑓))
6426ad5antr 732 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹 β‰  𝐸)
651, 44, 2, 30, 35, 37, 36, 63, 64tgbtwnne 28314 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐸 β‰  𝑓)
661, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64btwnhl1 28436 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹((hlGβ€˜πΊ)β€˜πΈ)𝑓)
671, 2, 3, 37, 36, 35, 30, 66hlcomd 28428 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑓((hlGβ€˜πΊ)β€˜πΈ)𝐹)
681, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67cgrahl2 28641 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ‘Žπ΅π‘β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘“β€βŸ©)
6946necomd 2993 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž β‰  𝐡)
701, 2, 3, 31, 40, 32, 30, 69hlid 28433 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž((hlGβ€˜πΊ)β€˜π΅)π‘Ž)
7152necomd 2993 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐 β‰  𝐡)
721, 2, 3, 33, 40, 32, 30, 71hlid 28433 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐((hlGβ€˜πΊ)β€˜π΅)𝑐)
731, 44, 2, 30, 32, 40, 31, 43tgbtwncom 28312 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 ∈ (π‘ŽπΌπ΅))
7428simplrd 768 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷))
751, 44, 2, 30, 40, 31, 35, 38, 74tgcgrcoml 28303 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (π‘Ž βˆ’ 𝐴) = (𝐸 βˆ’ 𝐷))
7629simplrd 768 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))
7776eqcomd 2734 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ 𝐴) = (𝐷 βˆ’ 𝑑))
781, 44, 2, 30, 32, 40, 38, 34, 77tgcgrcoml 28303 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐴 βˆ’ 𝐡) = (𝐷 βˆ’ 𝑑))
791, 44, 2, 30, 31, 40, 32, 35, 38, 34, 73, 57, 75, 78tgcgrextend 28309 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (π‘Ž βˆ’ 𝐡) = (𝐸 βˆ’ 𝑑))
801, 44, 2, 30, 31, 32, 35, 34, 79tgcgrcoml 28303 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝑑))
811, 44, 2, 30, 32, 39, 33, 50tgbtwncom 28312 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 ∈ (𝑐𝐼𝐡))
8228simprrd 772 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))
831, 44, 2, 30, 39, 33, 35, 37, 82tgcgrcoml 28303 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝑐 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐹))
8429simprrd 772 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))
8584eqcomd 2734 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ 𝐢) = (𝐹 βˆ’ 𝑓))
861, 44, 2, 30, 32, 39, 37, 36, 85tgcgrcoml 28303 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐢 βˆ’ 𝐡) = (𝐹 βˆ’ 𝑓))
871, 44, 2, 30, 33, 39, 32, 35, 37, 36, 81, 63, 83, 86tgcgrextend 28309 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝑐 βˆ’ 𝐡) = (𝐸 βˆ’ 𝑓))
881, 44, 2, 30, 33, 32, 35, 36, 87tgcgrcoml 28303 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ 𝑐) = (𝐸 βˆ’ 𝑓))
891, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 72, 80, 88cgracgr 28642 . . . . . . . . 9 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))
9028, 29, 893jca 1125 . . . . . . . 8 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
9190ex 411 . . . . . . 7 ((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) β†’ ((((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) β†’ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
9291reximdva 3165 . . . . . 6 (((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) β†’ (βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) β†’ βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
9392reximdva 3165 . . . . 5 ((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
9493imp 405 . . . 4 (((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
951, 44, 2, 4, 8, 6, 14, 12axtgsegcon 28288 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘Ž ∈ 𝑃 (𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)))
961, 44, 2, 4, 8, 10, 14, 16axtgsegcon 28288 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘ ∈ 𝑃 (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))
97 reeanv 3224 . . . . . . . 8 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ↔ (βˆƒπ‘Ž ∈ 𝑃 (𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ βˆƒπ‘ ∈ 𝑃 (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))))
9895, 96, 97sylanbrc 581 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))))
991, 44, 2, 4, 14, 12, 8, 6axtgsegcon 28288 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)))
1001, 44, 2, 4, 14, 16, 8, 10axtgsegcon 28288 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘“ ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))
101 reeanv 3224 . . . . . . . 8 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ↔ (βˆƒπ‘‘ ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ βˆƒπ‘“ ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))
10299, 100, 101sylanbrc 581 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))
10398, 102jca 510 . . . . . 6 (πœ‘ β†’ (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
104 r19.41vv 3222 . . . . . . . . 9 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))))
105 ancom 459 . . . . . . . . . 10 ((((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
1061052rexbii 3126 . . . . . . . . 9 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
107 ancom 459 . . . . . . . . 9 ((βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
108104, 106, 1073bitr3i 300 . . . . . . . 8 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
1091082rexbii 3126 . . . . . . 7 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
110 r19.41vv 3222 . . . . . . 7 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
111109, 110bitr2i 275 . . . . . 6 ((βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
112103, 111sylib 217 . . . . 5 (πœ‘ β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
113112adantr 479 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
11494, 113reximddv2 3210 . . 3 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
11522, 27, 1143jca 1125 . 2 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
116 df-3an 1086 . . 3 (((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) ↔ (((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸)) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
1174ad6antr 734 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐺 ∈ TarskiG)
11812ad6antr 734 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 ∈ 𝑃)
11914ad6antr 734 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐸 ∈ 𝑃)
12016ad6antr 734 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹 ∈ 𝑃)
1216ad6antr 734 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴 ∈ 𝑃)
1228ad6antr 734 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐡 ∈ 𝑃)
12310ad6antr 734 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 ∈ 𝑃)
124 simp-4r 782 . . . . . . . . . 10 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑦 ∈ 𝑃)
125 simp-5r 784 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ π‘₯ ∈ 𝑃)
126 simpllr 774 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑧 ∈ 𝑃)
127 simplr 767 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑑 ∈ 𝑃)
128 eqid 2728 . . . . . . . . . . . . . 14 (cgrGβ€˜πΊ) = (cgrGβ€˜πΊ)
129 simpr1 1191 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ ((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))))
130129simplld 766 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴 ∈ (𝐡𝐼π‘₯))
131 simpr2 1192 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))))
132131simplld 766 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 ∈ (𝐸𝐼𝑧))
1331, 44, 2, 117, 119, 118, 126, 132tgbtwncom 28312 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 ∈ (𝑧𝐼𝐸))
134131simplrd 768 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴))
135134eqcomd 2734 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝐴) = (𝐷 βˆ’ 𝑧))
1361, 44, 2, 117, 122, 121, 118, 126, 135tgcgrcomr 28302 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝐴) = (𝑧 βˆ’ 𝐷))
137129simplrd 768 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷))
1381, 44, 2, 117, 121, 125, 119, 118, 137tgcgrcomr 28302 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐴 βˆ’ π‘₯) = (𝐷 βˆ’ 𝐸))
1391, 44, 2, 117, 122, 121, 125, 126, 118, 119, 130, 133, 136, 138tgcgrextend 28309 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ π‘₯) = (𝑧 βˆ’ 𝐸))
1401, 44, 2, 117, 122, 125, 126, 119, 139tgcgrcoml 28303 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (π‘₯ βˆ’ 𝐡) = (𝑧 βˆ’ 𝐸))
141129simprld 770 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 ∈ (𝐡𝐼𝑦))
1421, 44, 2, 117, 122, 123, 124, 141tgbtwncom 28312 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 ∈ (𝑦𝐼𝐡))
143131simprld 770 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹 ∈ (𝐸𝐼𝑑))
144129simprrd 772 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))
1451, 44, 2, 117, 123, 124, 119, 120, 144tgcgrcoml 28303 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝑦 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐹))
146131simprrd 772 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))
147146eqcomd 2734 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝐢) = (𝐹 βˆ’ 𝑑))
1481, 44, 2, 117, 122, 123, 120, 127, 147tgcgrcoml 28303 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐢 βˆ’ 𝐡) = (𝐹 βˆ’ 𝑑))
1491, 44, 2, 117, 124, 123, 122, 119, 120, 127, 142, 143, 145, 148tgcgrextend 28309 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝑦 βˆ’ 𝐡) = (𝐸 βˆ’ 𝑑))
1501, 44, 2, 117, 124, 122, 119, 127, 149tgcgrcoml 28303 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝑦) = (𝐸 βˆ’ 𝑑))
151 simpr3 1193 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))
1521, 44, 2, 117, 125, 124, 126, 127, 151tgcgrcomlr 28304 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝑦 βˆ’ π‘₯) = (𝑑 βˆ’ 𝑧))
1531, 44, 128, 117, 125, 122, 124, 126, 119, 127, 140, 150, 152trgcgr 28340 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ‘₯π΅π‘¦β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘§πΈπ‘‘β€βŸ©)
154 simp-6r 786 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸)))
155154simprld 770 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 β‰  𝐸)
1561, 44, 2, 117, 119, 118, 126, 132, 155tgbtwnne 28314 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐸 β‰  𝑧)
1571, 2, 3, 119, 126, 118, 117, 122, 132, 156, 155btwnhl1 28436 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷((hlGβ€˜πΊ)β€˜πΈ)𝑧)
1581, 2, 3, 118, 126, 119, 117, 157hlcomd 28428 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑧((hlGβ€˜πΊ)β€˜πΈ)𝐷)
159154simprrd 772 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹 β‰  𝐸)
1601, 44, 2, 117, 119, 120, 127, 143, 159tgbtwnne 28314 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐸 β‰  𝑑)
1611, 2, 3, 119, 127, 120, 117, 122, 143, 160, 159btwnhl1 28436 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹((hlGβ€˜πΊ)β€˜πΈ)𝑑)
1621, 2, 3, 120, 127, 119, 117, 161hlcomd 28428 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑑((hlGβ€˜πΊ)β€˜πΈ)𝐹)
1631, 2, 3, 117, 125, 122, 124, 118, 119, 120, 126, 127, 153, 158, 162iscgrad 28635 . . . . . . . . . . . 12 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ‘₯π΅π‘¦β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
1641, 2, 117, 3, 125, 122, 124, 118, 119, 120, 163cgracom 28646 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘₯π΅π‘¦β€βŸ©)
165154simplld 766 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴 β‰  𝐡)
1661, 44, 2, 117, 122, 121, 125, 130, 165tgbtwnne 28314 . . . . . . . . . . . 12 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐡 β‰  π‘₯)
1671, 2, 3, 122, 125, 121, 117, 121, 130, 166, 165btwnhl1 28436 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴((hlGβ€˜πΊ)β€˜π΅)π‘₯)
1681, 2, 3, 117, 118, 119, 120, 125, 122, 124, 164, 121, 167cgrahl1 28640 . . . . . . . . . 10 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ΄π΅π‘¦β€βŸ©)
169154simplrd 768 . . . . . . . . . . . 12 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 β‰  𝐡)
1701, 44, 2, 117, 122, 123, 124, 141, 169tgbtwnne 28314 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐡 β‰  𝑦)
1711, 2, 3, 122, 124, 123, 117, 121, 141, 170, 169btwnhl1 28436 . . . . . . . . . 10 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢((hlGβ€˜πΊ)β€˜π΅)𝑦)
1721, 2, 3, 117, 118, 119, 120, 121, 122, 124, 168, 123, 171cgrahl2 28641 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ΄π΅πΆβ€βŸ©)
1731, 2, 117, 3, 118, 119, 120, 121, 122, 123, 172cgracom 28646 . . . . . . . 8 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
174173adantl3r 748 . . . . . . 7 ((((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
175 simpr 483 . . . . . . . 8 (((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
176 oveq2 7434 . . . . . . . . . . . . 13 (𝑑 = 𝑧 β†’ (𝐸𝐼𝑑) = (𝐸𝐼𝑧))
177176eleq2d 2815 . . . . . . . . . . . 12 (𝑑 = 𝑧 β†’ (𝐷 ∈ (𝐸𝐼𝑑) ↔ 𝐷 ∈ (𝐸𝐼𝑧)))
178 oveq2 7434 . . . . . . . . . . . . 13 (𝑑 = 𝑧 β†’ (𝐷 βˆ’ 𝑑) = (𝐷 βˆ’ 𝑧))
179178eqeq1d 2730 . . . . . . . . . . . 12 (𝑑 = 𝑧 β†’ ((𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴) ↔ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)))
180177, 179anbi12d 630 . . . . . . . . . . 11 (𝑑 = 𝑧 β†’ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴))))
181180anbi1d 629 . . . . . . . . . 10 (𝑑 = 𝑧 β†’ (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
182 oveq1 7433 . . . . . . . . . . 11 (𝑑 = 𝑧 β†’ (𝑑 βˆ’ 𝑓) = (𝑧 βˆ’ 𝑓))
183182eqeq2d 2739 . . . . . . . . . 10 (𝑑 = 𝑧 β†’ ((π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓)))
184181, 1833anbi23d 1435 . . . . . . . . 9 (𝑑 = 𝑧 β†’ ((((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓))))
185 oveq2 7434 . . . . . . . . . . . . 13 (𝑓 = 𝑑 β†’ (𝐸𝐼𝑓) = (𝐸𝐼𝑑))
186185eleq2d 2815 . . . . . . . . . . . 12 (𝑓 = 𝑑 β†’ (𝐹 ∈ (𝐸𝐼𝑓) ↔ 𝐹 ∈ (𝐸𝐼𝑑)))
187 oveq2 7434 . . . . . . . . . . . . 13 (𝑓 = 𝑑 β†’ (𝐹 βˆ’ 𝑓) = (𝐹 βˆ’ 𝑑))
188187eqeq1d 2730 . . . . . . . . . . . 12 (𝑓 = 𝑑 β†’ ((𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢) ↔ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢)))
189186, 188anbi12d 630 . . . . . . . . . . 11 (𝑓 = 𝑑 β†’ ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)) ↔ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))))
190189anbi2d 628 . . . . . . . . . 10 (𝑓 = 𝑑 β†’ (((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢)))))
191 oveq2 7434 . . . . . . . . . . 11 (𝑓 = 𝑑 β†’ (𝑧 βˆ’ 𝑓) = (𝑧 βˆ’ 𝑑))
192191eqeq2d 2739 . . . . . . . . . 10 (𝑓 = 𝑑 β†’ ((π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑)))
193190, 1923anbi23d 1435 . . . . . . . . 9 (𝑓 = 𝑑 β†’ ((((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))))
194184, 193cbvrex2vw 3237 . . . . . . . 8 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑)))
195175, 194sylib 217 . . . . . . 7 (((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑)))
196174, 195r19.29vva 3211 . . . . . 6 (((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
197196adantl3r 748 . . . . 5 ((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
198 simpr 483 . . . . . 6 (((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
199 oveq2 7434 . . . . . . . . . . . 12 (π‘Ž = π‘₯ β†’ (π΅πΌπ‘Ž) = (𝐡𝐼π‘₯))
200199eleq2d 2815 . . . . . . . . . . 11 (π‘Ž = π‘₯ β†’ (𝐴 ∈ (π΅πΌπ‘Ž) ↔ 𝐴 ∈ (𝐡𝐼π‘₯)))
201 oveq2 7434 . . . . . . . . . . . 12 (π‘Ž = π‘₯ β†’ (𝐴 βˆ’ π‘Ž) = (𝐴 βˆ’ π‘₯))
202201eqeq1d 2730 . . . . . . . . . . 11 (π‘Ž = π‘₯ β†’ ((𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷) ↔ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)))
203200, 202anbi12d 630 . . . . . . . . . 10 (π‘Ž = π‘₯ β†’ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ↔ (𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷))))
204203anbi1d 629 . . . . . . . . 9 (π‘Ž = π‘₯ β†’ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ↔ ((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))))
205 oveq1 7433 . . . . . . . . . 10 (π‘Ž = π‘₯ β†’ (π‘Ž βˆ’ 𝑐) = (π‘₯ βˆ’ 𝑐))
206205eqeq1d 2730 . . . . . . . . 9 (π‘Ž = π‘₯ β†’ ((π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
207204, 2063anbi13d 1434 . . . . . . . 8 (π‘Ž = π‘₯ β†’ ((((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
2082072rexbidv 3217 . . . . . . 7 (π‘Ž = π‘₯ β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
209 oveq2 7434 . . . . . . . . . . . 12 (𝑐 = 𝑦 β†’ (𝐡𝐼𝑐) = (𝐡𝐼𝑦))
210209eleq2d 2815 . . . . . . . . . . 11 (𝑐 = 𝑦 β†’ (𝐢 ∈ (𝐡𝐼𝑐) ↔ 𝐢 ∈ (𝐡𝐼𝑦)))
211 oveq2 7434 . . . . . . . . . . . 12 (𝑐 = 𝑦 β†’ (𝐢 βˆ’ 𝑐) = (𝐢 βˆ’ 𝑦))
212211eqeq1d 2730 . . . . . . . . . . 11 (𝑐 = 𝑦 β†’ ((𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹) ↔ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹)))
213210, 212anbi12d 630 . . . . . . . . . 10 (𝑐 = 𝑦 β†’ ((𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)) ↔ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))))
214213anbi2d 628 . . . . . . . . 9 (𝑐 = 𝑦 β†’ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ↔ ((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹)))))
215 oveq2 7434 . . . . . . . . . 10 (𝑐 = 𝑦 β†’ (π‘₯ βˆ’ 𝑐) = (π‘₯ βˆ’ 𝑦))
216215eqeq1d 2730 . . . . . . . . 9 (𝑐 = 𝑦 β†’ ((π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
217214, 2163anbi13d 1434 . . . . . . . 8 (𝑐 = 𝑦 β†’ ((((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))))
2182172rexbidv 3217 . . . . . . 7 (𝑐 = 𝑦 β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))))
219208, 218cbvrex2vw 3237 . . . . . 6 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
220198, 219sylib 217 . . . . 5 (((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
221197, 220r19.29vva 3211 . . . 4 (((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
222221anasss 465 . . 3 ((πœ‘ ∧ (((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸)) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
223116, 222sylan2b 592 . 2 ((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
224115, 223impbida 799 1 (πœ‘ β†’ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ© ↔ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2937  βˆƒwrex 3067   class class class wbr 5152  β€˜cfv 6553  (class class class)co 7426  βŸ¨β€œcs3 14833  Basecbs 17187  distcds 17249  TarskiGcstrkg 28251  Itvcitv 28257  cgrGccgrg 28334  hlGchlg 28424  cgrAccgra 28631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-oadd 8497  df-er 8731  df-map 8853  df-pm 8854  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-dju 9932  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-nn 12251  df-2 12313  df-3 12314  df-n0 12511  df-xnn0 12583  df-z 12597  df-uz 12861  df-fz 13525  df-fzo 13668  df-hash 14330  df-word 14505  df-concat 14561  df-s1 14586  df-s2 14839  df-s3 14840  df-trkgc 28272  df-trkgb 28273  df-trkgcb 28274  df-trkg 28277  df-cgrg 28335  df-leg 28407  df-hlg 28425  df-cgra 28632
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator