Metamath Proof Explorer

Theorem prlnghpg

Description: If two lines A and B are parallel, then any two points X and Y of B lie on the same half-plane limited by A . Theorem 12.6 of Schwabhauser p. 122. . (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses prlnghpg.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
prlnghpg.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
prlnghpg.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
prlnghpg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
prlnghpg.1 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
prlnghpg.2 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
prlnghpg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
prlnghpg.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion prlnghpg ( 𝜑 → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 )

Proof

Step Hyp Ref Expression
1 prlnghpg.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
2 prlnghpg.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
3 prlnghpg.p ⊢ ∥ = ( parlnG ‘ 𝐺 )
4 prlnghpg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 prlnghpg.1 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
6 prlnghpg.2 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
7 prlnghpg.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 prlnghpg.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
11 1 2 3 4 brprlng ⊢ ( 𝜑 → ( 𝐴 ∥ 𝐵 ↔ ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) ) )
12 5 11 mpbid ⊢ ( 𝜑 → ( ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) ∧ ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) ) )
13 12 simpld ⊢ ( 𝜑 → ( 𝐴 ∈ ran 𝐿 ∧ 𝐵 ∈ ran 𝐿 ) )
14 13 simpld ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
15 13 simprd ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
16 9 1 10 4 15 8 tglnpt ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐺 ) )
17 eleq1w ⊢ ( 𝑎 = 𝑐 → ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ↔ 𝑐 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) )
18 eleq1w ⊢ ( 𝑏 = 𝑑 → ( 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ↔ 𝑑 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) )
19 17 18 bi2anan9 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ↔ ( 𝑐 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑑 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ) )
20 oveq12 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) = ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) )
21 20 eleq2d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ↔ 𝑠 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) )
22 21 rexbidv ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ↔ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) )
23 eleq1w ⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ↔ 𝑡 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) )
24 23 cbvrexvw ⊢ ( ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ↔ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) )
25 22 24 bitrdi ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ↔ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) )
26 19 25 anbi12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) ↔ ( ( 𝑐 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑑 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) ) )
27 26 cbvopabv ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑑 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑐 ( Itv ‘ 𝐺 ) 𝑑 ) ) }
28 9 1 10 4 15 7 tglnpt ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐺 ) )
29 4 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝐺 ∈ TarskiG )
30 14 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝐴 ∈ ran 𝐿 )
31 16 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑌 ∈ ( Base ‘ 𝐺 ) )
32 12 simprd ⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∨ ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ) )
33 6 neneqd ⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
34 32 33 orcnd ⊢ ( 𝜑 → ( ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
35 34 simprd ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
37 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 )
38 8 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
39 inelcm ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
40 37 38 39 syl2anc ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
41 40 neneqd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → ¬ ( 𝐴 ∩ 𝐵 ) = ∅ )
42 36 41 pm2.65da ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝐴 )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → ¬ 𝑌 ∈ 𝐴 )
44 9 10 1 29 30 31 27 43 hpgid ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 )
45 simpr ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑌 = 𝑋 )
46 44 45 breqtrd ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑋 ) → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 )
47 42 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) → ¬ 𝑌 ∈ 𝐴 )
48 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
49 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑡 ∈ 𝐴 )
50 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝐺 ∈ TarskiG )
51 16 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑌 ∈ ( Base ‘ 𝐺 ) )
52 28 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
53 14 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝐴 ∈ ran 𝐿 )
54 9 1 10 50 53 49 tglnpt ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑡 ∈ ( Base ‘ 𝐺 ) )
55 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑌 ≠ 𝑋 )
56 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) )
57 9 10 1 50 51 52 54 55 56 btwnlng1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑡 ∈ ( 𝑌 𝐿 𝑋 ) )
58 15 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝐵 ∈ ran 𝐿 )
59 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑌 ∈ 𝐵 )
60 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑋 ∈ 𝐵 )
61 9 10 1 50 51 52 55 55 58 59 60 tglinethru ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝐵 = ( 𝑌 𝐿 𝑋 ) )
62 57 61 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑡 ∈ 𝐵 )
63 inelcm ⊢ ( ( 𝑡 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
64 49 62 63 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
65 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
66 9 65 10 27 16 28 islnopp ⊢ ( 𝜑 → ( 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ↔ ( ( ¬ 𝑌 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) → ( 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ↔ ( ( ¬ 𝑌 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝐴 ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) ) )
68 67 simplbda ⊢ ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) → ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) )
69 64 68 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
70 69 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) ∧ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) → ¬ ( 𝐴 ∩ 𝐵 ) = ∅ )
71 48 70 pm2.65da ⊢ ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) → ¬ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 )
72 simpr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → 𝐵 ⊆ ℎ )
73 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → 𝐺 ∈ TarskiG )
74 simpllr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → ℎ ∈ ran 𝐸 )
75 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → 𝐴 ∈ ran 𝐿 )
76 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → 𝑋 ∈ 𝐵 )
77 72 76 sseldd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → 𝑋 ∈ ℎ )
78 35 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
79 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
80 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
81 inelcm ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
82 79 80 81 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
83 82 neneqd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ¬ ( 𝐴 ∩ 𝐵 ) = ∅ )
84 78 83 pm2.65da ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐴 )
85 84 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → ¬ 𝑋 ∈ 𝐴 )
86 77 85 eldifd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → 𝑋 ∈ ( ℎ ∖ 𝐴 ) )
87 simplr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → 𝐴 ⊆ ℎ )
88 9 1 2 73 74 75 86 87 plng3p ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → ℎ = ( 𝐴 𝐸 𝑋 ) )
89 72 88 sseqtrd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → 𝐵 ⊆ ( 𝐴 𝐸 𝑋 ) )
90 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → 𝑌 ∈ 𝐵 )
91 89 90 sseldd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ 𝐴 ⊆ ℎ ) ∧ 𝐵 ⊆ ℎ ) → 𝑌 ∈ ( 𝐴 𝐸 𝑋 ) )
92 91 anasss ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ran 𝐸 ) ∧ ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) ) → 𝑌 ∈ ( 𝐴 𝐸 𝑋 ) )
93 34 simpld ⊢ ( 𝜑 → ∃ ℎ ∈ ran 𝐸 ( 𝐴 ⊆ ℎ ∧ 𝐵 ⊆ ℎ ) )
94 92 93 r19.29a ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 𝐸 𝑋 ) )
95 28 84 eldifd ⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) )
96 9 10 1 2 4 14 95 27 16 elplng ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐴 𝐸 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∨ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) ) )
97 94 96 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐴 ∨ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) → ( 𝑌 ∈ 𝐴 ∨ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 ∨ 𝑌 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ∧ 𝑏 ∈ ( ( Base ‘ 𝐺 ) ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑎 ( Itv ‘ 𝐺 ) 𝑏 ) ) } 𝑋 ) )
99 47 71 98 ecase13d ⊢ ( ( 𝜑 ∧ 𝑌 ≠ 𝑋 ) → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 )
100 46 99 pm2.61dane ⊢ ( 𝜑 → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 )
101 9 10 1 4 14 16 27 28 100 hpgcom ⊢ ( 𝜑 → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 )