Metamath Proof Explorer

Theorem krippenlem

Description: Lemma for krippen . We can assume krippen.7 "without loss of generality". (Contributed by Thierry Arnoux, 12-Aug-2019)

Ref Expression
Hypotheses mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirval.d ⊢ − = ( dist ‘ 𝐺 )
mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
krippen.m ⊢ 𝑀 = ( 𝑆 ‘ 𝑋 )
krippen.n ⊢ 𝑁 = ( 𝑆 ‘ 𝑌 )
krippen.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
krippen.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
krippen.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
krippen.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
krippen.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
krippen.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
krippen.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
krippen.1 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
krippen.2 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐹 ) )
krippen.3 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝐵 ) )
krippen.4 ⊢ ( 𝜑 → ( 𝐶 − 𝐸 ) = ( 𝐶 − 𝐹 ) )
krippen.5 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 ‘ 𝐴 ) )
krippen.6 ⊢ ( 𝜑 → 𝐹 = ( 𝑁 ‘ 𝐸 ) )
krippen.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
krippen.7 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ≤ ( 𝐶 − 𝐸 ) )
Assertion krippenlem ( 𝜑 → 𝐶 ∈ ( 𝑋 𝐼 𝑌 ) )

Proof

Step Hyp Ref Expression
1 mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 mirval.d ⊢ − = ( dist ‘ 𝐺 )
3 mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
6 mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 krippen.m ⊢ 𝑀 = ( 𝑆 ‘ 𝑋 )
8 krippen.n ⊢ 𝑁 = ( 𝑆 ‘ 𝑌 )
9 krippen.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10 krippen.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
11 krippen.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
12 krippen.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
13 krippen.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
14 krippen.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
15 krippen.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
16 krippen.1 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
17 krippen.2 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐹 ) )
18 krippen.3 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝐵 ) )
19 krippen.4 ⊢ ( 𝜑 → ( 𝐶 − 𝐸 ) = ( 𝐶 − 𝐹 ) )
20 krippen.5 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 ‘ 𝐴 ) )
21 krippen.6 ⊢ ( 𝜑 → 𝐹 = ( 𝑁 ‘ 𝐸 ) )
22 krippen.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
23 krippen.7 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ≤ ( 𝐶 − 𝐸 ) )
24 16 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
25 6 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐺 ∈ TarskiG )
26 11 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐶 ∈ 𝑃 )
27 9 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐴 ∈ 𝑃 )
28 10 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐵 ∈ 𝑃 )
29 18 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝐵 ) )
30 23 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( 𝐶 − 𝐴 ) ≤ ( 𝐶 − 𝐸 ) )
31 simpr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐸 = 𝐶 )
32 31 oveq2d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( 𝐶 − 𝐸 ) = ( 𝐶 − 𝐶 ) )
33 30 32 breqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( 𝐶 − 𝐴 ) ≤ ( 𝐶 − 𝐶 ) )
34 1 2 3 22 25 26 27 26 28 33 legeq ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐶 = 𝐴 )
35 1 2 3 25 26 27 26 28 29 34 tgcgreq ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐶 = 𝐵 )
36 20 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐵 = ( 𝑀 ‘ 𝐴 ) )
37 35 34 36 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( 𝑀 ‘ 𝐴 ) = 𝐴 )
38 14 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝑋 ∈ 𝑃 )
39 1 2 3 4 5 25 38 7 27 mirinv ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( ( 𝑀 ‘ 𝐴 ) = 𝐴 ↔ 𝑋 = 𝐴 ) )
40 37 39 mpbid ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝑋 = 𝐴 )
41 13 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐹 ∈ 𝑃 )
42 19 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( 𝐶 − 𝐸 ) = ( 𝐶 − 𝐹 ) )
43 42 32 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝐶 ) )
44 1 2 3 25 26 41 26 43 axtgcgrid ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐶 = 𝐹 )
45 21 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐹 = ( 𝑁 ‘ 𝐸 ) )
46 31 44 45 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( 𝑁 ‘ 𝐸 ) = 𝐸 )
47 15 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝑌 ∈ 𝑃 )
48 12 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐸 ∈ 𝑃 )
49 1 2 3 4 5 25 47 8 48 mirinv ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( ( 𝑁 ‘ 𝐸 ) = 𝐸 ↔ 𝑌 = 𝐸 ) )
50 46 49 mpbid ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝑌 = 𝐸 )
51 40 50 oveq12d ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → ( 𝑋 𝐼 𝑌 ) = ( 𝐴 𝐼 𝐸 ) )
52 24 51 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐶 ) → 𝐶 ∈ ( 𝑋 𝐼 𝑌 ) )
53 6 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
54 53 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝐺 ∈ TarskiG )
55 11 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
56 eqid ⊢ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 )
57 1 2 3 4 5 53 55 56 mirf ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝑆 ‘ 𝐶 ) : 𝑃 ⟶ 𝑃 )
58 15 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝑌 ∈ 𝑃 )
59 57 58 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ∈ 𝑃 )
60 59 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ∈ 𝑃 )
61 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝑞 ∈ 𝑃 )
62 55 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝐶 ∈ 𝑃 )
63 58 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝑌 ∈ 𝑃 )
64 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) )
65 1 2 3 4 5 6 11 56 15 mirbtwn ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝑌 ) )
66 65 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝐶 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝑌 ) )
67 1 2 3 54 60 61 62 63 64 66 tgbtwnexch3 ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝐶 ∈ ( 𝑞 𝐼 𝑌 ) )
68 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝑋 ∈ 𝑃 )
69 9 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐴 ∈ 𝑃 )
70 69 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝐴 ∈ 𝑃 )
71 10 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐵 ∈ 𝑃 )
72 71 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝐵 ∈ 𝑃 )
73 eqid ⊢ ( 𝑆 ‘ 𝑞 ) = ( 𝑆 ‘ 𝑞 )
74 12 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐸 ∈ 𝑃 )
75 57 74 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ∈ 𝑃 )
76 13 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐹 ∈ 𝑃 )
77 57 76 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ∈ 𝑃 )
78 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 = 𝐶 ) → 𝐺 ∈ TarskiG )
79 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ 𝑃 )
80 75 adantr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 = 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ∈ 𝑃 )
81 1 2 3 78 79 80 tgbtwntriv1 ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ ( 𝐴 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
82 simpr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 )
83 82 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 = 𝐶 ) → ( 𝐴 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) = ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
84 81 83 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
85 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
86 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∈ 𝑃 )
87 75 adantr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ∈ 𝑃 )
88 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
89 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → 𝐸 ∈ 𝑃 )
90 simplr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → 𝐸 ≠ 𝐶 )
91 1 2 3 6 9 11 12 16 tgbtwncom ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐸 𝐼 𝐴 ) )
92 91 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ∈ ( 𝐸 𝐼 𝐴 ) )
93 1 2 3 4 5 85 88 56 89 mirbtwn ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) 𝐼 𝐸 ) )
94 1 2 3 85 87 88 89 93 tgbtwncom ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ∈ ( 𝐸 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
95 1 3 85 89 88 86 87 90 92 94 tgbtwnconn2 ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → ( 𝐴 ∈ ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) ∨ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ∈ ( 𝐶 𝐼 𝐴 ) ) )
96 23 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐶 − 𝐴 ) ≤ ( 𝐶 − 𝐸 ) )
97 1 2 3 4 5 53 55 56 74 mircgr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) = ( 𝐶 − 𝐸 ) )
98 96 97 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐶 − 𝐴 ) ≤ ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
99 98 adantr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → ( 𝐶 − 𝐴 ) ≤ ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
100 1 2 3 22 85 86 87 88 86 95 99 legbtwn ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) → 𝐴 ∈ ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
101 84 100 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐴 ∈ ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
102 1 2 3 53 55 69 75 101 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐴 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) 𝐼 𝐶 ) )
103 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 = 𝐶 ) → 𝐺 ∈ TarskiG )
104 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 = 𝐶 ) → 𝐵 ∈ 𝑃 )
105 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 = 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ∈ 𝑃 )
106 1 2 3 103 104 105 tgbtwntriv1 ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 = 𝐶 ) → 𝐵 ∈ ( 𝐵 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
107 simpr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 = 𝐶 ) → 𝐵 = 𝐶 )
108 107 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 = 𝐶 ) → ( 𝐵 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) = ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
109 106 108 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 = 𝐶 ) → 𝐵 ∈ ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
110 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
111 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ 𝑃 )
112 77 adantr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ∈ 𝑃 )
113 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
114 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → 𝐹 ∈ 𝑃 )
115 6 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = 𝐶 ) → 𝐺 ∈ TarskiG )
116 11 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = 𝐶 ) → 𝐶 ∈ 𝑃 )
117 12 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = 𝐶 ) → 𝐸 ∈ 𝑃 )
118 19 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = 𝐶 ) → ( 𝐶 − 𝐸 ) = ( 𝐶 − 𝐹 ) )
119 simpr ⊢ ( ( 𝜑 ∧ 𝐹 = 𝐶 ) → 𝐹 = 𝐶 )
120 119 oveq2d ⊢ ( ( 𝜑 ∧ 𝐹 = 𝐶 ) → ( 𝐶 − 𝐹 ) = ( 𝐶 − 𝐶 ) )
121 118 120 eqtrd ⊢ ( ( 𝜑 ∧ 𝐹 = 𝐶 ) → ( 𝐶 − 𝐸 ) = ( 𝐶 − 𝐶 ) )
122 1 2 3 115 116 117 116 121 axtgcgrid ⊢ ( ( 𝜑 ∧ 𝐹 = 𝐶 ) → 𝐶 = 𝐸 )
123 122 eqcomd ⊢ ( ( 𝜑 ∧ 𝐹 = 𝐶 ) → 𝐸 = 𝐶 )
124 123 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐹 = 𝐶 ) → 𝐸 = 𝐶 )
125 simplr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐹 = 𝐶 ) → 𝐸 ≠ 𝐶 )
126 125 neneqd ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐹 = 𝐶 ) → ¬ 𝐸 = 𝐶 )
127 124 126 pm2.65da ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ¬ 𝐹 = 𝐶 )
128 127 neqned ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐹 ≠ 𝐶 )
129 128 adantr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → 𝐹 ≠ 𝐶 )
130 1 2 3 6 10 11 13 17 tgbtwncom ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 𝐼 𝐵 ) )
131 130 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ ( 𝐹 𝐼 𝐵 ) )
132 1 2 3 4 5 110 113 56 114 mirbtwn ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) 𝐼 𝐹 ) )
133 1 2 3 110 112 113 114 132 tgbtwncom ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → 𝐶 ∈ ( 𝐹 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
134 1 3 110 114 113 111 112 129 131 133 tgbtwnconn2 ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → ( 𝐵 ∈ ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) ∨ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ∈ ( 𝐶 𝐼 𝐵 ) ) )
135 23 18 19 3brtr3d ⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐹 ) )
136 135 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − 𝐹 ) )
137 1 2 3 4 5 53 55 56 76 mircgr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) = ( 𝐶 − 𝐹 ) )
138 136 137 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
139 138 adantr ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → ( 𝐶 − 𝐵 ) ≤ ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
140 1 2 3 22 110 111 112 113 111 134 139 legbtwn ⊢ ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → 𝐵 ∈ ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
141 109 140 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐵 ∈ ( 𝐶 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
142 1 2 3 53 55 71 77 141 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐵 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) 𝐼 𝐶 ) )
143 19 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐶 − 𝐸 ) = ( 𝐶 − 𝐹 ) )
144 143 97 137 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) = ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
145 1 2 3 53 55 75 55 77 144 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) − 𝐶 ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) − 𝐶 ) )
146 18 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝐵 ) )
147 1 2 3 53 55 69 55 71 146 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐴 − 𝐶 ) = ( 𝐵 − 𝐶 ) )
148 eqid ⊢ ( 𝑆 ‘ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) = ( 𝑆 ‘ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) )
149 1 2 3 4 5 53 59 148 75 mircgr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − ( ( 𝑆 ‘ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) ‘ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) )
150 eqid ⊢ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 )
151 eqid ⊢ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 )
152 eqid ⊢ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 )
153 21 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐹 = ( 𝑁 ‘ 𝐸 ) )
154 8 fveq1i ⊢ ( 𝑁 ‘ 𝐸 ) = ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐸 )
155 153 154 eqtr2di ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝑌 ) ‘ 𝐸 ) = 𝐹 )
156 1 2 3 4 5 53 56 150 151 152 55 58 74 76 155 mirauto ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( 𝑆 ‘ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) ‘ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) )
157 156 oveq2d ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − ( ( 𝑆 ‘ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) ‘ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
158 149 157 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
159 1 2 3 53 59 75 59 77 158 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) )
160 eqidd ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) = ( 𝐶 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) )
161 1 2 3 53 75 69 55 59 77 71 55 59 102 142 145 147 159 160 tgifscgr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐴 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) = ( 𝐵 − ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) )
162 1 2 3 53 69 59 71 59 161 tgcgrcomlr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − 𝐴 ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − 𝐵 ) )
163 162 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − 𝐴 ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − 𝐵 ) )
164 54 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → 𝐺 ∈ TarskiG )
165 60 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ∈ 𝑃 )
166 61 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → 𝑞 ∈ 𝑃 )
167 64 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) )
168 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 )
169 168 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) )
170 167 169 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ) )
171 1 2 3 164 165 166 170 axtgbtwnid ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝑞 )
172 171 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − 𝐴 ) = ( 𝑞 − 𝐴 ) )
173 171 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − 𝐵 ) = ( 𝑞 − 𝐵 ) )
174 163 172 173 3eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝐶 ) → ( 𝑞 − 𝐴 ) = ( 𝑞 − 𝐵 ) )
175 53 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → 𝐺 ∈ TarskiG )
176 59 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ∈ 𝑃 )
177 55 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → 𝐶 ∈ 𝑃 )
178 61 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → 𝑞 ∈ 𝑃 )
179 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
180 69 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → 𝐴 ∈ 𝑃 )
181 71 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → 𝐵 ∈ 𝑃 )
182 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 )
183 60 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ∈ 𝑃 )
184 64 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) )
185 1 4 3 175 183 178 177 184 btwncolg3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → ( 𝐶 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐿 𝑞 ) ∨ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) = 𝑞 ) )
186 162 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − 𝐴 ) = ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) − 𝐵 ) )
187 146 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝐵 ) )
188 1 4 3 175 176 177 178 179 180 181 2 182 185 186 187 lncgr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) ∧ ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ≠ 𝐶 ) → ( 𝑞 − 𝐴 ) = ( 𝑞 − 𝐵 ) )
189 174 188 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → ( 𝑞 − 𝐴 ) = ( 𝑞 − 𝐵 ) )
190 189 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → ( 𝑞 − 𝐵 ) = ( 𝑞 − 𝐴 ) )
191 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) )
192 1 2 3 54 70 61 72 191 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝑞 ∈ ( 𝐵 𝐼 𝐴 ) )
193 1 2 3 4 5 54 61 73 70 72 190 192 ismir ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝐵 = ( ( 𝑆 ‘ 𝑞 ) ‘ 𝐴 ) )
194 193 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → ( ( 𝑆 ‘ 𝑞 ) ‘ 𝐴 ) = 𝐵 )
195 20 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝐵 = ( 𝑀 ‘ 𝐴 ) )
196 7 fveq1i ⊢ ( 𝑀 ‘ 𝐴 ) = ( ( 𝑆 ‘ 𝑋 ) ‘ 𝐴 )
197 195 196 eqtr2di ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → ( ( 𝑆 ‘ 𝑋 ) ‘ 𝐴 ) = 𝐵 )
198 1 2 3 4 5 54 61 68 70 72 194 197 miduniq ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝑞 = 𝑋 )
199 198 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → ( 𝑞 𝐼 𝑌 ) = ( 𝑋 𝐼 𝑌 ) )
200 67 199 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) ) → 𝐶 ∈ ( 𝑋 𝐼 𝑌 ) )
201 1 2 3 4 5 53 58 8 74 mirbtwn ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝑌 ∈ ( ( 𝑁 ‘ 𝐸 ) 𝐼 𝐸 ) )
202 153 oveq1d ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( 𝐹 𝐼 𝐸 ) = ( ( 𝑁 ‘ 𝐸 ) 𝐼 𝐸 ) )
203 201 202 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝑌 ∈ ( 𝐹 𝐼 𝐸 ) )
204 1 2 3 53 76 58 74 203 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝑌 ∈ ( 𝐸 𝐼 𝐹 ) )
205 1 2 3 4 5 53 55 56 74 58 76 204 mirbtwni ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐸 ) 𝐼 ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐹 ) ) )
206 1 2 3 53 75 69 55 77 71 59 102 142 205 tgtrisegint ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → ∃ 𝑞 ∈ 𝑃 ( 𝑞 ∈ ( ( ( 𝑆 ‘ 𝐶 ) ‘ 𝑌 ) 𝐼 𝐶 ) ∧ 𝑞 ∈ ( 𝐴 𝐼 𝐵 ) ) )
207 200 206 r19.29a ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐶 ) → 𝐶 ∈ ( 𝑋 𝐼 𝑌 ) )
208 52 207 pm2.61dane ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑋 𝐼 𝑌 ) )