Metamath Proof Explorer

Theorem tgbtwnconn1

Description: Connectivity law for betweenness. Theorem 5.1 of Schwabhauser p. 39-41. In earlier presentations of Tarski's axioms, this theorem appeared as an additional axiom. It was derived from the other axioms by Gupta, 1965. (Contributed by Thierry Arnoux, 30-Apr-2019)

Ref Expression
Hypotheses tgbtwnconn1.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgbtwnconn1.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgbtwnconn1.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgbtwnconn1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgbtwnconn1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgbtwnconn1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgbtwnconn1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgbtwnconn1.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
tgbtwnconn1.2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
tgbtwnconn1.3 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
Assertion tgbtwnconn1 ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 tgbtwnconn1.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgbtwnconn1.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tgbtwnconn1.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
4 tgbtwnconn1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5 tgbtwnconn1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6 tgbtwnconn1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7 tgbtwnconn1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
8 tgbtwnconn1.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
9 tgbtwnconn1.2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
10 tgbtwnconn1.3 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
11 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) )
12 11 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) )
13 12 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 = 𝑒 ) → 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) )
14 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 = 𝑒 ) → 𝐶 = 𝑒 )
15 14 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 = 𝑒 ) → ( 𝐴 𝐼 𝐶 ) = ( 𝐴 𝐼 𝑒 ) )
16 13 15 eleqtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 = 𝑒 ) → 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) )
17 16 olcd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 = 𝑒 ) → ( 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) ) )
18 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) )
19 18 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐷 = 𝑓 ) → 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) )
20 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐷 = 𝑓 ) → 𝐷 = 𝑓 )
21 20 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐷 = 𝑓 ) → ( 𝐴 𝐼 𝐷 ) = ( 𝐴 𝐼 𝑓 ) )
22 19 21 eleqtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐷 = 𝑓 ) → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
23 22 orcd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐷 = 𝑓 ) → ( 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) ) )
24 df-ne ⊢ ( 𝐶 ≠ 𝑒 ↔ ¬ 𝐶 = 𝑒 )
25 3 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝐺 ∈ TarskiG )
26 25 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐺 ∈ TarskiG )
27 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝐴 ∈ 𝑃 )
28 27 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐴 ∈ 𝑃 )
29 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝐵 ∈ 𝑃 )
30 29 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐵 ∈ 𝑃 )
31 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝐶 ∈ 𝑃 )
32 31 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐶 ∈ 𝑃 )
33 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝐷 ∈ 𝑃 )
34 33 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐷 ∈ 𝑃 )
35 simp-11l ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝜑 )
36 35 8 syl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐴 ≠ 𝐵 )
37 35 9 syl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
38 35 10 syl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
39 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
40 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝑒 ∈ 𝑃 )
41 40 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝑒 ∈ 𝑃 )
42 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝑓 ∈ 𝑃 )
43 42 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝑓 ∈ 𝑃 )
44 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → ℎ ∈ 𝑃 )
45 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝑗 ∈ 𝑃 )
46 12 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) )
47 18 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) )
48 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) )
49 48 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝑒 ∈ ( 𝐴 𝐼 ℎ ) )
50 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) )
51 50 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) )
52 11 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) )
53 52 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) )
54 1 39 2 26 34 41 34 32 53 tgcgrcomlr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → ( 𝑒 ( dist ‘ 𝐺 ) 𝐷 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) )
55 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) )
56 55 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) )
57 48 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) )
58 50 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) )
59 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝑥 ∈ 𝑃 )
60 simprl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) )
61 simprr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) )
62 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐶 ≠ 𝑒 )
63 1 2 26 28 30 32 34 36 37 38 39 41 43 44 45 46 47 49 51 54 56 57 58 59 60 61 62 tgbtwnconn1lem3 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) ) → 𝐷 = 𝑓 )
64 1 39 2 25 27 31 42 18 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝐶 ∈ ( 𝑓 𝐼 𝐴 ) )
65 1 39 2 25 27 33 40 12 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝐷 ∈ ( 𝑒 𝐼 𝐴 ) )
66 1 39 2 25 42 40 27 31 33 64 65 axtgpasch ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) )
67 66 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐶 𝐼 𝑒 ) ∧ 𝑥 ∈ ( 𝐷 𝐼 𝑓 ) ) )
68 63 67 r19.29a ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑗 ∈ 𝑃 ) ∧ ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → 𝐷 = 𝑓 )
69 1 39 2 25 27 42 29 33 axtgsegcon ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ∃ 𝑗 ∈ 𝑃 ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) )
70 69 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) → ∃ 𝑗 ∈ 𝑃 ( 𝑓 ∈ ( 𝐴 𝐼 𝑗 ) ∧ ( 𝑓 ( dist ‘ 𝐺 ) 𝑗 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐷 ) ) )
71 68 70 r19.29a ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) ∧ ℎ ∈ 𝑃 ) ∧ ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) → 𝐷 = 𝑓 )
72 1 39 2 25 27 40 29 31 axtgsegcon ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ∃ ℎ ∈ 𝑃 ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) )
73 72 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) → ∃ ℎ ∈ 𝑃 ( 𝑒 ∈ ( 𝐴 𝐼 ℎ ) ∧ ( 𝑒 ( dist ‘ 𝐺 ) ℎ ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) )
74 71 73 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) ∧ 𝐶 ≠ 𝑒 ) → 𝐷 = 𝑓 )
75 74 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ( 𝐶 ≠ 𝑒 → 𝐷 = 𝑓 ) )
76 24 75 biimtrrid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ( ¬ 𝐶 = 𝑒 → 𝐷 = 𝑓 ) )
77 76 orrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ( 𝐶 = 𝑒 ∨ 𝐷 = 𝑓 ) )
78 17 23 77 mpjaodan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) ) → ( 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) ) )
79 1 39 2 3 4 6 6 7 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑃 ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) )
80 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) → ∃ 𝑓 ∈ 𝑃 ( 𝐶 ∈ ( 𝐴 𝐼 𝑓 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐷 ) ) )
81 78 80 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ 𝑃 ) ∧ ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) ) → ( 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) ) )
82 1 39 2 3 4 7 7 6 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑒 ∈ 𝑃 ( 𝐷 ∈ ( 𝐴 𝐼 𝑒 ) ∧ ( 𝐷 ( dist ‘ 𝐺 ) 𝑒 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐶 ) ) )
83 81 82 r19.29a ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐴 𝐼 𝐶 ) ) )