Metamath Proof Explorer

Theorem midexlem

Description: Lemma for the existence of a middle point. Lemma 7.25 of Schwabhauser p. 55. This proof of the existence of a midpoint requires the existence of a third point C equidistant to A and B This condition will be removed later. Because the operation notation ( A ( midGG ) B ) for a midpoint implies its uniqueness, it cannot be used until uniqueness is proven, and until then, an equivalent mirror point notation B = ( MA ) has to be used. See mideu for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019)

Ref Expression
Hypotheses mirval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirval.d ⊢ − = ( dist ‘ 𝐺 )
mirval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
mirval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
mirval.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
midexlem.m ⊢ 𝑀 = ( 𝑆 ‘ 𝑥 )
midexlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
midexlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
midexlem.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
midexlem.1 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝐵 ) )
Assertion midexlem ( 𝜑 → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )

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 midexlem.m ⊢ 𝑀 = ( 𝑆 ‘ 𝑥 )
8 midexlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
9 midexlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
10 midexlem.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
11 midexlem.1 ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝐵 ) )
12 fveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝐶 ) )
13 7 12 syl5eq ⊢ ( 𝑥 = 𝐶 → 𝑀 = ( 𝑆 ‘ 𝐶 ) )
14 13 fveq1d ⊢ ( 𝑥 = 𝐶 → ( 𝑀 ‘ 𝐴 ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) )
15 14 rspceeqv ⊢ ( ( 𝐶 ∈ 𝑃 ∧ 𝐵 = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
16 10 15 sylan ⊢ ( ( 𝜑 ∧ 𝐵 = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
17 16 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝐵 = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
18 eqid ⊢ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐴 )
19 1 2 3 4 5 6 8 18 mircinv ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐴 ) = 𝐴 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐴 ) = 𝐴 )
21 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
22 20 21 eqtr2d ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐴 ) )
23 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝐴 ) )
24 7 23 syl5eq ⊢ ( 𝑥 = 𝐴 → 𝑀 = ( 𝑆 ‘ 𝐴 ) )
25 24 fveq1d ⊢ ( 𝑥 = 𝐴 → ( 𝑀 ‘ 𝐴 ) = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐴 ) )
26 25 rspceeqv ⊢ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐴 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
27 8 22 26 syl2an2r ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
28 27 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝐴 = 𝐵 ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
29 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 𝐺 ∈ TarskiG )
30 eqid ⊢ ( 𝑆 ‘ 𝐶 ) = ( 𝑆 ‘ 𝐶 )
31 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 𝐴 ∈ 𝑃 )
32 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 𝐵 ∈ 𝑃 )
33 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 𝐶 ∈ 𝑃 )
34 simpr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
35 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝐵 ) )
36 1 2 3 4 5 29 30 31 32 33 34 35 colmid ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → ( 𝐵 = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐴 ) ∨ 𝐴 = 𝐵 ) )
37 17 28 36 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
38 6 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 𝐺 ∈ TarskiG )
39 38 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐺 ∈ TarskiG )
40 39 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → 𝐺 ∈ TarskiG )
41 40 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) → 𝐺 ∈ TarskiG )
42 41 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝐺 ∈ TarskiG )
43 simprl ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝑥 ∈ 𝑃 )
44 8 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 𝐴 ∈ 𝑃 )
45 44 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐴 ∈ 𝑃 )
46 45 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → 𝐴 ∈ 𝑃 )
47 46 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) → 𝐴 ∈ 𝑃 )
48 47 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝐴 ∈ 𝑃 )
49 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐵 ∈ 𝑃 )
50 49 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → 𝐵 ∈ 𝑃 )
51 50 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) → 𝐵 ∈ 𝑃 )
52 51 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝐵 ∈ 𝑃 )
53 42 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐺 ∈ TarskiG )
54 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝑟 ∈ 𝑃 )
55 54 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑟 ∈ 𝑃 )
56 10 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 𝐶 ∈ 𝑃 )
57 56 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐶 ∈ 𝑃 )
58 57 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → 𝐶 ∈ 𝑃 )
59 58 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) → 𝐶 ∈ 𝑃 )
60 59 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝐶 ∈ 𝑃 )
61 60 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐶 ∈ 𝑃 )
62 43 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑥 ∈ 𝑃 )
63 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
64 52 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐵 ∈ 𝑃 )
65 48 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐴 ∈ 𝑃 )
66 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 = 𝐴 ) → 𝑟 = 𝐴 )
67 9 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 𝐵 ∈ 𝑃 )
68 simpr ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
69 1 3 4 38 56 44 67 68 ncolne1 ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 𝐶 ≠ 𝐴 )
70 69 ad7antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝐶 ≠ 𝐴 )
71 70 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐶 ≠ 𝐴 )
72 71 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 = 𝐴 ) → 𝐶 ≠ 𝐴 )
73 72 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 = 𝐴 ) → 𝐴 ≠ 𝐶 )
74 66 73 eqnetrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 = 𝐴 ) → 𝑟 ≠ 𝐶 )
75 53 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 ≠ 𝐴 ) → 𝐺 ∈ TarskiG )
76 55 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 ≠ 𝐴 ) → 𝑟 ∈ 𝑃 )
77 65 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 ≠ 𝐴 ) → 𝐴 ∈ 𝑃 )
78 61 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 ≠ 𝐴 ) → 𝐶 ∈ 𝑃 )
79 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → 𝑞 ∈ 𝑃 )
80 79 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝑞 ∈ 𝑃 )
81 80 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑞 ∈ 𝑃 )
82 81 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 ≠ 𝐴 ) → 𝑞 ∈ 𝑃 )
83 68 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
84 1 4 3 53 65 64 61 83 ncolrot2 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ¬ ( 𝐵 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
85 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ) → 𝐺 ∈ TarskiG )
86 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ) → 𝐵 ∈ 𝑃 )
87 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ) → 𝐴 ∈ 𝑃 )
88 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ) → 𝐶 ∈ 𝑃 )
89 simpr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ) → ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
90 1 4 3 85 86 87 88 89 colcom ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
91 90 stoic1a ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → ¬ ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
92 91 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ¬ ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
93 1 3 4 53 61 64 65 92 ncolne1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐶 ≠ 𝐵 )
94 93 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐵 ≠ 𝐶 )
95 simprl ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) )
96 95 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) )
97 96 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) )
98 1 3 4 53 61 64 81 93 97 btwnlng3 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑞 ∈ ( 𝐶 𝐿 𝐵 ) )
99 1 3 4 53 64 61 81 94 98 lncom ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑞 ∈ ( 𝐵 𝐿 𝐶 ) )
100 53 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑞 = 𝐶 ) → 𝐺 ∈ TarskiG )
101 61 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑞 = 𝐶 ) → 𝐶 ∈ 𝑃 )
102 64 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑞 = 𝐶 ) → 𝐵 ∈ 𝑃 )
103 97 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑞 = 𝐶 ) → 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) )
104 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑞 = 𝐶 ) → 𝑞 = 𝐶 )
105 104 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑞 = 𝐶 ) → ( 𝐶 𝐼 𝑞 ) = ( 𝐶 𝐼 𝐶 ) )
106 103 105 eleqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑞 = 𝐶 ) → 𝐵 ∈ ( 𝐶 𝐼 𝐶 ) )
107 1 2 3 100 101 102 106 axtgbtwnid ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑞 = 𝐶 ) → 𝐶 = 𝐵 )
108 93 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑞 = 𝐶 ) → 𝐶 ≠ 𝐵 )
109 108 neneqd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑞 = 𝐶 ) → ¬ 𝐶 = 𝐵 )
110 107 109 pm2.65da ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ¬ 𝑞 = 𝐶 )
111 110 neqned ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑞 ≠ 𝐶 )
112 1 3 4 53 64 61 65 81 84 99 111 ncolncol ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ¬ ( 𝑞 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
113 1 4 3 53 61 65 81 112 ncolcom ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ¬ ( 𝑞 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
114 113 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 ≠ 𝐴 ) → ¬ ( 𝑞 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
115 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → 𝑝 ∈ 𝑃 )
116 115 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) → 𝑝 ∈ 𝑃 )
117 116 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝑝 ∈ 𝑃 )
118 117 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑝 ∈ 𝑃 )
119 simp-4r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) )
120 119 simprd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) )
121 120 eqcomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ( 𝐴 − 𝑝 ) = ( 𝐵 − 𝑞 ) )
122 121 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐴 − 𝑝 ) = ( 𝐵 − 𝑞 ) )
123 1 2 3 53 65 118 64 81 122 tgcgrcomlr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑝 − 𝐴 ) = ( 𝑞 − 𝐵 ) )
124 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) )
125 124 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) )
126 125 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐴 ≠ 𝑝 )
127 126 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑝 ≠ 𝐴 )
128 1 2 3 53 118 65 81 64 123 127 tgcgrneq ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑞 ≠ 𝐵 )
129 1 3 4 53 61 64 65 81 92 98 128 ncolncol ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ¬ ( 𝑞 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
130 1 3 4 53 81 64 65 129 ncolne2 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑞 ≠ 𝐴 )
131 130 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐴 ≠ 𝑞 )
132 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) )
133 132 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) )
134 1 3 4 53 65 81 55 131 133 btwnlng1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑟 ∈ ( 𝐴 𝐿 𝑞 ) )
135 1 3 4 53 81 65 55 130 134 lncom ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑟 ∈ ( 𝑞 𝐿 𝐴 ) )
136 135 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 ≠ 𝐴 ) → 𝑟 ∈ ( 𝑞 𝐿 𝐴 ) )
137 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 ≠ 𝐴 ) → 𝑟 ≠ 𝐴 )
138 1 3 4 75 82 77 78 76 114 136 137 ncolncol ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 ≠ 𝐴 ) → ¬ ( 𝑟 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
139 1 3 4 75 76 77 78 138 ncolne2 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) ∧ 𝑟 ≠ 𝐴 ) → 𝑟 ≠ 𝐶 )
140 74 139 pm2.61dane ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑟 ≠ 𝐶 )
141 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) )
142 141 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) )
143 142 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) )
144 1 4 3 53 55 62 61 143 btwncolg3 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐶 ∈ ( 𝑟 𝐿 𝑥 ) ∨ 𝑟 = 𝑥 ) )
145 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑠 ∈ 𝑃 )
146 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) )
147 146 simprd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) )
148 147 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) )
149 simprl ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) )
150 124 simpld ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) )
151 150 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) )
152 151 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) )
153 11 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ( 𝐶 − 𝐴 ) = ( 𝐶 − 𝐵 ) )
154 153 eqcomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ( 𝐶 − 𝐵 ) = ( 𝐶 − 𝐴 ) )
155 1 2 3 42 48 52 axtgcgrrflx ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐴 ) )
156 1 2 3 42 60 48 117 60 52 80 52 48 70 152 96 153 121 154 155 axtg5seg ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ( 𝑝 − 𝐵 ) = ( 𝑞 − 𝐴 ) )
157 1 2 3 42 117 52 80 48 156 tgcgrcomlr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ( 𝐵 − 𝑝 ) = ( 𝐴 − 𝑞 ) )
158 157 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐵 − 𝑝 ) = ( 𝐴 − 𝑞 ) )
159 simprr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ )
160 1 2 3 63 53 64 55 118 65 145 81 159 cgr3simp2 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑟 − 𝑝 ) = ( 𝑠 − 𝑞 ) )
161 1 2 3 53 64 65 axtgcgrrflx ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐵 − 𝐴 ) = ( 𝐴 − 𝐵 ) )
162 1 2 3 53 64 55 118 65 65 145 81 64 148 149 158 160 161 123 tgifscgr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑟 − 𝐴 ) = ( 𝑠 − 𝐵 ) )
163 simp-10l ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝜑 )
164 125 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) )
165 1 3 4 53 61 65 118 71 164 btwnlng3 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑝 ∈ ( 𝐶 𝐿 𝐴 ) )
166 1 3 4 53 61 65 64 118 83 165 127 ncolncol ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ¬ ( 𝑝 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
167 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝑝 𝐿 𝐴 ) ∨ 𝑝 = 𝐴 ) ) → 𝐺 ∈ TarskiG )
168 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝑝 𝐿 𝐴 ) ∨ 𝑝 = 𝐴 ) ) → 𝑝 ∈ 𝑃 )
169 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝑝 𝐿 𝐴 ) ∨ 𝑝 = 𝐴 ) ) → 𝐴 ∈ 𝑃 )
170 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝑝 𝐿 𝐴 ) ∨ 𝑝 = 𝐴 ) ) → 𝐵 ∈ 𝑃 )
171 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝑝 𝐿 𝐴 ) ∨ 𝑝 = 𝐴 ) ) → ( 𝐵 ∈ ( 𝑝 𝐿 𝐴 ) ∨ 𝑝 = 𝐴 ) )
172 1 4 3 167 168 169 170 171 colrot1 ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝑝 𝐿 𝐴 ) ∨ 𝑝 = 𝐴 ) ) → ( 𝑝 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
173 172 stoic1a ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ¬ ( 𝑝 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → ¬ ( 𝐵 ∈ ( 𝑝 𝐿 𝐴 ) ∨ 𝑝 = 𝐴 ) )
174 163 118 166 173 syl21anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ¬ ( 𝐵 ∈ ( 𝑝 𝐿 𝐴 ) ∨ 𝑝 = 𝐴 ) )
175 1 3 4 53 118 65 64 166 ncolne2 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑝 ≠ 𝐵 )
176 175 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝐵 ≠ 𝑝 )
177 176 neneqd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ¬ 𝐵 = 𝑝 )
178 1 4 3 53 65 81 55 133 btwncolg1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑟 ∈ ( 𝐴 𝐿 𝑞 ) ∨ 𝐴 = 𝑞 ) )
179 1 2 3 53 55 65 145 64 162 tgcgrcomlr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐴 − 𝑟 ) = ( 𝐵 − 𝑠 ) )
180 120 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) )
181 1 2 3 53 118 81 axtgcgrrflx ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑝 − 𝑞 ) = ( 𝑞 − 𝑝 ) )
182 1 2 3 53 64 55 118 81 65 145 81 118 148 149 158 160 180 181 tgifscgr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑟 − 𝑞 ) = ( 𝑠 − 𝑝 ) )
183 1 2 3 53 65 145 81 149 tgbtwncom ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑠 ∈ ( 𝑞 𝐼 𝐴 ) )
184 1 2 3 42 52 54 117 147 tgbtwncom ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝑟 ∈ ( 𝑝 𝐼 𝐵 ) )
185 184 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑟 ∈ ( 𝑝 𝐼 𝐵 ) )
186 160 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑠 − 𝑞 ) = ( 𝑟 − 𝑝 ) )
187 1 2 3 53 145 81 55 118 186 tgcgrcomlr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑞 − 𝑠 ) = ( 𝑝 − 𝑟 ) )
188 1 2 3 63 53 64 55 118 65 145 81 159 cgr3simp1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐵 − 𝑟 ) = ( 𝐴 − 𝑠 ) )
189 188 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐴 − 𝑠 ) = ( 𝐵 − 𝑟 ) )
190 1 2 3 53 65 145 64 55 189 tgcgrcomlr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑠 − 𝐴 ) = ( 𝑟 − 𝐵 ) )
191 1 2 3 53 81 145 65 118 55 64 183 185 187 190 tgcgrextend ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑞 − 𝐴 ) = ( 𝑝 − 𝐵 ) )
192 1 2 63 53 65 55 81 64 145 118 179 182 191 trgcgr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ⟨“ 𝐴 𝑟 𝑞 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐵 𝑠 𝑝 ”⟩ )
193 1 4 3 53 65 55 81 63 64 145 118 178 192 lnxfr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑠 ∈ ( 𝐵 𝐿 𝑝 ) ∨ 𝐵 = 𝑝 ) )
194 193 orcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐵 = 𝑝 ∨ 𝑠 ∈ ( 𝐵 𝐿 𝑝 ) ) )
195 194 ord ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( ¬ 𝐵 = 𝑝 → 𝑠 ∈ ( 𝐵 𝐿 𝑝 ) ) )
196 177 195 mpd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑠 ∈ ( 𝐵 𝐿 𝑝 ) )
197 1 3 4 53 64 118 55 176 148 btwnlng1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑟 ∈ ( 𝐵 𝐿 𝑝 ) )
198 1 3 4 53 65 81 145 131 149 btwnlng1 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑠 ∈ ( 𝐴 𝐿 𝑞 ) )
199 1 3 4 53 64 118 65 81 174 196 197 198 134 tglineinteq ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → 𝑠 = 𝑟 )
200 199 oveq1d ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑠 − 𝐵 ) = ( 𝑟 − 𝐵 ) )
201 162 200 eqtr2d ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑟 − 𝐵 ) = ( 𝑟 − 𝐴 ) )
202 154 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝐶 − 𝐵 ) = ( 𝐶 − 𝐴 ) )
203 1 4 3 53 55 61 62 63 64 65 2 140 144 201 202 lncgr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) ) → ( 𝑥 − 𝐵 ) = ( 𝑥 − 𝐴 ) )
204 1 2 3 63 42 52 54 117 48 80 147 157 tgcgrxfr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ∃ 𝑠 ∈ 𝑃 ( 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ∧ ⟨“ 𝐵 𝑟 𝑝 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐴 𝑠 𝑞 ”⟩ ) )
205 203 204 r19.29a ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → ( 𝑥 − 𝐵 ) = ( 𝑥 − 𝐴 ) )
206 simprrl ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) )
207 1 2 3 42 48 43 52 206 tgbtwncom ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝑥 ∈ ( 𝐵 𝐼 𝐴 ) )
208 1 2 3 4 5 42 43 7 48 52 205 207 ismir ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) ) ) → 𝐵 = ( 𝑀 ‘ 𝐴 ) )
209 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) → 𝑟 ∈ 𝑃 )
210 simprr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) → 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) )
211 1 2 3 41 59 51 116 47 209 151 210 axtgpasch ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐵 ) ∧ 𝑥 ∈ ( 𝑟 𝐼 𝐶 ) ) )
212 208 211 reximddv ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
213 1 2 3 40 58 46 115 150 tgbtwncom ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → 𝐴 ∈ ( 𝑝 𝐼 𝐶 ) )
214 1 2 3 40 58 50 79 95 tgbtwncom ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → 𝐵 ∈ ( 𝑞 𝐼 𝐶 ) )
215 1 2 3 40 115 79 58 46 50 213 214 axtgpasch ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → ∃ 𝑟 ∈ 𝑃 ( 𝑟 ∈ ( 𝐴 𝐼 𝑞 ) ∧ 𝑟 ∈ ( 𝐵 𝐼 𝑝 ) ) )
216 212 215 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
217 simplr ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝑝 ∈ 𝑃 )
218 1 2 3 39 57 49 45 217 axtgsegcon ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → ∃ 𝑞 ∈ 𝑃 ( 𝐵 ∈ ( 𝐶 𝐼 𝑞 ) ∧ ( 𝐵 − 𝑞 ) = ( 𝐴 − 𝑝 ) ) )
219 216 218 r19.29a ⊢ ( ( ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
220 1 fvexi ⊢ 𝑃 ∈ V
221 220 a1i ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 𝑃 ∈ V )
222 221 56 44 69 nehash2 ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
223 1 2 3 38 56 44 222 tgbtwndiff ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → ∃ 𝑝 ∈ 𝑃 ( 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) )
224 219 223 r19.29a ⊢ ( ( 𝜑 ∧ ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )
225 37 224 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 𝐵 = ( 𝑀 ‘ 𝐴 ) )