Metamath Proof Explorer

Theorem tgbtwnconn1lem3

Description: Lemma for tgbtwnconn1 . (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 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
tgbtwnconn1.m ⊢ − = ( dist ‘ 𝐺 )
tgbtwnconn1.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
tgbtwnconn1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
tgbtwnconn1.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
tgbtwnconn1.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
tgbtwnconn1.4 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐼 𝐸 ) )
tgbtwnconn1.5 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐹 ) )
tgbtwnconn1.6 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐴 𝐼 𝐻 ) )
tgbtwnconn1.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 𝐼 𝐽 ) )
tgbtwnconn1.8 ⊢ ( 𝜑 → ( 𝐸 − 𝐷 ) = ( 𝐶 − 𝐷 ) )
tgbtwnconn1.9 ⊢ ( 𝜑 → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝐷 ) )
tgbtwnconn1.10 ⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) )
tgbtwnconn1.11 ⊢ ( 𝜑 → ( 𝐹 − 𝐽 ) = ( 𝐵 − 𝐷 ) )
tgbtwnconn1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tgbtwnconn1.12 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 𝐼 𝐸 ) )
tgbtwnconn1.13 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 𝐼 𝐹 ) )
tgbtwnconn1.14 ⊢ ( 𝜑 → 𝐶 ≠ 𝐸 )
Assertion tgbtwnconn1lem3 ( 𝜑 → 𝐷 = 𝐹 )

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 tgbtwnconn1.m ⊢ − = ( dist ‘ 𝐺 )
12 tgbtwnconn1.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
13 tgbtwnconn1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
14 tgbtwnconn1.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
15 tgbtwnconn1.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
16 tgbtwnconn1.4 ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐴 𝐼 𝐸 ) )
17 tgbtwnconn1.5 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐹 ) )
18 tgbtwnconn1.6 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐴 𝐼 𝐻 ) )
19 tgbtwnconn1.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 𝐼 𝐽 ) )
20 tgbtwnconn1.8 ⊢ ( 𝜑 → ( 𝐸 − 𝐷 ) = ( 𝐶 − 𝐷 ) )
21 tgbtwnconn1.9 ⊢ ( 𝜑 → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝐷 ) )
22 tgbtwnconn1.10 ⊢ ( 𝜑 → ( 𝐸 − 𝐻 ) = ( 𝐵 − 𝐶 ) )
23 tgbtwnconn1.11 ⊢ ( 𝜑 → ( 𝐹 − 𝐽 ) = ( 𝐵 − 𝐷 ) )
24 tgbtwnconn1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
25 tgbtwnconn1.12 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐶 𝐼 𝐸 ) )
26 tgbtwnconn1.13 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 𝐼 𝐹 ) )
27 tgbtwnconn1.14 ⊢ ( 𝜑 → 𝐶 ≠ 𝐸 )
28 3 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐺 ∈ TarskiG )
29 13 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐹 ∈ 𝑃 )
30 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐷 ∈ 𝑃 )
31 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝑞 ∈ 𝑃 )
32 28 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝐺 ∈ TarskiG )
33 30 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝐷 ∈ 𝑃 )
34 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝑞 ∈ 𝑃 )
35 1 11 2 32 33 34 tgcgrtriv ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝐷 − 𝐷 ) = ( 𝑞 − 𝑞 ) )
36 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝐹 = 𝑋 )
37 24 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝑋 ∈ 𝑃 )
38 37 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝑋 ∈ 𝑃 )
39 eqidd ⊢ ( 𝜑 → ( 𝐶 − 𝐸 ) = ( 𝐶 − 𝐸 ) )
40 eqidd ⊢ ( 𝜑 → ( 𝑋 − 𝐸 ) = ( 𝑋 − 𝐸 ) )
41 21 eqcomd ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝐹 ) )
42 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 tgbtwnconn1lem2 ⊢ ( 𝜑 → ( 𝐸 − 𝐹 ) = ( 𝐶 − 𝐷 ) )
43 20 42 eqtr4d ⊢ ( 𝜑 → ( 𝐸 − 𝐷 ) = ( 𝐸 − 𝐹 ) )
44 1 11 2 3 6 24 12 7 6 24 12 13 25 25 39 40 41 43 tgifscgr ⊢ ( 𝜑 → ( 𝑋 − 𝐷 ) = ( 𝑋 − 𝐹 ) )
45 44 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝑋 − 𝐷 ) = ( 𝑋 − 𝐹 ) )
46 45 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝑋 − 𝐷 ) = ( 𝑋 − 𝐹 ) )
47 36 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝑋 − 𝐹 ) = ( 𝑋 − 𝑋 ) )
48 46 47 eqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝑋 − 𝐷 ) = ( 𝑋 − 𝑋 ) )
49 1 11 2 32 38 33 38 48 axtgcgrid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝑋 = 𝐷 )
50 36 49 eqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝐹 = 𝐷 )
51 50 oveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝐹 − 𝐷 ) = ( 𝐷 − 𝐷 ) )
52 29 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝐹 ∈ 𝑃 )
53 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) → 𝑝 ∈ 𝑃 )
54 53 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝑝 ∈ 𝑃 )
55 54 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝑝 ∈ 𝑃 )
56 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝑟 ∈ 𝑃 )
57 56 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝑟 ∈ 𝑃 )
58 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐶 ∈ 𝑃 )
59 simpr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐹 ) → 𝐶 = 𝐹 )
60 3 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐹 ) → 𝐺 ∈ TarskiG )
61 6 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐹 ) → 𝐶 ∈ 𝑃 )
62 13 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐹 ) → 𝐹 ∈ 𝑃 )
63 12 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐹 ) → 𝐸 ∈ 𝑃 )
64 21 42 eqtr4d ⊢ ( 𝜑 → ( 𝐶 − 𝐹 ) = ( 𝐸 − 𝐹 ) )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐹 ) → ( 𝐶 − 𝐹 ) = ( 𝐸 − 𝐹 ) )
66 1 11 2 60 61 62 63 62 65 59 tgcgreq ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐹 ) → 𝐸 = 𝐹 )
67 59 66 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐹 ) → 𝐶 = 𝐸 )
68 27 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐹 ) → 𝐶 ≠ 𝐸 )
69 68 neneqd ⊢ ( ( 𝜑 ∧ 𝐶 = 𝐹 ) → ¬ 𝐶 = 𝐸 )
70 67 69 pm2.65da ⊢ ( 𝜑 → ¬ 𝐶 = 𝐹 )
71 70 neqned ⊢ ( 𝜑 → 𝐶 ≠ 𝐹 )
72 71 necomd ⊢ ( 𝜑 → 𝐹 ≠ 𝐶 )
73 72 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐹 ≠ 𝐶 )
74 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) )
75 74 simpld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) )
76 12 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐸 ∈ 𝑃 )
77 1 11 2 3 6 24 12 25 tgbtwncom ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐸 𝐼 𝐶 ) )
78 77 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝑋 ∈ ( 𝐸 𝐼 𝐶 ) )
79 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) )
80 79 simpld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) )
81 1 11 2 28 76 37 58 54 78 80 tgbtwnexch3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐶 ∈ ( 𝑋 𝐼 𝑝 ) )
82 1 11 2 28 37 58 54 81 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐶 ∈ ( 𝑝 𝐼 𝑋 ) )
83 79 simprd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) )
84 83 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝑝 ) )
85 1 11 2 28 58 29 58 54 84 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐹 − 𝐶 ) = ( 𝑝 − 𝐶 ) )
86 74 simprd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) )
87 1 11 2 28 29 54 axtgcgrrflx ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐹 − 𝑝 ) = ( 𝑝 − 𝐹 ) )
88 1 11 2 28 29 58 56 54 58 37 54 29 73 75 82 85 86 87 83 axtg5seg ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝑟 − 𝑝 ) = ( 𝑋 − 𝐹 ) )
89 88 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝑋 − 𝐹 ) = ( 𝑟 − 𝑝 ) )
90 1 11 2 28 37 29 56 54 89 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐹 − 𝑋 ) = ( 𝑝 − 𝑟 ) )
91 90 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝐹 − 𝑋 ) = ( 𝑝 − 𝑟 ) )
92 1 11 2 32 52 38 55 57 91 36 tgcgreq ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝑝 = 𝑟 )
93 simprr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) )
94 93 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) )
95 92 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝑟 − 𝑝 ) = ( 𝑟 − 𝑟 ) )
96 94 95 eqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑟 ) )
97 1 11 2 32 57 34 57 96 axtgcgrid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝑟 = 𝑞 )
98 92 97 eqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → 𝑝 = 𝑞 )
99 98 oveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝑝 − 𝑞 ) = ( 𝑞 − 𝑞 ) )
100 35 51 99 3eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝐹 − 𝐷 ) = ( 𝑝 − 𝑞 ) )
101 28 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝐺 ∈ TarskiG )
102 29 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝐹 ∈ 𝑃 )
103 37 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝑋 ∈ 𝑃 )
104 30 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝐷 ∈ 𝑃 )
105 54 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝑝 ∈ 𝑃 )
106 56 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝑟 ∈ 𝑃 )
107 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝑞 ∈ 𝑃 )
108 1 11 2 3 7 24 13 26 tgbtwncom ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 𝐼 𝐷 ) )
109 108 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝑋 ∈ ( 𝐹 𝐼 𝐷 ) )
110 simplrl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) )
111 90 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → ( 𝐹 − 𝑋 ) = ( 𝑝 − 𝑟 ) )
112 88 93 45 3eqtr4rd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝑋 − 𝐷 ) = ( 𝑟 − 𝑞 ) )
113 112 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → ( 𝑋 − 𝐷 ) = ( 𝑟 − 𝑞 ) )
114 1 11 2 101 102 103 104 105 106 107 109 110 111 113 tgcgrextend ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → ( 𝐹 − 𝐷 ) = ( 𝑝 − 𝑞 ) )
115 100 114 pm2.61dane ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐹 − 𝐷 ) = ( 𝑝 − 𝑞 ) )
116 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
117 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
118 27 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐶 ≠ 𝐸 )
119 1 116 2 28 58 54 76 80 btwncolg2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐸 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝑝 ) ∨ 𝐶 = 𝑝 ) )
120 21 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝐷 ) )
121 85 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝐹 − 𝐶 ) = ( 𝑝 − 𝐶 ) )
122 50 oveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝐹 − 𝐶 ) = ( 𝐷 − 𝐶 ) )
123 98 oveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝑝 − 𝐶 ) = ( 𝑞 − 𝐶 ) )
124 121 122 123 3eqtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 = 𝑋 ) → ( 𝐷 − 𝐶 ) = ( 𝑞 − 𝐶 ) )
125 58 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝐶 ∈ 𝑃 )
126 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → 𝐹 ≠ 𝑋 )
127 85 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → ( 𝐹 − 𝐶 ) = ( 𝑝 − 𝐶 ) )
128 86 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐶 − 𝑋 ) = ( 𝐶 − 𝑟 ) )
129 1 11 2 28 58 37 58 56 128 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝑋 − 𝐶 ) = ( 𝑟 − 𝐶 ) )
130 129 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → ( 𝑋 − 𝐶 ) = ( 𝑟 − 𝐶 ) )
131 1 11 2 101 102 103 104 105 106 107 125 125 126 109 110 111 113 127 130 axtg5seg ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐹 ≠ 𝑋 ) → ( 𝐷 − 𝐶 ) = ( 𝑞 − 𝐶 ) )
132 124 131 pm2.61dane ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐷 − 𝐶 ) = ( 𝑞 − 𝐶 ) )
133 1 11 2 28 30 58 31 58 132 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐶 − 𝐷 ) = ( 𝐶 − 𝑞 ) )
134 83 120 133 3eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝑞 ) )
135 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐵 ∈ 𝑃 )
136 15 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐽 ∈ 𝑃 )
137 28 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐺 ∈ TarskiG )
138 136 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐽 ∈ 𝑃 )
139 58 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐶 ∈ 𝑃 )
140 1 11 2 3 4 6 13 15 17 19 tgbtwnexch ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐽 ) )
141 1 11 2 3 4 5 6 15 9 140 tgbtwnexch3 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐽 ) )
142 141 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐶 ∈ ( 𝐵 𝐼 𝐽 ) )
143 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐵 = 𝐽 )
144 143 oveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → ( 𝐵 𝐼 𝐽 ) = ( 𝐽 𝐼 𝐽 ) )
145 142 144 eleqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐶 ∈ ( 𝐽 𝐼 𝐽 ) )
146 1 11 2 137 138 139 145 axtgbtwnid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐽 = 𝐶 )
147 29 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐹 ∈ 𝑃 )
148 1 11 2 3 4 6 13 15 17 19 tgbtwnexch3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 𝐼 𝐽 ) )
149 1 11 2 3 5 6 13 15 141 148 tgbtwnexch2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 𝐼 𝐽 ) )
150 149 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐹 ∈ ( 𝐵 𝐼 𝐽 ) )
151 150 144 eleqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐹 ∈ ( 𝐽 𝐼 𝐽 ) )
152 1 11 2 137 138 147 151 axtgbtwnid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐽 = 𝐹 )
153 146 152 eqtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → 𝐶 = 𝐹 )
154 70 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐵 = 𝐽 ) → ¬ 𝐶 = 𝐹 )
155 153 154 pm2.65da ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ¬ 𝐵 = 𝐽 )
156 155 neqned ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐵 ≠ 𝐽 )
157 1 11 2 3 4 5 7 12 10 16 tgbtwnexch ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐸 ) )
158 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 tgbtwnconn1lem1 ⊢ ( 𝜑 → 𝐻 = 𝐽 )
159 158 oveq2d ⊢ ( 𝜑 → ( 𝐴 𝐼 𝐻 ) = ( 𝐴 𝐼 𝐽 ) )
160 18 159 eleqtrd ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐴 𝐼 𝐽 ) )
161 1 11 2 3 4 5 12 15 157 160 tgbtwnexch3 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐵 𝐼 𝐽 ) )
162 161 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐸 ∈ ( 𝐵 𝐼 𝐽 ) )
163 1 116 2 28 135 76 136 162 btwncolg3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐽 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝐸 ) ∨ 𝐵 = 𝐸 ) )
164 71 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐶 ≠ 𝐹 )
165 1 11 2 3 13 6 5 15 148 141 tgbtwnintr ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 𝐼 𝐵 ) )
166 165 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐶 ∈ ( 𝐹 𝐼 𝐵 ) )
167 1 116 2 28 58 135 29 166 btwncolg2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐹 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝐵 ) ∨ 𝐶 = 𝐵 ) )
168 28 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → 𝐺 ∈ TarskiG )
169 58 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → 𝐶 ∈ 𝑃 )
170 56 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → 𝑟 ∈ 𝑃 )
171 37 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → 𝑋 ∈ 𝑃 )
172 86 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) )
173 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → 𝐶 = 𝑟 )
174 1 11 2 168 169 170 169 171 172 173 tgcgreq ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → 𝐶 = 𝑋 )
175 76 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → 𝐸 ∈ 𝑃 )
176 eqidd ⊢ ( 𝜑 → ( 𝐷 − 𝐹 ) = ( 𝐷 − 𝐹 ) )
177 eqidd ⊢ ( 𝜑 → ( 𝑋 − 𝐹 ) = ( 𝑋 − 𝐹 ) )
178 20 eqcomd ⊢ ( 𝜑 → ( 𝐶 − 𝐷 ) = ( 𝐸 − 𝐷 ) )
179 1 11 2 3 6 7 12 7 178 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐷 − 𝐶 ) = ( 𝐷 − 𝐸 ) )
180 1 11 2 3 6 13 12 13 64 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐹 − 𝐶 ) = ( 𝐹 − 𝐸 ) )
181 1 11 2 3 7 24 13 6 7 24 13 12 26 26 176 177 179 180 tgifscgr ⊢ ( 𝜑 → ( 𝑋 − 𝐶 ) = ( 𝑋 − 𝐸 ) )
182 181 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → ( 𝑋 − 𝐶 ) = ( 𝑋 − 𝐸 ) )
183 174 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → ( 𝑋 − 𝐶 ) = ( 𝑋 − 𝑋 ) )
184 182 183 eqtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → ( 𝑋 − 𝐸 ) = ( 𝑋 − 𝑋 ) )
185 1 11 2 168 171 175 171 184 axtgcgrid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → 𝑋 = 𝐸 )
186 174 185 eqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → 𝐶 = 𝐸 )
187 27 neneqd ⊢ ( 𝜑 → ¬ 𝐶 = 𝐸 )
188 187 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) ∧ 𝐶 = 𝑟 ) → ¬ 𝐶 = 𝐸 )
189 186 188 pm2.65da ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ¬ 𝐶 = 𝑟 )
190 189 neqned ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐶 ≠ 𝑟 )
191 1 11 2 28 29 58 56 75 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐶 ∈ ( 𝑟 𝐼 𝐹 ) )
192 1 116 2 28 58 29 56 191 btwncolg2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝑟 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝐹 ) ∨ 𝐶 = 𝐹 ) )
193 93 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝑟 − 𝑝 ) = ( 𝑟 − 𝑞 ) )
194 1 116 2 28 58 56 29 117 54 31 11 190 192 134 193 lncgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐹 − 𝑝 ) = ( 𝐹 − 𝑞 ) )
195 1 116 2 28 58 29 135 117 54 31 11 164 167 134 194 lncgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐵 − 𝑝 ) = ( 𝐵 − 𝑞 ) )
196 148 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐹 ∈ ( 𝐶 𝐼 𝐽 ) )
197 1 116 2 28 58 136 29 196 btwncolg1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐹 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝐽 ) ∨ 𝐶 = 𝐽 ) )
198 1 116 2 28 58 29 136 117 54 31 11 164 197 134 194 lncgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐽 − 𝑝 ) = ( 𝐽 − 𝑞 ) )
199 1 116 2 28 135 136 76 117 54 31 11 156 163 195 198 lncgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐸 − 𝑝 ) = ( 𝐸 − 𝑞 ) )
200 1 116 2 28 58 76 54 117 31 58 11 118 119 134 199 lnid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝑝 = 𝑞 )
201 200 oveq1d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝑝 − 𝑞 ) = ( 𝑞 − 𝑞 ) )
202 115 201 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → ( 𝐹 − 𝐷 ) = ( 𝑞 − 𝑞 ) )
203 1 11 2 28 29 30 31 202 axtgcgrid ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐹 = 𝐷 )
204 203 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) ) → 𝐷 = 𝐹 )
205 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) → 𝐺 ∈ TarskiG )
206 205 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) → 𝐺 ∈ TarskiG )
207 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) → 𝑟 ∈ 𝑃 )
208 1 11 2 206 53 207 207 53 axtgsegcon ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) → ∃ 𝑞 ∈ 𝑃 ( 𝑟 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑟 − 𝑞 ) = ( 𝑟 − 𝑝 ) ) )
209 204 208 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) ) → 𝐷 = 𝐹 )
210 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) → 𝐹 ∈ 𝑃 )
211 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) → 𝐶 ∈ 𝑃 )
212 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) → 𝑋 ∈ 𝑃 )
213 1 11 2 205 210 211 211 212 axtgsegcon ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) → ∃ 𝑟 ∈ 𝑃 ( 𝐶 ∈ ( 𝐹 𝐼 𝑟 ) ∧ ( 𝐶 − 𝑟 ) = ( 𝐶 − 𝑋 ) ) )
214 209 213 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) ) → 𝐷 = 𝐹 )
215 1 11 2 3 12 6 6 13 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑃 ( 𝐶 ∈ ( 𝐸 𝐼 𝑝 ) ∧ ( 𝐶 − 𝑝 ) = ( 𝐶 − 𝐹 ) ) )
216 214 215 r19.29a ⊢ ( 𝜑 → 𝐷 = 𝐹 )