Metamath Proof Explorer

Theorem hlpasch

Description: An application of the axiom of Pasch for half-lines. (Contributed by Thierry Arnoux, 15-Sep-2020)

Ref Expression
Hypotheses hlpasch.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
hlpasch.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
hlpasch.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
hlpasch.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
hlpasch.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
hlpasch.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
hlpasch.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
hlpasch.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
hlpasch.5 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
hlpasch.6 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
hlpasch.7 ⊢ ( 𝜑 → 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐷 )
hlpasch.8 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐼 𝐶 ) )
Assertion hlpasch ( 𝜑 → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 hlpasch.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 hlpasch.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 hlpasch.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 hlpasch.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 hlpasch.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 hlpasch.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 hlpasch.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 hlpasch.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
9 hlpasch.5 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 hlpasch.6 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
11 hlpasch.7 ⊢ ( 𝜑 → 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐷 )
12 hlpasch.8 ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑋 𝐼 𝐶 ) )
13 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
14 4 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐺 ∈ TarskiG )
15 9 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐷 ∈ 𝑃 )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝑋 ∈ 𝑃 )
17 7 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐶 ∈ 𝑃 )
18 6 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐵 ∈ 𝑃 )
19 5 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐴 ∈ 𝑃 )
20 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
21 simpr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
22 1 20 2 14 18 17 15 21 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) )
23 12 adantr ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → 𝐴 ∈ ( 𝑋 𝐼 𝐶 ) )
24 1 2 13 14 15 16 17 18 19 22 23 outpasch ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) )
25 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝑒 ∈ 𝑃 )
26 18 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝐵 ∈ 𝑃 )
27 19 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝐴 ∈ 𝑃 )
28 14 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝐺 ∈ TarskiG )
29 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) )
30 1 20 2 28 26 27 25 29 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝐴 ∈ ( 𝑒 𝐼 𝐵 ) )
31 28 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐺 ∈ TarskiG )
32 26 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐵 ∈ 𝑃 )
33 27 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐴 ∈ 𝑃 )
34 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) )
35 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝑒 = 𝐵 )
36 35 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → ( 𝐵 𝐼 𝑒 ) = ( 𝐵 𝐼 𝐵 ) )
37 34 36 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐴 ∈ ( 𝐵 𝐼 𝐵 ) )
38 1 20 2 31 32 33 37 axtgbtwnid ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐵 = 𝐴 )
39 38 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐴 = 𝐵 )
40 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝐴 ≠ 𝐵 )
41 40 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐴 ≠ 𝐵 )
42 41 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) ∧ 𝑒 = 𝐵 ) → ¬ 𝐴 = 𝐵 )
43 39 42 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → ¬ 𝑒 = 𝐵 )
44 43 neqned ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝑒 ≠ 𝐵 )
45 1 2 3 25 26 27 28 27 30 44 40 btwnhl2 ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 )
46 15 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝐷 ∈ 𝑃 )
47 16 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝑋 ∈ 𝑃 )
48 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) )
49 1 20 2 28 46 25 47 48 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) )
50 45 49 jca ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )
51 50 ex ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) → ( ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) ) )
52 51 reximdva ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → ( ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ∧ 𝐴 ∈ ( 𝐵 𝐼 𝑒 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) ) )
53 24 52 mpd ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )
54 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → 𝐷 ∈ 𝑃 )
55 54 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐷 ∈ 𝑃 )
56 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) ∧ 𝑒 = 𝐷 ) → 𝑒 = 𝐷 )
57 56 breq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) ∧ 𝑒 = 𝐷 ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ↔ 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 ) )
58 56 eleq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) ∧ 𝑒 = 𝐷 ) → ( 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ↔ 𝐷 ∈ ( 𝑋 𝐼 𝐷 ) ) )
59 57 58 anbi12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) ∧ 𝑒 = 𝐷 ) → ( ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) ↔ ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 ∧ 𝐷 ∈ ( 𝑋 𝐼 𝐷 ) ) ) )
60 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → 𝐴 ∈ 𝑃 )
61 60 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐴 ∈ 𝑃 )
62 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → 𝐵 ∈ 𝑃 )
63 62 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐵 ∈ 𝑃 )
64 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → 𝐺 ∈ TarskiG )
65 64 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐺 ∈ TarskiG )
66 1 2 3 7 9 6 4 11 hlcomd ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐵 ) 𝐶 )
67 66 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐷 ( 𝐾 ‘ 𝐵 ) 𝐶 )
68 7 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
69 68 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐶 ∈ 𝑃 )
70 12 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐴 ∈ ( 𝑋 𝐼 𝐶 ) )
71 70 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐴 ∈ ( 𝑋 𝐼 𝐶 ) )
72 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝑋 = 𝐵 )
73 72 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → ( 𝑋 𝐼 𝐶 ) = ( 𝐵 𝐼 𝐶 ) )
74 71 73 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) )
75 1 2 3 7 9 6 4 ishlg ⊢ ( 𝜑 → ( 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐷 ↔ ( 𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ) ) )
76 11 75 mpbid ⊢ ( 𝜑 → ( 𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ ( 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ) )
77 76 simp1d ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
78 77 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐶 ≠ 𝐵 )
79 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → 𝐴 ≠ 𝐵 )
80 79 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐴 ≠ 𝐵 )
81 1 2 3 55 69 63 65 61 74 78 80 hlbtwn ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → ( 𝐷 ( 𝐾 ‘ 𝐵 ) 𝐶 ↔ 𝐷 ( 𝐾 ‘ 𝐵 ) 𝐴 ) )
82 67 81 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐷 ( 𝐾 ‘ 𝐵 ) 𝐴 )
83 1 2 3 55 61 63 65 82 hlcomd ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 )
84 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → 𝑋 ∈ 𝑃 )
85 84 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝑋 ∈ 𝑃 )
86 1 20 2 65 85 55 tgbtwntriv2 ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → 𝐷 ∈ ( 𝑋 𝐼 𝐷 ) )
87 83 86 jca ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 ∧ 𝐷 ∈ ( 𝑋 𝐼 𝐷 ) ) )
88 55 59 87 rspcedvd ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 = 𝐵 ) → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )
89 84 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝑋 ∈ 𝑃 )
90 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 = 𝑋 ) → 𝑒 = 𝑋 )
91 90 breq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 = 𝑋 ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ↔ 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ) )
92 90 eleq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 = 𝑋 ) → ( 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ↔ 𝑋 ∈ ( 𝑋 𝐼 𝐷 ) ) )
93 91 92 anbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 = 𝑋 ) → ( ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) ↔ ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ∧ 𝑋 ∈ ( 𝑋 𝐼 𝐷 ) ) ) )
94 93 ad4ant14 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑒 = 𝑋 ) → ( ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) ↔ ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ∧ 𝑋 ∈ ( 𝑋 𝐼 𝐷 ) ) ) )
95 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 )
96 1 20 2 64 84 54 tgbtwntriv1 ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → 𝑋 ∈ ( 𝑋 𝐼 𝐷 ) )
97 96 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝑋 ∈ ( 𝑋 𝐼 𝐷 ) )
98 95 97 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ∧ 𝑋 ∈ ( 𝑋 𝐼 𝐷 ) ) )
99 89 94 98 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )
100 54 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐷 ∈ 𝑃 )
101 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) ∧ 𝑒 = 𝐷 ) → 𝑒 = 𝐷 )
102 101 breq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) ∧ 𝑒 = 𝐷 ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ↔ 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 ) )
103 101 eleq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) ∧ 𝑒 = 𝐷 ) → ( 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ↔ 𝐷 ∈ ( 𝑋 𝐼 𝐷 ) ) )
104 102 103 anbi12d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) ∧ 𝑒 = 𝐷 ) → ( ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) ↔ ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 ∧ 𝐷 ∈ ( 𝑋 𝐼 𝐷 ) ) ) )
105 79 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐴 ≠ 𝐵 )
106 1 2 3 7 9 6 4 11 hlne2 ⊢ ( 𝜑 → 𝐷 ≠ 𝐵 )
107 106 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐷 ≠ 𝐵 )
108 64 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐺 ∈ TarskiG )
109 62 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐵 ∈ 𝑃 )
110 60 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐴 ∈ 𝑃 )
111 68 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐶 ∈ 𝑃 )
112 111 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐶 ∈ 𝑃 )
113 84 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝑋 ∈ 𝑃 )
114 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) )
115 70 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐴 ∈ ( 𝑋 𝐼 𝐶 ) )
116 115 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐴 ∈ ( 𝑋 𝐼 𝐶 ) )
117 1 20 2 108 113 109 110 112 114 116 tgbtwnexch3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝐶 ) )
118 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) )
119 1 2 108 109 110 100 112 117 118 tgbtwnconn3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → ( 𝐴 ∈ ( 𝐵 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐵 𝐼 𝐴 ) ) )
120 1 2 3 5 9 6 4 ishlg ⊢ ( 𝜑 → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 ↔ ( 𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐵 𝐼 𝐴 ) ) ) ) )
121 120 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 ↔ ( 𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐵 𝐼 𝐴 ) ) ) ) )
122 105 107 119 121 mpbir3and ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 )
123 1 20 2 108 113 100 tgbtwntriv2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → 𝐷 ∈ ( 𝑋 𝐼 𝐷 ) )
124 122 123 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 ∧ 𝐷 ∈ ( 𝑋 𝐼 𝐷 ) ) )
125 100 104 124 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )
126 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝑋 ∈ 𝑃 )
127 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐵 ∈ 𝑃 )
128 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐴 ∈ 𝑃 )
129 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
130 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝑋 ≠ 𝐵 )
131 130 neneqd ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ¬ 𝑋 = 𝐵 )
132 64 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
133 132 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 = 𝐶 ) → 𝐺 ∈ TarskiG )
134 126 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 = 𝐶 ) → 𝑋 ∈ 𝑃 )
135 128 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 = 𝐶 ) → 𝐴 ∈ 𝑃 )
136 115 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 = 𝐶 ) → 𝐴 ∈ ( 𝑋 𝐼 𝐶 ) )
137 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 = 𝐶 ) → 𝑋 = 𝐶 )
138 137 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 = 𝐶 ) → ( 𝑋 𝐼 𝑋 ) = ( 𝑋 𝐼 𝐶 ) )
139 136 138 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 = 𝐶 ) → 𝐴 ∈ ( 𝑋 𝐼 𝑋 ) )
140 1 20 2 133 134 135 139 axtgbtwnid ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 = 𝐶 ) → 𝑋 = 𝐴 )
141 140 olcd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 = 𝐶 ) → ( 𝐵 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝐴 ) ∨ 𝑋 = 𝐴 ) )
142 132 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
143 127 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → 𝐵 ∈ 𝑃 )
144 111 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
145 126 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → 𝑋 ∈ 𝑃 )
146 128 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → 𝐴 ∈ 𝑃 )
147 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → 𝑋 ≠ 𝐶 )
148 147 necomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → 𝐶 ≠ 𝑋 )
149 148 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → ¬ 𝐶 = 𝑋 )
150 54 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐷 ∈ 𝑃 )
151 106 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐷 ≠ 𝐵 )
152 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) )
153 1 2 13 132 150 127 126 151 152 lncom ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝑋 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝐵 ) )
154 77 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
155 154 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐵 ≠ 𝐶 )
156 66 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐷 ( 𝐾 ‘ 𝐵 ) 𝐶 )
157 1 2 3 150 111 127 132 13 156 hlln ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐷 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝐵 ) )
158 1 2 13 132 127 111 150 155 157 lncom ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐷 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐶 ) )
159 158 orcd ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( 𝐷 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐶 ) ∨ 𝐵 = 𝐶 ) )
160 1 2 13 132 126 150 127 111 153 159 coltr ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐶 ) ∨ 𝐵 = 𝐶 ) )
161 1 13 2 132 127 111 126 160 colrot1 ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( 𝐵 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝑋 ) ∨ 𝐶 = 𝑋 ) )
162 161 orcomd ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( 𝐶 = 𝑋 ∨ 𝐵 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝑋 ) ) )
163 162 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → ( 𝐶 = 𝑋 ∨ 𝐵 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝑋 ) ) )
164 163 ord ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → ( ¬ 𝐶 = 𝑋 → 𝐵 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝑋 ) ) )
165 149 164 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → 𝐵 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝑋 ) )
166 1 13 2 132 126 128 111 115 btwncolg3 ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( 𝐶 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝐴 ) ∨ 𝑋 = 𝐴 ) )
167 166 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → ( 𝐶 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝐴 ) ∨ 𝑋 = 𝐴 ) )
168 1 2 13 142 143 144 145 146 165 167 coltr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) ∧ 𝑋 ≠ 𝐶 ) → ( 𝐵 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝐴 ) ∨ 𝑋 = 𝐴 ) )
169 141 168 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( 𝐵 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝐴 ) ∨ 𝑋 = 𝐴 ) )
170 1 13 2 132 126 128 127 169 colrot2 ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( 𝐴 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝑋 ) ∨ 𝐵 = 𝑋 ) )
171 1 13 2 132 127 126 128 170 colcom ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( 𝐴 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝐵 ) ∨ 𝑋 = 𝐵 ) )
172 171 orcomd ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( 𝑋 = 𝐵 ∨ 𝐴 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝐵 ) ) )
173 172 ord ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( ¬ 𝑋 = 𝐵 → 𝐴 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝐵 ) ) )
174 131 173 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → 𝐴 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝐵 ) )
175 1 2 3 126 127 128 129 128 13 174 lnhl ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑋 ∨ 𝐵 ∈ ( 𝑋 𝐼 𝐴 ) ) )
176 99 125 175 mpjaodan ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑋 ≠ 𝐵 ) → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )
177 88 176 pm2.61dane ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )
178 4 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
179 8 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝑋 ∈ 𝑃 )
180 6 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐵 ∈ 𝑃 )
181 5 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐴 ∈ 𝑃 )
182 9 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐷 ∈ 𝑃 )
183 simpr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) )
184 1 20 2 178 179 180 68 181 182 70 183 axtgpasch ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) )
185 184 adantr ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) )
186 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝑒 ∈ 𝑃 )
187 181 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝐴 ∈ 𝑃 )
188 180 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝐵 ∈ 𝑃 )
189 178 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝐺 ∈ TarskiG )
190 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) )
191 1 20 2 189 187 186 188 190 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝑒 ∈ ( 𝐵 𝐼 𝐴 ) )
192 10 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
193 192 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝐵 ≠ 𝐴 )
194 189 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐺 ∈ TarskiG )
195 9 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐷 ∈ 𝑃 )
196 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝑋 ∈ 𝑃 )
197 188 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐵 ∈ 𝑃 )
198 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) )
199 106 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐷 )
200 199 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐵 ≠ 𝐷 )
201 200 neneqd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → ¬ 𝐵 = 𝐷 )
202 ioran ⊢ ( ¬ ( 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ∨ 𝐵 = 𝐷 ) ↔ ( ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ∧ ¬ 𝐵 = 𝐷 ) )
203 198 201 202 sylanbrc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → ¬ ( 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ∨ 𝐵 = 𝐷 ) )
204 1 13 2 194 197 195 196 203 ncolrot2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → ¬ ( 𝐷 ∈ ( 𝑋 ( LineG ‘ 𝐺 ) 𝐵 ) ∨ 𝑋 = 𝐵 ) )
205 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝑒 = 𝐵 )
206 186 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝑒 ∈ 𝑃 )
207 1 2 13 194 195 196 197 204 ncolne1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐷 ≠ 𝑋 )
208 simplrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) )
209 1 2 13 194 195 196 206 207 208 btwnlng1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝑒 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝑋 ) )
210 205 209 eqeltrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐵 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝑋 ) )
211 1 2 13 194 195 196 207 tglinerflx1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐷 ∈ ( 𝐷 ( LineG ‘ 𝐺 ) 𝑋 ) )
212 106 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐷 ≠ 𝐵 )
213 212 necomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐵 ≠ 𝐷 )
214 1 2 13 194 197 195 213 tglinerflx1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐵 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) )
215 1 2 13 194 197 195 213 tglinerflx2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐷 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) )
216 1 2 13 194 195 196 197 195 204 210 211 214 215 tglineinteq ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) ∧ 𝑒 = 𝐵 ) → 𝐵 = 𝐷 )
217 216 201 pm2.65da ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → ¬ 𝑒 = 𝐵 )
218 217 neqned ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝑒 ≠ 𝐵 )
219 1 2 3 188 187 186 189 187 191 193 218 btwnhl1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝑒 ( 𝐾 ‘ 𝐵 ) 𝐴 )
220 1 2 3 186 187 188 189 219 hlcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 )
221 178 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) → 𝐺 ∈ TarskiG )
222 182 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) → 𝐷 ∈ 𝑃 )
223 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) → 𝑒 ∈ 𝑃 )
224 179 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) → 𝑋 ∈ 𝑃 )
225 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) → 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) )
226 1 20 2 221 222 223 224 225 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) → 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) )
227 226 adantrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) )
228 220 227 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )
229 228 ex ⊢ ( ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) ∧ 𝑒 ∈ 𝑃 ) → ( ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) → ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) ) )
230 229 reximdva ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → ( ∃ 𝑒 ∈ 𝑃 ( 𝑒 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑒 ∈ ( 𝐷 𝐼 𝑋 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) ) )
231 185 230 mpd ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) ∧ ¬ 𝑋 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐷 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )
232 177 231 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )
233 76 simp3d ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐵 𝐼 𝐶 ) ) )
234 53 232 233 mpjaodan ⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝑃 ( 𝐴 ( 𝐾 ‘ 𝐵 ) 𝑒 ∧ 𝑒 ∈ ( 𝑋 𝐼 𝐷 ) ) )