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

Theorem acopyeu 28520
Description: Angle construction. Theorem 11.15 of [Schwabhauser] p. 98. This is Hilbert's axiom III.4 for geometry. Akin to a uniqueness theorem, this states that if two points 𝑋 and π‘Œ both fulfill the conditions, then they are on the same half-line. (Contributed by Thierry Arnoux, 9-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 (πœ‘ β†’ 𝐹 ∈ 𝑃)
acopy.l 𝐿 = (LineGβ€˜πΊ)
acopy.1 (πœ‘ β†’ Β¬ (𝐴 ∈ (𝐡𝐿𝐢) ∨ 𝐡 = 𝐢))
acopy.2 (πœ‘ β†’ Β¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
acopyeu.x (πœ‘ β†’ 𝑋 ∈ 𝑃)
acopyeu.y (πœ‘ β†’ π‘Œ ∈ 𝑃)
acopyeu.k 𝐾 = (hlGβ€˜πΊ)
acopyeu.1 (πœ‘ β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπ‘‹β€βŸ©)
acopyeu.2 (πœ‘ β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπ‘Œβ€βŸ©)
acopyeu.3 (πœ‘ β†’ 𝑋((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝐹)
acopyeu.4 (πœ‘ β†’ π‘Œ((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝐹)
Assertion
Ref Expression
acopyeu (πœ‘ β†’ 𝑋(πΎβ€˜πΈ)π‘Œ)

Proof of Theorem acopyeu
Dummy variables π‘Ž 𝑑 𝑑 π‘₯ 𝑦 𝑏 𝑒 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfcgra2.p . . . 4 𝑃 = (Baseβ€˜πΊ)
2 dfcgra2.i . . . 4 𝐼 = (Itvβ€˜πΊ)
3 acopyeu.k . . . 4 𝐾 = (hlGβ€˜πΊ)
4 acopyeu.x . . . . . 6 (πœ‘ β†’ 𝑋 ∈ 𝑃)
54ad2antrr 723 . . . . 5 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝑋 ∈ 𝑃)
65ad3antrrr 727 . . . 4 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑋 ∈ 𝑃)
7 simplr 766 . . . 4 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑦 ∈ 𝑃)
8 acopyeu.y . . . . . 6 (πœ‘ β†’ π‘Œ ∈ 𝑃)
98ad2antrr 723 . . . . 5 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ π‘Œ ∈ 𝑃)
109ad3antrrr 727 . . . 4 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ π‘Œ ∈ 𝑃)
11 dfcgra2.g . . . . . 6 (πœ‘ β†’ 𝐺 ∈ TarskiG)
1211ad2antrr 723 . . . . 5 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝐺 ∈ TarskiG)
1312ad3antrrr 727 . . . 4 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝐺 ∈ TarskiG)
14 dfcgra2.e . . . . . 6 (πœ‘ β†’ 𝐸 ∈ 𝑃)
1514ad2antrr 723 . . . . 5 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝐸 ∈ 𝑃)
1615ad3antrrr 727 . . . 4 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝐸 ∈ 𝑃)
17 dfcgra2.m . . . . . . 7 βˆ’ = (distβ€˜πΊ)
18 acopy.l . . . . . . 7 𝐿 = (LineGβ€˜πΊ)
19 dfcgra2.a . . . . . . . . 9 (πœ‘ β†’ 𝐴 ∈ 𝑃)
2019ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝐴 ∈ 𝑃)
2120ad3antrrr 727 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝐴 ∈ 𝑃)
22 dfcgra2.b . . . . . . . . 9 (πœ‘ β†’ 𝐡 ∈ 𝑃)
2322ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝐡 ∈ 𝑃)
2423ad3antrrr 727 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝐡 ∈ 𝑃)
25 dfcgra2.c . . . . . . . . 9 (πœ‘ β†’ 𝐢 ∈ 𝑃)
2625ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝐢 ∈ 𝑃)
2726ad3antrrr 727 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝐢 ∈ 𝑃)
28 simplr 766 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝑑 ∈ 𝑃)
2928ad3antrrr 727 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑑 ∈ 𝑃)
30 dfcgra2.f . . . . . . . . 9 (πœ‘ β†’ 𝐹 ∈ 𝑃)
3130ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝐹 ∈ 𝑃)
3231ad3antrrr 727 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝐹 ∈ 𝑃)
33 acopy.1 . . . . . . . . 9 (πœ‘ β†’ Β¬ (𝐴 ∈ (𝐡𝐿𝐢) ∨ 𝐡 = 𝐢))
3433ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ Β¬ (𝐴 ∈ (𝐡𝐿𝐢) ∨ 𝐡 = 𝐢))
3534ad3antrrr 727 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ (𝐴 ∈ (𝐡𝐿𝐢) ∨ 𝐡 = 𝐢))
36 dfcgra2.d . . . . . . . . . 10 (πœ‘ β†’ 𝐷 ∈ 𝑃)
3736ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝐷 ∈ 𝑃)
38 acopy.2 . . . . . . . . . 10 (πœ‘ β†’ Β¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
3938ad2antrr 723 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ Β¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
40 simprl 768 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝑑(πΎβ€˜πΈ)𝐷)
411, 2, 3, 28, 37, 15, 12, 18, 40hlln 28293 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝑑 ∈ (𝐷𝐿𝐸))
421, 2, 3, 28, 37, 15, 12, 40hlne1 28291 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝑑 β‰  𝐸)
431, 2, 18, 12, 37, 15, 31, 28, 39, 41, 42ncolncol 28332 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ Β¬ (𝑑 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
4443ad3antrrr 727 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ (𝑑 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
45 simprr 770 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))
461, 17, 2, 12, 15, 28, 23, 20, 45tgcgrcomlr 28166 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ (𝑑 βˆ’ 𝐸) = (𝐴 βˆ’ 𝐡))
4746eqcomd 2737 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ (𝐴 βˆ’ 𝐡) = (𝑑 βˆ’ 𝐸))
4847ad3antrrr 727 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ (𝐴 βˆ’ 𝐡) = (𝑑 βˆ’ 𝐸))
49 simpl 482 . . . . . . . . . . 11 ((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) β†’ 𝑒 = π‘Ž)
5049eleq1d 2817 . . . . . . . . . 10 ((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) β†’ (𝑒 ∈ (𝑃 βˆ– (𝑑𝐿𝐸)) ↔ π‘Ž ∈ (𝑃 βˆ– (𝑑𝐿𝐸))))
51 simpr 484 . . . . . . . . . . 11 ((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) β†’ 𝑣 = 𝑏)
5251eleq1d 2817 . . . . . . . . . 10 ((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) β†’ (𝑣 ∈ (𝑃 βˆ– (𝑑𝐿𝐸)) ↔ 𝑏 ∈ (𝑃 βˆ– (𝑑𝐿𝐸))))
5350, 52anbi12d 630 . . . . . . . . 9 ((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) β†’ ((𝑒 ∈ (𝑃 βˆ– (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 βˆ– (𝑑𝐿𝐸))) ↔ (π‘Ž ∈ (𝑃 βˆ– (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 βˆ– (𝑑𝐿𝐸)))))
54 simpr 484 . . . . . . . . . . 11 (((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) ∧ 𝑀 = 𝑑) β†’ 𝑀 = 𝑑)
55 simpll 764 . . . . . . . . . . . 12 (((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) ∧ 𝑀 = 𝑑) β†’ 𝑒 = π‘Ž)
56 simplr 766 . . . . . . . . . . . 12 (((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) ∧ 𝑀 = 𝑑) β†’ 𝑣 = 𝑏)
5755, 56oveq12d 7430 . . . . . . . . . . 11 (((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) ∧ 𝑀 = 𝑑) β†’ (𝑒𝐼𝑣) = (π‘ŽπΌπ‘))
5854, 57eleq12d 2826 . . . . . . . . . 10 (((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) ∧ 𝑀 = 𝑑) β†’ (𝑀 ∈ (𝑒𝐼𝑣) ↔ 𝑑 ∈ (π‘ŽπΌπ‘)))
5958cbvrexdva 3236 . . . . . . . . 9 ((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) β†’ (βˆƒπ‘€ ∈ (𝑑𝐿𝐸)𝑀 ∈ (𝑒𝐼𝑣) ↔ βˆƒπ‘‘ ∈ (𝑑𝐿𝐸)𝑑 ∈ (π‘ŽπΌπ‘)))
6053, 59anbi12d 630 . . . . . . . 8 ((𝑒 = π‘Ž ∧ 𝑣 = 𝑏) β†’ (((𝑒 ∈ (𝑃 βˆ– (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 βˆ– (𝑑𝐿𝐸))) ∧ βˆƒπ‘€ ∈ (𝑑𝐿𝐸)𝑀 ∈ (𝑒𝐼𝑣)) ↔ ((π‘Ž ∈ (𝑃 βˆ– (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 βˆ– (𝑑𝐿𝐸))) ∧ βˆƒπ‘‘ ∈ (𝑑𝐿𝐸)𝑑 ∈ (π‘ŽπΌπ‘))))
6160cbvopabv 5221 . . . . . . 7 {βŸ¨π‘’, π‘£βŸ© ∣ ((𝑒 ∈ (𝑃 βˆ– (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 βˆ– (𝑑𝐿𝐸))) ∧ βˆƒπ‘€ ∈ (𝑑𝐿𝐸)𝑀 ∈ (𝑒𝐼𝑣))} = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 βˆ– (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 βˆ– (𝑑𝐿𝐸))) ∧ βˆƒπ‘‘ ∈ (𝑑𝐿𝐸)𝑑 ∈ (π‘ŽπΌπ‘))}
62 simpllr 773 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ π‘₯ ∈ 𝑃)
63 simprll 776 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ©)
64 simprrl 778 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ©)
651, 2, 18, 12, 28, 15, 42tgelrnln 28316 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ (𝑑𝐿𝐸) ∈ ran 𝐿)
6665ad3antrrr 727 . . . . . . . 8 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ (𝑑𝐿𝐸) ∈ ran 𝐿)
671, 2, 18, 12, 28, 15, 42tglinerflx2 28320 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝐸 ∈ (𝑑𝐿𝐸))
6867ad3antrrr 727 . . . . . . . . 9 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝐸 ∈ (𝑑𝐿𝐸))
6937ad3antrrr 727 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝐷 ∈ 𝑃)
70 acopyeu.1 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπ‘‹β€βŸ©)
711, 18, 2, 11, 22, 25, 19, 33ncolrot2 28249 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ Β¬ (𝐢 ∈ (𝐴𝐿𝐡) ∨ 𝐴 = 𝐡))
721, 2, 17, 11, 19, 22, 25, 36, 14, 4, 70, 18, 71cgrancol 28515 . . . . . . . . . . . . . . 15 (πœ‘ β†’ Β¬ (𝑋 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
731, 18, 2, 11, 36, 14, 4, 72ncolcom 28247 . . . . . . . . . . . . . 14 (πœ‘ β†’ Β¬ (𝑋 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
7473ad5antr 731 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ (𝑋 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
75 simprlr 777 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ π‘₯(πΎβ€˜πΈ)𝑋)
761, 2, 3, 62, 6, 16, 13, 18, 75hlln 28293 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ π‘₯ ∈ (𝑋𝐿𝐸))
771, 2, 3, 62, 6, 16, 13, 75hlne1 28291 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ π‘₯ β‰  𝐸)
781, 2, 18, 13, 6, 16, 69, 62, 74, 76, 77ncolncol 28332 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ (π‘₯ ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
791, 18, 2, 13, 16, 69, 62, 78ncolcom 28247 . . . . . . . . . . 11 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ (π‘₯ ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
80 pm2.45 879 . . . . . . . . . . 11 (Β¬ (π‘₯ ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) β†’ Β¬ π‘₯ ∈ (𝐷𝐿𝐸))
8179, 80syl 17 . . . . . . . . . 10 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ π‘₯ ∈ (𝐷𝐿𝐸))
821, 2, 18, 11, 36, 14, 30, 38ncolne1 28311 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐷 β‰  𝐸)
831, 2, 18, 11, 36, 14, 82tgelrnln 28316 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐷𝐿𝐸) ∈ ran 𝐿)
8483ad2antrr 723 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ (𝐷𝐿𝐸) ∈ ran 𝐿)
851, 2, 18, 11, 36, 14, 82tglinerflx2 28320 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐸 ∈ (𝐷𝐿𝐸))
8685ad2antrr 723 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝐸 ∈ (𝐷𝐿𝐸))
871, 2, 18, 12, 28, 15, 42, 42, 84, 41, 86tglinethru 28322 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ (𝐷𝐿𝐸) = (𝑑𝐿𝐸))
8887ad3antrrr 727 . . . . . . . . . 10 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ (𝐷𝐿𝐸) = (𝑑𝐿𝐸))
8981, 88neleqtrd 2854 . . . . . . . . 9 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ π‘₯ ∈ (𝑑𝐿𝐸))
901, 2, 18, 13, 66, 16, 61, 3, 68, 62, 6, 89, 75hphl 28457 . . . . . . . 8 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ π‘₯((hpGβ€˜πΊ)β€˜(𝑑𝐿𝐸))𝑋)
9187fveq2d 6895 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ ((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸)) = ((hpGβ€˜πΊ)β€˜(𝑑𝐿𝐸)))
9291ad3antrrr 727 . . . . . . . . 9 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ ((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸)) = ((hpGβ€˜πΊ)β€˜(𝑑𝐿𝐸)))
93 acopyeu.3 . . . . . . . . . 10 (πœ‘ β†’ 𝑋((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝐹)
9493ad5antr 731 . . . . . . . . 9 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑋((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝐹)
9592, 94breqdi 5163 . . . . . . . 8 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑋((hpGβ€˜πΊ)β€˜(𝑑𝐿𝐸))𝐹)
961, 2, 18, 13, 66, 62, 61, 6, 90, 32, 95hpgtr 28454 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ π‘₯((hpGβ€˜πΊ)β€˜(𝑑𝐿𝐸))𝐹)
97 acopyeu.2 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπ‘Œβ€βŸ©)
981, 2, 17, 11, 19, 22, 25, 36, 14, 8, 97, 18, 71cgrancol 28515 . . . . . . . . . . . . . . 15 (πœ‘ β†’ Β¬ (π‘Œ ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
991, 18, 2, 11, 36, 14, 8, 98ncolcom 28247 . . . . . . . . . . . . . 14 (πœ‘ β†’ Β¬ (π‘Œ ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
10099ad5antr 731 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ (π‘Œ ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
101 simprrr 779 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑦(πΎβ€˜πΈ)π‘Œ)
1021, 2, 3, 7, 10, 16, 13, 18, 101hlln 28293 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑦 ∈ (π‘ŒπΏπΈ))
1031, 2, 3, 7, 10, 16, 13, 101hlne1 28291 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑦 β‰  𝐸)
1041, 2, 18, 13, 10, 16, 69, 7, 100, 102, 103ncolncol 28332 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ (𝑦 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
1051, 18, 2, 13, 16, 69, 7, 104ncolcom 28247 . . . . . . . . . . 11 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
106 pm2.45 879 . . . . . . . . . . 11 (Β¬ (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) β†’ Β¬ 𝑦 ∈ (𝐷𝐿𝐸))
107105, 106syl 17 . . . . . . . . . 10 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ 𝑦 ∈ (𝐷𝐿𝐸))
108107, 88neleqtrd 2854 . . . . . . . . 9 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ Β¬ 𝑦 ∈ (𝑑𝐿𝐸))
1091, 2, 18, 13, 66, 16, 61, 3, 68, 7, 10, 108, 101hphl 28457 . . . . . . . 8 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑦((hpGβ€˜πΊ)β€˜(𝑑𝐿𝐸))π‘Œ)
110 acopyeu.4 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝐹)
111110ad5antr 731 . . . . . . . . 9 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ π‘Œ((hpGβ€˜πΊ)β€˜(𝐷𝐿𝐸))𝐹)
11292, 111breqdi 5163 . . . . . . . 8 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ π‘Œ((hpGβ€˜πΊ)β€˜(𝑑𝐿𝐸))𝐹)
1131, 2, 18, 13, 66, 7, 61, 10, 109, 32, 112hpgtr 28454 . . . . . . 7 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑦((hpGβ€˜πΊ)β€˜(𝑑𝐿𝐸))𝐹)
1141, 17, 2, 18, 3, 13, 21, 24, 27, 29, 16, 32, 35, 44, 48, 61, 62, 7, 63, 64, 96, 113trgcopyeulem 28491 . . . . . 6 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ π‘₯ = 𝑦)
115114, 75eqbrtrrd 5172 . . . . 5 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑦(πΎβ€˜πΈ)𝑋)
1161, 2, 3, 7, 6, 16, 13, 115hlcomd 28290 . . . 4 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑋(πΎβ€˜πΈ)𝑦)
1171, 2, 3, 6, 7, 10, 13, 16, 116, 101hltr 28296 . . 3 ((((((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))) β†’ 𝑋(πΎβ€˜πΈ)π‘Œ)
11870ad2antrr 723 . . . . . 6 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπ‘‹β€βŸ©)
1191, 2, 3, 12, 20, 23, 26, 37, 15, 5, 118, 28, 40cgrahl1 28502 . . . . 5 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘‹β€βŸ©)
1201, 2, 18, 11, 19, 22, 25, 33ncolne1 28311 . . . . . . 7 (πœ‘ β†’ 𝐴 β‰  𝐡)
121120ad2antrr 723 . . . . . 6 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝐴 β‰  𝐡)
1221, 2, 3, 12, 20, 23, 26, 28, 15, 5, 17, 121, 47iscgra1 28496 . . . . 5 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘‹β€βŸ© ↔ βˆƒπ‘₯ ∈ 𝑃 (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋)))
123119, 122mpbid 231 . . . 4 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ βˆƒπ‘₯ ∈ 𝑃 (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋))
12497ad2antrr 723 . . . . . 6 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ·πΈπ‘Œβ€βŸ©)
1251, 2, 3, 12, 20, 23, 26, 37, 15, 9, 124, 28, 40cgrahl1 28502 . . . . 5 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘Œβ€βŸ©)
1261, 2, 3, 12, 20, 23, 26, 28, 15, 9, 17, 121, 47iscgra1 28496 . . . . 5 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrAβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘Œβ€βŸ© ↔ βˆƒπ‘¦ ∈ 𝑃 (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ)))
127125, 126mpbid 231 . . . 4 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ βˆƒπ‘¦ ∈ 𝑃 (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ))
128 reeanv 3225 . . . 4 (βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ)) ↔ (βˆƒπ‘₯ ∈ 𝑃 (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ βˆƒπ‘¦ ∈ 𝑃 (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ)))
129123, 127, 128sylanbrc 582 . . 3 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘₯β€βŸ© ∧ π‘₯(πΎβ€˜πΈ)𝑋) ∧ (βŸ¨β€œπ΄π΅πΆβ€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπ‘‘πΈπ‘¦β€βŸ© ∧ 𝑦(πΎβ€˜πΈ)π‘Œ)))
130117, 129r19.29vva 3212 . 2 (((πœ‘ ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴))) β†’ 𝑋(πΎβ€˜πΈ)π‘Œ)
131120necomd 2995 . . 3 (πœ‘ β†’ 𝐡 β‰  𝐴)
1321, 2, 3, 14, 22, 19, 11, 36, 17, 82, 131hlcgrex 28302 . 2 (πœ‘ β†’ βˆƒπ‘‘ ∈ 𝑃 (𝑑(πΎβ€˜πΈ)𝐷 ∧ (𝐸 βˆ’ 𝑑) = (𝐡 βˆ’ 𝐴)))
133130, 132r19.29a 3161 1 (πœ‘ β†’ 𝑋(πΎβ€˜πΈ)π‘Œ)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   ∨ wo 844   = wceq 1540   ∈ wcel 2105   β‰  wne 2939  βˆƒwrex 3069   βˆ– cdif 3945   class class class wbr 5148  {copab 5210  ran crn 5677  β€˜cfv 6543  (class class class)co 7412  βŸ¨β€œcs3 14800  Basecbs 17151  distcds 17213  TarskiGcstrkg 28113  Itvcitv 28119  LineGclng 28120  cgrGccgrg 28196  hlGchlg 28286  hpGchpg 28443  cgrAccgra 28493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-1o 8472  df-oadd 8476  df-er 8709  df-map 8828  df-pm 8829  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-dju 9902  df-card 9940  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-nn 12220  df-2 12282  df-3 12283  df-n0 12480  df-xnn0 12552  df-z 12566  df-uz 12830  df-fz 13492  df-fzo 13635  df-hash 14298  df-word 14472  df-concat 14528  df-s1 14553  df-s2 14806  df-s3 14807  df-trkgc 28134  df-trkgb 28135  df-trkgcb 28136  df-trkgld 28138  df-trkg 28139  df-cgrg 28197  df-leg 28269  df-hlg 28287  df-mir 28339  df-rag 28380  df-perpg 28382  df-hpg 28444  df-mid 28460  df-lmi 28461  df-cgra 28494
This theorem is referenced by:  tgasa1  28544
  Copyright terms: Public domain W3C validator