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	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑋 𝐼 𝑌 ) )