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

Theorem acopyeu 27950
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 724 . . . . 5 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝑋𝑃)
65ad3antrrr 728 . . . 4 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑋𝑃)
7 simplr 767 . . . 4 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑦𝑃)
8 acopyeu.y . . . . . 6 (𝜑𝑌𝑃)
98ad2antrr 724 . . . . 5 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝑌𝑃)
109ad3antrrr 728 . . . 4 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑌𝑃)
11 dfcgra2.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
1211ad2antrr 724 . . . . 5 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝐺 ∈ TarskiG)
1312ad3antrrr 728 . . . 4 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝐺 ∈ TarskiG)
14 dfcgra2.e . . . . . 6 (𝜑𝐸𝑃)
1514ad2antrr 724 . . . . 5 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝐸𝑃)
1615ad3antrrr 728 . . . 4 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝐸𝑃)
17 dfcgra2.m . . . . . . 7 = (dist‘𝐺)
18 acopy.l . . . . . . 7 𝐿 = (LineG‘𝐺)
19 dfcgra2.a . . . . . . . . 9 (𝜑𝐴𝑃)
2019ad2antrr 724 . . . . . . . 8 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝐴𝑃)
2120ad3antrrr 728 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝐴𝑃)
22 dfcgra2.b . . . . . . . . 9 (𝜑𝐵𝑃)
2322ad2antrr 724 . . . . . . . 8 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝐵𝑃)
2423ad3antrrr 728 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝐵𝑃)
25 dfcgra2.c . . . . . . . . 9 (𝜑𝐶𝑃)
2625ad2antrr 724 . . . . . . . 8 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝐶𝑃)
2726ad3antrrr 728 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝐶𝑃)
28 simplr 767 . . . . . . . 8 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝑑𝑃)
2928ad3antrrr 728 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑑𝑃)
30 dfcgra2.f . . . . . . . . 9 (𝜑𝐹𝑃)
3130ad2antrr 724 . . . . . . . 8 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝐹𝑃)
3231ad3antrrr 728 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝐹𝑃)
33 acopy.1 . . . . . . . . 9 (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
3433ad2antrr 724 . . . . . . . 8 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
3534ad3antrrr 728 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
36 dfcgra2.d . . . . . . . . . 10 (𝜑𝐷𝑃)
3736ad2antrr 724 . . . . . . . . 9 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝐷𝑃)
38 acopy.2 . . . . . . . . . 10 (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
3938ad2antrr 724 . . . . . . . . 9 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
40 simprl 769 . . . . . . . . . 10 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝑑(𝐾𝐸)𝐷)
411, 2, 3, 28, 37, 15, 12, 18, 40hlln 27723 . . . . . . . . 9 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝑑 ∈ (𝐷𝐿𝐸))
421, 2, 3, 28, 37, 15, 12, 40hlne1 27721 . . . . . . . . 9 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝑑𝐸)
431, 2, 18, 12, 37, 15, 31, 28, 39, 41, 42ncolncol 27762 . . . . . . . 8 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ¬ (𝑑 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
4443ad3antrrr 728 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ¬ (𝑑 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
45 simprr 771 . . . . . . . . . 10 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → (𝐸 𝑑) = (𝐵 𝐴))
461, 17, 2, 12, 15, 28, 23, 20, 45tgcgrcomlr 27596 . . . . . . . . 9 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → (𝑑 𝐸) = (𝐴 𝐵))
4746eqcomd 2737 . . . . . . . 8 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → (𝐴 𝐵) = (𝑑 𝐸))
4847ad3antrrr 728 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → (𝐴 𝐵) = (𝑑 𝐸))
49 simpl 483 . . . . . . . . . . 11 ((𝑢 = 𝑎𝑣 = 𝑏) → 𝑢 = 𝑎)
5049eleq1d 2817 . . . . . . . . . 10 ((𝑢 = 𝑎𝑣 = 𝑏) → (𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ↔ 𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸))))
51 simpr 485 . . . . . . . . . . 11 ((𝑢 = 𝑎𝑣 = 𝑏) → 𝑣 = 𝑏)
5251eleq1d 2817 . . . . . . . . . 10 ((𝑢 = 𝑎𝑣 = 𝑏) → (𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ↔ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸))))
5350, 52anbi12d 631 . . . . . . . . 9 ((𝑢 = 𝑎𝑣 = 𝑏) → ((𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ↔ (𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸)))))
54 simpr 485 . . . . . . . . . . 11 (((𝑢 = 𝑎𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → 𝑤 = 𝑡)
55 simpll 765 . . . . . . . . . . . 12 (((𝑢 = 𝑎𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → 𝑢 = 𝑎)
56 simplr 767 . . . . . . . . . . . 12 (((𝑢 = 𝑎𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → 𝑣 = 𝑏)
5755, 56oveq12d 7411 . . . . . . . . . . 11 (((𝑢 = 𝑎𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → (𝑢𝐼𝑣) = (𝑎𝐼𝑏))
5854, 57eleq12d 2826 . . . . . . . . . 10 (((𝑢 = 𝑎𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → (𝑤 ∈ (𝑢𝐼𝑣) ↔ 𝑡 ∈ (𝑎𝐼𝑏)))
5958cbvrexdva 3236 . . . . . . . . 9 ((𝑢 = 𝑎𝑣 = 𝑏) → (∃𝑤 ∈ (𝑑𝐿𝐸)𝑤 ∈ (𝑢𝐼𝑣) ↔ ∃𝑡 ∈ (𝑑𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏)))
6053, 59anbi12d 631 . . . . . . . 8 ((𝑢 = 𝑎𝑣 = 𝑏) → (((𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑤 ∈ (𝑑𝐿𝐸)𝑤 ∈ (𝑢𝐼𝑣)) ↔ ((𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑡 ∈ (𝑑𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏))))
6160cbvopabv 5214 . . . . . . 7 {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑤 ∈ (𝑑𝐿𝐸)𝑤 ∈ (𝑢𝐼𝑣))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑡 ∈ (𝑑𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏))}
62 simpllr 774 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑥𝑃)
63 simprll 777 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩)
64 simprrl 779 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩)
651, 2, 18, 12, 28, 15, 42tgelrnln 27746 . . . . . . . . 9 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → (𝑑𝐿𝐸) ∈ ran 𝐿)
6665ad3antrrr 728 . . . . . . . 8 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → (𝑑𝐿𝐸) ∈ ran 𝐿)
671, 2, 18, 12, 28, 15, 42tglinerflx2 27750 . . . . . . . . . 10 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝐸 ∈ (𝑑𝐿𝐸))
6867ad3antrrr 728 . . . . . . . . 9 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝐸 ∈ (𝑑𝐿𝐸))
6937ad3antrrr 728 . . . . . . . . . . . 12 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝐷𝑃)
70 acopyeu.1 . . . . . . . . . . . . . . . 16 (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑋”⟩)
711, 18, 2, 11, 22, 25, 19, 33ncolrot2 27679 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
721, 2, 17, 11, 19, 22, 25, 36, 14, 4, 70, 18, 71cgrancol 27945 . . . . . . . . . . . . . . 15 (𝜑 → ¬ (𝑋 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
731, 18, 2, 11, 36, 14, 4, 72ncolcom 27677 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑋 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
7473ad5antr 732 . . . . . . . . . . . . 13 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ¬ (𝑋 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
75 simprlr 778 . . . . . . . . . . . . . 14 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑥(𝐾𝐸)𝑋)
761, 2, 3, 62, 6, 16, 13, 18, 75hlln 27723 . . . . . . . . . . . . 13 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑥 ∈ (𝑋𝐿𝐸))
771, 2, 3, 62, 6, 16, 13, 75hlne1 27721 . . . . . . . . . . . . 13 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑥𝐸)
781, 2, 18, 13, 6, 16, 69, 62, 74, 76, 77ncolncol 27762 . . . . . . . . . . . 12 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ¬ (𝑥 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
791, 18, 2, 13, 16, 69, 62, 78ncolcom 27677 . . . . . . . . . . 11 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ¬ (𝑥 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
80 pm2.45 880 . . . . . . . . . . 11 (¬ (𝑥 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) → ¬ 𝑥 ∈ (𝐷𝐿𝐸))
8179, 80syl 17 . . . . . . . . . 10 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ¬ 𝑥 ∈ (𝐷𝐿𝐸))
821, 2, 18, 11, 36, 14, 30, 38ncolne1 27741 . . . . . . . . . . . . . 14 (𝜑𝐷𝐸)
831, 2, 18, 11, 36, 14, 82tgelrnln 27746 . . . . . . . . . . . . 13 (𝜑 → (𝐷𝐿𝐸) ∈ ran 𝐿)
8483ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → (𝐷𝐿𝐸) ∈ ran 𝐿)
851, 2, 18, 11, 36, 14, 82tglinerflx2 27750 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ (𝐷𝐿𝐸))
8685ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝐸 ∈ (𝐷𝐿𝐸))
871, 2, 18, 12, 28, 15, 42, 42, 84, 41, 86tglinethru 27752 . . . . . . . . . . 11 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → (𝐷𝐿𝐸) = (𝑑𝐿𝐸))
8887ad3antrrr 728 . . . . . . . . . 10 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → (𝐷𝐿𝐸) = (𝑑𝐿𝐸))
8981, 88neleqtrd 2854 . . . . . . . . 9 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ¬ 𝑥 ∈ (𝑑𝐿𝐸))
901, 2, 18, 13, 66, 16, 61, 3, 68, 62, 6, 89, 75hphl 27887 . . . . . . . 8 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑥((hpG‘𝐺)‘(𝑑𝐿𝐸))𝑋)
9187fveq2d 6882 . . . . . . . . . 10 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ((hpG‘𝐺)‘(𝐷𝐿𝐸)) = ((hpG‘𝐺)‘(𝑑𝐿𝐸)))
9291ad3antrrr 728 . . . . . . . . 9 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ((hpG‘𝐺)‘(𝐷𝐿𝐸)) = ((hpG‘𝐺)‘(𝑑𝐿𝐸)))
93 acopyeu.3 . . . . . . . . . 10 (𝜑𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)
9493ad5antr 732 . . . . . . . . 9 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)
9592, 94breqdi 5156 . . . . . . . 8 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑋((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹)
961, 2, 18, 13, 66, 62, 61, 6, 90, 32, 95hpgtr 27884 . . . . . . 7 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑥((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹)
97 acopyeu.2 . . . . . . . . . . . . . . . 16 (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑌”⟩)
981, 2, 17, 11, 19, 22, 25, 36, 14, 8, 97, 18, 71cgrancol 27945 . . . . . . . . . . . . . . 15 (𝜑 → ¬ (𝑌 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
991, 18, 2, 11, 36, 14, 8, 98ncolcom 27677 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑌 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
10099ad5antr 732 . . . . . . . . . . . . 13 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ¬ (𝑌 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
101 simprrr 780 . . . . . . . . . . . . . 14 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑦(𝐾𝐸)𝑌)
1021, 2, 3, 7, 10, 16, 13, 18, 101hlln 27723 . . . . . . . . . . . . 13 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑦 ∈ (𝑌𝐿𝐸))
1031, 2, 3, 7, 10, 16, 13, 101hlne1 27721 . . . . . . . . . . . . 13 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑦𝐸)
1041, 2, 18, 13, 10, 16, 69, 7, 100, 102, 103ncolncol 27762 . . . . . . . . . . . 12 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ¬ (𝑦 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
1051, 18, 2, 13, 16, 69, 7, 104ncolcom 27677 . . . . . . . . . . 11 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → ¬ (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
106 pm2.45 880 . . . . . . . . . . 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 27887 . . . . . . . 8 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑦((hpG‘𝐺)‘(𝑑𝐿𝐸))𝑌)
110 acopyeu.4 . . . . . . . . . 10 (𝜑𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)
111110ad5antr 732 . . . . . . . . 9 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)
11292, 111breqdi 5156 . . . . . . . 8 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑌((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹)
1131, 2, 18, 13, 66, 7, 61, 10, 109, 32, 112hpgtr 27884 . . . . . . 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 27921 . . . . . 6 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑥 = 𝑦)
115114, 75eqbrtrrd 5165 . . . . 5 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑦(𝐾𝐸)𝑋)
1161, 2, 3, 7, 6, 16, 13, 115hlcomd 27720 . . . 4 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑋(𝐾𝐸)𝑦)
1171, 2, 3, 6, 7, 10, 13, 16, 116, 101hltr 27726 . . 3 ((((((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) ∧ 𝑥𝑃) ∧ 𝑦𝑃) ∧ ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))) → 𝑋(𝐾𝐸)𝑌)
11870ad2antrr 724 . . . . . 6 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑋”⟩)
1191, 2, 3, 12, 20, 23, 26, 37, 15, 5, 118, 28, 40cgrahl1 27932 . . . . 5 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝑋”⟩)
1201, 2, 18, 11, 19, 22, 25, 33ncolne1 27741 . . . . . . 7 (𝜑𝐴𝐵)
121120ad2antrr 724 . . . . . 6 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝐴𝐵)
1221, 2, 3, 12, 20, 23, 26, 28, 15, 5, 17, 121, 47iscgra1 27926 . . . . 5 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝑋”⟩ ↔ ∃𝑥𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋)))
123119, 122mpbid 231 . . . 4 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ∃𝑥𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋))
12497ad2antrr 724 . . . . . 6 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑌”⟩)
1251, 2, 3, 12, 20, 23, 26, 37, 15, 9, 124, 28, 40cgrahl1 27932 . . . . 5 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝑌”⟩)
1261, 2, 3, 12, 20, 23, 26, 28, 15, 9, 17, 121, 47iscgra1 27926 . . . . 5 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → (⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝑑𝐸𝑌”⟩ ↔ ∃𝑦𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌)))
127125, 126mpbid 231 . . . 4 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ∃𝑦𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌))
128 reeanv 3225 . . . 4 (∃𝑥𝑃𝑦𝑃 ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌)) ↔ (∃𝑥𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ ∃𝑦𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌)))
129123, 127, 128sylanbrc 583 . . 3 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → ∃𝑥𝑃𝑦𝑃 ((⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑥”⟩ ∧ 𝑥(𝐾𝐸)𝑋) ∧ (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝑑𝐸𝑦”⟩ ∧ 𝑦(𝐾𝐸)𝑌)))
130117, 129r19.29vva 3212 . 2 (((𝜑𝑑𝑃) ∧ (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴))) → 𝑋(𝐾𝐸)𝑌)
131120necomd 2995 . . 3 (𝜑𝐵𝐴)
1321, 2, 3, 14, 22, 19, 11, 36, 17, 82, 131hlcgrex 27732 . 2 (𝜑 → ∃𝑑𝑃 (𝑑(𝐾𝐸)𝐷 ∧ (𝐸 𝑑) = (𝐵 𝐴)))
133130, 132r19.29a 3161 1 (𝜑𝑋(𝐾𝐸)𝑌)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2939  wrex 3069  cdif 3941   class class class wbr 5141  {copab 5203  ran crn 5670  cfv 6532  (class class class)co 7393  ⟨“cs3 14775  Basecbs 17126  distcds 17188  TarskiGcstrkg 27543  Itvcitv 27549  LineGclng 27550  cgrGccgrg 27626  hlGchlg 27716  hpGchpg 27873  cgrAccgra 27923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  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 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-tp 4627  df-op 4629  df-uni 4902  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 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-1st 7957  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-oadd 8452  df-er 8686  df-map 8805  df-pm 8806  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-dju 9878  df-card 9916  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-nn 12195  df-2 12257  df-3 12258  df-n0 12455  df-xnn0 12527  df-z 12541  df-uz 12805  df-fz 13467  df-fzo 13610  df-hash 14273  df-word 14447  df-concat 14503  df-s1 14528  df-s2 14781  df-s3 14782  df-trkgc 27564  df-trkgb 27565  df-trkgcb 27566  df-trkgld 27568  df-trkg 27569  df-cgrg 27627  df-leg 27699  df-hlg 27717  df-mir 27769  df-rag 27810  df-perpg 27812  df-hpg 27874  df-mid 27890  df-lmi 27891  df-cgra 27924
This theorem is referenced by:  tgasa1  27974
  Copyright terms: Public domain W3C validator