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

Theorem dfcgra2 28584
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 28562 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 2726 . . . . 5 (hlGβ€˜πΊ) = (hlGβ€˜πΊ)
4 dfcgra2.g . . . . . 6 (πœ‘ β†’ 𝐺 ∈ TarskiG)
54adantr 480 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐺 ∈ TarskiG)
6 dfcgra2.a . . . . . 6 (πœ‘ β†’ 𝐴 ∈ 𝑃)
76adantr 480 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐴 ∈ 𝑃)
8 dfcgra2.b . . . . . 6 (πœ‘ β†’ 𝐡 ∈ 𝑃)
98adantr 480 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐡 ∈ 𝑃)
10 dfcgra2.c . . . . . 6 (πœ‘ β†’ 𝐢 ∈ 𝑃)
1110adantr 480 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐢 ∈ 𝑃)
12 dfcgra2.d . . . . . 6 (πœ‘ β†’ 𝐷 ∈ 𝑃)
1312adantr 480 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐷 ∈ 𝑃)
14 dfcgra2.e . . . . . 6 (πœ‘ β†’ 𝐸 ∈ 𝑃)
1514adantr 480 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐸 ∈ 𝑃)
16 dfcgra2.f . . . . . 6 (πœ‘ β†’ 𝐹 ∈ 𝑃)
1716adantr 480 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐹 ∈ 𝑃)
18 simpr 484 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
191, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane1 28566 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐴 β‰  𝐡)
201, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane2 28567 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐡 β‰  𝐢)
2120necomd 2990 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐢 β‰  𝐡)
2219, 21jca 511 . . 3 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ (𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡))
231, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane3 28568 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐸 β‰  𝐷)
2423necomd 2990 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐷 β‰  𝐸)
251, 2, 3, 5, 7, 9, 11, 13, 15, 17, 18cgrane4 28569 . . . . 5 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐸 β‰  𝐹)
2625necomd 2990 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ 𝐹 β‰  𝐸)
2724, 26jca 511 . . 3 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))
28 simprl 768 . . . . . . . . 9 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))))
29 simprr 770 . . . . . . . . 9 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))
304ad6antr 733 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐺 ∈ TarskiG)
31 simp-5r 783 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž ∈ 𝑃)
328ad6antr 733 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐡 ∈ 𝑃)
33 simp-4r 781 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐 ∈ 𝑃)
34 simpllr 773 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑑 ∈ 𝑃)
3514ad6antr 733 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐸 ∈ 𝑃)
36 simplr 766 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑓 ∈ 𝑃)
3716ad6antr 733 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹 ∈ 𝑃)
3812ad6antr 733 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷 ∈ 𝑃)
3910ad6antr 733 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 ∈ 𝑃)
406ad6antr 733 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 ∈ 𝑃)
41 simp-6r 785 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
421, 2, 30, 3, 40, 32, 39, 38, 35, 37, 41cgracom 28576 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ΄π΅πΆβ€βŸ©)
4328simplld 765 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 ∈ (π΅πΌπ‘Ž))
44 dfcgra2.m . . . . . . . . . . . . . . . . . 18 βˆ’ = (distβ€˜πΊ)
4519ad5antr 731 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 β‰  𝐡)
461, 44, 2, 30, 32, 40, 31, 43, 45tgbtwnne 28244 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐡 β‰  π‘Ž)
471, 2, 3, 32, 31, 40, 30, 40, 43, 46, 45btwnhl1 28366 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴((hlGβ€˜πΊ)β€˜π΅)π‘Ž)
481, 2, 3, 40, 31, 32, 30, 47hlcomd 28358 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž((hlGβ€˜πΊ)β€˜π΅)𝐴)
491, 2, 3, 30, 38, 35, 37, 40, 32, 39, 42, 31, 48cgrahl1 28570 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘Žπ΅πΆβ€βŸ©)
5028simprld 769 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 ∈ (𝐡𝐼𝑐))
5121ad5antr 731 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 β‰  𝐡)
521, 44, 2, 30, 32, 39, 33, 50, 51tgbtwnne 28244 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐡 β‰  𝑐)
531, 2, 3, 32, 33, 39, 30, 40, 50, 52, 51btwnhl1 28366 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢((hlGβ€˜πΊ)β€˜π΅)𝑐)
541, 2, 3, 39, 33, 32, 30, 53hlcomd 28358 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐((hlGβ€˜πΊ)β€˜π΅)𝐢)
551, 2, 3, 30, 38, 35, 37, 31, 32, 39, 49, 33, 54cgrahl2 28571 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘Žπ΅π‘β€βŸ©)
561, 2, 30, 3, 38, 35, 37, 31, 32, 33, 55cgracom 28576 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ‘Žπ΅π‘β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
5729simplld 765 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷 ∈ (𝐸𝐼𝑑))
5824ad5antr 731 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷 β‰  𝐸)
591, 44, 2, 30, 35, 38, 34, 57, 58tgbtwnne 28244 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐸 β‰  𝑑)
601, 2, 3, 35, 34, 38, 30, 40, 57, 59, 58btwnhl1 28366 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐷((hlGβ€˜πΊ)β€˜πΈ)𝑑)
611, 2, 3, 38, 34, 35, 30, 60hlcomd 28358 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑑((hlGβ€˜πΊ)β€˜πΈ)𝐷)
621, 2, 3, 30, 31, 32, 33, 38, 35, 37, 56, 34, 61cgrahl1 28570 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ‘Žπ΅π‘β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘‘πΈπΉβ€βŸ©)
6329simprld 769 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹 ∈ (𝐸𝐼𝑓))
6426ad5antr 731 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹 β‰  𝐸)
651, 44, 2, 30, 35, 37, 36, 63, 64tgbtwnne 28244 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐸 β‰  𝑓)
661, 2, 3, 35, 36, 37, 30, 40, 63, 65, 64btwnhl1 28366 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐹((hlGβ€˜πΊ)β€˜πΈ)𝑓)
671, 2, 3, 37, 36, 35, 30, 66hlcomd 28358 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑓((hlGβ€˜πΊ)β€˜πΈ)𝐹)
681, 2, 3, 30, 31, 32, 33, 34, 35, 37, 62, 36, 67cgrahl2 28571 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βŸ¨β€œπ‘Žπ΅π‘β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘“β€βŸ©)
6946necomd 2990 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž β‰  𝐡)
701, 2, 3, 31, 40, 32, 30, 69hlid 28363 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ π‘Ž((hlGβ€˜πΊ)β€˜π΅)π‘Ž)
7152necomd 2990 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐 β‰  𝐡)
721, 2, 3, 33, 40, 32, 30, 71hlid 28363 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝑐((hlGβ€˜πΊ)β€˜π΅)𝑐)
731, 44, 2, 30, 32, 40, 31, 43tgbtwncom 28242 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐴 ∈ (π‘ŽπΌπ΅))
7428simplrd 767 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷))
751, 44, 2, 30, 40, 31, 35, 38, 74tgcgrcoml 28233 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (π‘Ž βˆ’ 𝐴) = (𝐸 βˆ’ 𝐷))
7629simplrd 767 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))
7776eqcomd 2732 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ 𝐴) = (𝐷 βˆ’ 𝑑))
781, 44, 2, 30, 32, 40, 38, 34, 77tgcgrcoml 28233 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐴 βˆ’ 𝐡) = (𝐷 βˆ’ 𝑑))
791, 44, 2, 30, 31, 40, 32, 35, 38, 34, 73, 57, 75, 78tgcgrextend 28239 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (π‘Ž βˆ’ 𝐡) = (𝐸 βˆ’ 𝑑))
801, 44, 2, 30, 31, 32, 35, 34, 79tgcgrcoml 28233 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝑑))
811, 44, 2, 30, 32, 39, 33, 50tgbtwncom 28242 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ 𝐢 ∈ (𝑐𝐼𝐡))
8228simprrd 771 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))
831, 44, 2, 30, 39, 33, 35, 37, 82tgcgrcoml 28233 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝑐 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐹))
8429simprrd 771 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))
8584eqcomd 2732 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ 𝐢) = (𝐹 βˆ’ 𝑓))
861, 44, 2, 30, 32, 39, 37, 36, 85tgcgrcoml 28233 . . . . . . . . . . . 12 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐢 βˆ’ 𝐡) = (𝐹 βˆ’ 𝑓))
871, 44, 2, 30, 33, 39, 32, 35, 37, 36, 81, 63, 83, 86tgcgrextend 28239 . . . . . . . . . . 11 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝑐 βˆ’ 𝐡) = (𝐸 βˆ’ 𝑓))
881, 44, 2, 30, 33, 32, 35, 36, 87tgcgrcoml 28233 . . . . . . . . . 10 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (𝐡 βˆ’ 𝑐) = (𝐸 βˆ’ 𝑓))
891, 2, 3, 30, 31, 32, 33, 34, 35, 36, 68, 31, 44, 33, 70, 72, 80, 88cgracgr 28572 . . . . . . . . 9 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))
9028, 29, 893jca 1125 . . . . . . . 8 (((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) ∧ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
9190ex 412 . . . . . . 7 ((((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ 𝑓 ∈ 𝑃) β†’ ((((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) β†’ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
9291reximdva 3162 . . . . . 6 (((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) β†’ (βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) β†’ βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
9392reximdva 3162 . . . . 5 ((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
9493imp 406 . . . 4 (((((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) ∧ π‘Ž ∈ 𝑃) ∧ 𝑐 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))) β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
951, 44, 2, 4, 8, 6, 14, 12axtgsegcon 28218 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘Ž ∈ 𝑃 (𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)))
961, 44, 2, 4, 8, 10, 14, 16axtgsegcon 28218 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘ ∈ 𝑃 (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))
97 reeanv 3220 . . . . . . . 8 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ↔ (βˆƒπ‘Ž ∈ 𝑃 (𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ βˆƒπ‘ ∈ 𝑃 (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))))
9895, 96, 97sylanbrc 582 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))))
991, 44, 2, 4, 14, 12, 8, 6axtgsegcon 28218 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)))
1001, 44, 2, 4, 14, 16, 8, 10axtgsegcon 28218 . . . . . . . 8 (πœ‘ β†’ βˆƒπ‘“ ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))
101 reeanv 3220 . . . . . . . 8 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ↔ (βˆƒπ‘‘ ∈ 𝑃 (𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ βˆƒπ‘“ ∈ 𝑃 (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))
10299, 100, 101sylanbrc 582 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))))
10398, 102jca 511 . . . . . 6 (πœ‘ β†’ (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
104 r19.41vv 3218 . . . . . . . . 9 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))))
105 ancom 460 . . . . . . . . . 10 ((((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
1061052rexbii 3123 . . . . . . . . 9 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
107 ancom 460 . . . . . . . . 9 ((βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))) ↔ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
108104, 106, 1073bitr3i 301 . . . . . . . 8 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
1091082rexbii 3123 . . . . . . 7 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
110 r19.41vv 3218 . . . . . . 7 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
111109, 110bitr2i 276 . . . . . 6 ((βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))) ↔ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
112103, 111sylib 217 . . . . 5 (πœ‘ β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
113112adantr 480 . . . 4 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
11494, 113reximddv2 3206 . . 3 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
11522, 27, 1143jca 1125 . 2 ((πœ‘ ∧ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©) β†’ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
116 df-3an 1086 . . 3 (((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) ↔ (((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸)) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
1174ad6antr 733 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐺 ∈ TarskiG)
11812ad6antr 733 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 ∈ 𝑃)
11914ad6antr 733 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐸 ∈ 𝑃)
12016ad6antr 733 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹 ∈ 𝑃)
1216ad6antr 733 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴 ∈ 𝑃)
1228ad6antr 733 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐡 ∈ 𝑃)
12310ad6antr 733 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 ∈ 𝑃)
124 simp-4r 781 . . . . . . . . . 10 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑦 ∈ 𝑃)
125 simp-5r 783 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ π‘₯ ∈ 𝑃)
126 simpllr 773 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑧 ∈ 𝑃)
127 simplr 766 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑑 ∈ 𝑃)
128 eqid 2726 . . . . . . . . . . . . . 14 (cgrGβ€˜πΊ) = (cgrGβ€˜πΊ)
129 simpr1 1191 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ ((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))))
130129simplld 765 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴 ∈ (𝐡𝐼π‘₯))
131 simpr2 1192 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))))
132131simplld 765 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 ∈ (𝐸𝐼𝑧))
1331, 44, 2, 117, 119, 118, 126, 132tgbtwncom 28242 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 ∈ (𝑧𝐼𝐸))
134131simplrd 767 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴))
135134eqcomd 2732 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝐴) = (𝐷 βˆ’ 𝑧))
1361, 44, 2, 117, 122, 121, 118, 126, 135tgcgrcomr 28232 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝐴) = (𝑧 βˆ’ 𝐷))
137129simplrd 767 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷))
1381, 44, 2, 117, 121, 125, 119, 118, 137tgcgrcomr 28232 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐴 βˆ’ π‘₯) = (𝐷 βˆ’ 𝐸))
1391, 44, 2, 117, 122, 121, 125, 126, 118, 119, 130, 133, 136, 138tgcgrextend 28239 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ π‘₯) = (𝑧 βˆ’ 𝐸))
1401, 44, 2, 117, 122, 125, 126, 119, 139tgcgrcoml 28233 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (π‘₯ βˆ’ 𝐡) = (𝑧 βˆ’ 𝐸))
141129simprld 769 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 ∈ (𝐡𝐼𝑦))
1421, 44, 2, 117, 122, 123, 124, 141tgbtwncom 28242 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 ∈ (𝑦𝐼𝐡))
143131simprld 769 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹 ∈ (𝐸𝐼𝑑))
144129simprrd 771 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))
1451, 44, 2, 117, 123, 124, 119, 120, 144tgcgrcoml 28233 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝑦 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐹))
146131simprrd 771 . . . . . . . . . . . . . . . . . 18 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))
147146eqcomd 2732 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝐢) = (𝐹 βˆ’ 𝑑))
1481, 44, 2, 117, 122, 123, 120, 127, 147tgcgrcoml 28233 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐢 βˆ’ 𝐡) = (𝐹 βˆ’ 𝑑))
1491, 44, 2, 117, 124, 123, 122, 119, 120, 127, 142, 143, 145, 148tgcgrextend 28239 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝑦 βˆ’ 𝐡) = (𝐸 βˆ’ 𝑑))
1501, 44, 2, 117, 124, 122, 119, 127, 149tgcgrcoml 28233 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝐡 βˆ’ 𝑦) = (𝐸 βˆ’ 𝑑))
151 simpr3 1193 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))
1521, 44, 2, 117, 125, 124, 126, 127, 151tgcgrcomlr 28234 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ (𝑦 βˆ’ π‘₯) = (𝑑 βˆ’ 𝑧))
1531, 44, 128, 117, 125, 122, 124, 126, 119, 127, 140, 150, 152trgcgr 28270 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ‘₯π΅π‘¦β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘§πΈπ‘‘β€βŸ©)
154 simp-6r 785 . . . . . . . . . . . . . . . . 17 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸)))
155154simprld 769 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷 β‰  𝐸)
1561, 44, 2, 117, 119, 118, 126, 132, 155tgbtwnne 28244 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐸 β‰  𝑧)
1571, 2, 3, 119, 126, 118, 117, 122, 132, 156, 155btwnhl1 28366 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐷((hlGβ€˜πΊ)β€˜πΈ)𝑧)
1581, 2, 3, 118, 126, 119, 117, 157hlcomd 28358 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑧((hlGβ€˜πΊ)β€˜πΈ)𝐷)
159154simprrd 771 . . . . . . . . . . . . . . . 16 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹 β‰  𝐸)
1601, 44, 2, 117, 119, 120, 127, 143, 159tgbtwnne 28244 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐸 β‰  𝑑)
1611, 2, 3, 119, 127, 120, 117, 122, 143, 160, 159btwnhl1 28366 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐹((hlGβ€˜πΊ)β€˜πΈ)𝑑)
1621, 2, 3, 120, 127, 119, 117, 161hlcomd 28358 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝑑((hlGβ€˜πΊ)β€˜πΈ)𝐹)
1631, 2, 3, 117, 125, 122, 124, 118, 119, 120, 126, 127, 153, 158, 162iscgrad 28565 . . . . . . . . . . . 12 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ‘₯π΅π‘¦β€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
1641, 2, 117, 3, 125, 122, 124, 118, 119, 120, 163cgracom 28576 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘₯π΅π‘¦β€βŸ©)
165154simplld 765 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴 β‰  𝐡)
1661, 44, 2, 117, 122, 121, 125, 130, 165tgbtwnne 28244 . . . . . . . . . . . 12 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐡 β‰  π‘₯)
1671, 2, 3, 122, 125, 121, 117, 121, 130, 166, 165btwnhl1 28366 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐴((hlGβ€˜πΊ)β€˜π΅)π‘₯)
1681, 2, 3, 117, 118, 119, 120, 125, 122, 124, 164, 121, 167cgrahl1 28570 . . . . . . . . . 10 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ΄π΅π‘¦β€βŸ©)
169154simplrd 767 . . . . . . . . . . . 12 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢 β‰  𝐡)
1701, 44, 2, 117, 122, 123, 124, 141, 169tgbtwnne 28244 . . . . . . . . . . 11 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐡 β‰  𝑦)
1711, 2, 3, 122, 124, 123, 117, 121, 141, 170, 169btwnhl1 28366 . . . . . . . . . 10 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ 𝐢((hlGβ€˜πΊ)β€˜π΅)𝑦)
1721, 2, 3, 117, 118, 119, 120, 121, 122, 124, 168, 123, 171cgrahl2 28571 . . . . . . . . 9 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ·πΈπΉβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ΄π΅πΆβ€βŸ©)
1731, 2, 117, 3, 118, 119, 120, 121, 122, 123, 172cgracom 28576 . . . . . . . 8 (((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
174173adantl3r 747 . . . . . . 7 ((((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) ∧ 𝑧 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
175 simpr 484 . . . . . . . 8 (((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
176 oveq2 7412 . . . . . . . . . . . . 13 (𝑑 = 𝑧 β†’ (𝐸𝐼𝑑) = (𝐸𝐼𝑧))
177176eleq2d 2813 . . . . . . . . . . . 12 (𝑑 = 𝑧 β†’ (𝐷 ∈ (𝐸𝐼𝑑) ↔ 𝐷 ∈ (𝐸𝐼𝑧)))
178 oveq2 7412 . . . . . . . . . . . . 13 (𝑑 = 𝑧 β†’ (𝐷 βˆ’ 𝑑) = (𝐷 βˆ’ 𝑧))
179178eqeq1d 2728 . . . . . . . . . . . 12 (𝑑 = 𝑧 β†’ ((𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴) ↔ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)))
180177, 179anbi12d 630 . . . . . . . . . . 11 (𝑑 = 𝑧 β†’ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ↔ (𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴))))
181180anbi1d 629 . . . . . . . . . 10 (𝑑 = 𝑧 β†’ (((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)))))
182 oveq1 7411 . . . . . . . . . . 11 (𝑑 = 𝑧 β†’ (𝑑 βˆ’ 𝑓) = (𝑧 βˆ’ 𝑓))
183182eqeq2d 2737 . . . . . . . . . 10 (𝑑 = 𝑧 β†’ ((π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓)))
184181, 1833anbi23d 1435 . . . . . . . . 9 (𝑑 = 𝑧 β†’ ((((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓))))
185 oveq2 7412 . . . . . . . . . . . . 13 (𝑓 = 𝑑 β†’ (𝐸𝐼𝑓) = (𝐸𝐼𝑑))
186185eleq2d 2813 . . . . . . . . . . . 12 (𝑓 = 𝑑 β†’ (𝐹 ∈ (𝐸𝐼𝑓) ↔ 𝐹 ∈ (𝐸𝐼𝑑)))
187 oveq2 7412 . . . . . . . . . . . . 13 (𝑓 = 𝑑 β†’ (𝐹 βˆ’ 𝑓) = (𝐹 βˆ’ 𝑑))
188187eqeq1d 2728 . . . . . . . . . . . 12 (𝑓 = 𝑑 β†’ ((𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢) ↔ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢)))
189186, 188anbi12d 630 . . . . . . . . . . 11 (𝑓 = 𝑑 β†’ ((𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢)) ↔ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))))
190189anbi2d 628 . . . . . . . . . 10 (𝑓 = 𝑑 β†’ (((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ↔ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢)))))
191 oveq2 7412 . . . . . . . . . . 11 (𝑓 = 𝑑 β†’ (𝑧 βˆ’ 𝑓) = (𝑧 βˆ’ 𝑑))
192191eqeq2d 2737 . . . . . . . . . 10 (𝑓 = 𝑑 β†’ ((π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑)))
193190, 1923anbi23d 1435 . . . . . . . . 9 (𝑓 = 𝑑 β†’ ((((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑))))
194184, 193cbvrex2vw 3233 . . . . . . . 8 (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑)))
195175, 194sylib 217 . . . . . . 7 (((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘§ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑧) ∧ (𝐷 βˆ’ 𝑧) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑑) ∧ (𝐹 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑑)))
196174, 195r19.29vva 3207 . . . . . 6 (((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
197196adantl3r 747 . . . . 5 ((((((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
198 simpr 484 . . . . . 6 (((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
199 oveq2 7412 . . . . . . . . . . . 12 (π‘Ž = π‘₯ β†’ (π΅πΌπ‘Ž) = (𝐡𝐼π‘₯))
200199eleq2d 2813 . . . . . . . . . . 11 (π‘Ž = π‘₯ β†’ (𝐴 ∈ (π΅πΌπ‘Ž) ↔ 𝐴 ∈ (𝐡𝐼π‘₯)))
201 oveq2 7412 . . . . . . . . . . . 12 (π‘Ž = π‘₯ β†’ (𝐴 βˆ’ π‘Ž) = (𝐴 βˆ’ π‘₯))
202201eqeq1d 2728 . . . . . . . . . . 11 (π‘Ž = π‘₯ β†’ ((𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷) ↔ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)))
203200, 202anbi12d 630 . . . . . . . . . 10 (π‘Ž = π‘₯ β†’ ((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ↔ (𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷))))
204203anbi1d 629 . . . . . . . . 9 (π‘Ž = π‘₯ β†’ (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ↔ ((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)))))
205 oveq1 7411 . . . . . . . . . 10 (π‘Ž = π‘₯ β†’ (π‘Ž βˆ’ 𝑐) = (π‘₯ βˆ’ 𝑐))
206205eqeq1d 2728 . . . . . . . . 9 (π‘Ž = π‘₯ β†’ ((π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))
207204, 2063anbi13d 1434 . . . . . . . 8 (π‘Ž = π‘₯ β†’ ((((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
2082072rexbidv 3213 . . . . . . 7 (π‘Ž = π‘₯ β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))))
209 oveq2 7412 . . . . . . . . . . . 12 (𝑐 = 𝑦 β†’ (𝐡𝐼𝑐) = (𝐡𝐼𝑦))
210209eleq2d 2813 . . . . . . . . . . 11 (𝑐 = 𝑦 β†’ (𝐢 ∈ (𝐡𝐼𝑐) ↔ 𝐢 ∈ (𝐡𝐼𝑦)))
211 oveq2 7412 . . . . . . . . . . . 12 (𝑐 = 𝑦 β†’ (𝐢 βˆ’ 𝑐) = (𝐢 βˆ’ 𝑦))
212211eqeq1d 2728 . . . . . . . . . . 11 (𝑐 = 𝑦 β†’ ((𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹) ↔ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹)))
213210, 212anbi12d 630 . . . . . . . . . 10 (𝑐 = 𝑦 β†’ ((𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹)) ↔ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))))
214213anbi2d 628 . . . . . . . . 9 (𝑐 = 𝑦 β†’ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ↔ ((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹)))))
215 oveq2 7412 . . . . . . . . . 10 (𝑐 = 𝑦 β†’ (π‘₯ βˆ’ 𝑐) = (π‘₯ βˆ’ 𝑦))
216215eqeq1d 2728 . . . . . . . . 9 (𝑐 = 𝑦 β†’ ((π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓) ↔ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
217214, 2163anbi13d 1434 . . . . . . . 8 (𝑐 = 𝑦 β†’ ((((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))))
2182172rexbidv 3213 . . . . . . 7 (𝑐 = 𝑦 β†’ (βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓))))
219208, 218cbvrex2vw 3233 . . . . . 6 (βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)) ↔ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
220198, 219sylib 217 . . . . 5 (((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (𝐡𝐼π‘₯) ∧ (𝐴 βˆ’ π‘₯) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑦) ∧ (𝐢 βˆ’ 𝑦) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘₯ βˆ’ 𝑦) = (𝑑 βˆ’ 𝑓)))
221197, 220r19.29vva 3207 . . . 4 (((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸))) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
222221anasss 466 . . 3 ((πœ‘ ∧ (((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸)) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
223116, 222sylan2b 593 . 2 ((πœ‘ ∧ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ©)
224115, 223impbida 798 1 (πœ‘ β†’ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπΉβ€βŸ© ↔ ((𝐴 β‰  𝐡 ∧ 𝐢 β‰  𝐡) ∧ (𝐷 β‰  𝐸 ∧ 𝐹 β‰  𝐸) ∧ βˆƒπ‘Ž ∈ 𝑃 βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 βˆƒπ‘“ ∈ 𝑃 (((𝐴 ∈ (π΅πΌπ‘Ž) ∧ (𝐴 βˆ’ π‘Ž) = (𝐸 βˆ’ 𝐷)) ∧ (𝐢 ∈ (𝐡𝐼𝑐) ∧ (𝐢 βˆ’ 𝑐) = (𝐸 βˆ’ 𝐹))) ∧ ((𝐷 ∈ (𝐸𝐼𝑑) ∧ (𝐷 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)) ∧ (𝐹 ∈ (𝐸𝐼𝑓) ∧ (𝐹 βˆ’ 𝑓) = (𝐡 βˆ’ 𝐢))) ∧ (π‘Ž βˆ’ 𝑐) = (𝑑 βˆ’ 𝑓)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2934  βˆƒwrex 3064   class class class wbr 5141  β€˜cfv 6536  (class class class)co 7404  βŸ¨β€œcs3 14796  Basecbs 17150  distcds 17212  TarskiGcstrkg 28181  Itvcitv 28187  cgrGccgrg 28264  hlGchlg 28354  cgrAccgra 28561
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 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-oadd 8468  df-er 8702  df-map 8821  df-pm 8822  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-dju 9895  df-card 9933  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11447  df-neg 11448  df-nn 12214  df-2 12276  df-3 12277  df-n0 12474  df-xnn0 12546  df-z 12560  df-uz 12824  df-fz 13488  df-fzo 13631  df-hash 14293  df-word 14468  df-concat 14524  df-s1 14549  df-s2 14802  df-s3 14803  df-trkgc 28202  df-trkgb 28203  df-trkgcb 28204  df-trkg 28207  df-cgrg 28265  df-leg 28337  df-hlg 28355  df-cgra 28562
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator