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 
|- P = ( Base ` G )
mirval.d 
|- .- = ( dist ` G )
mirval.i 
|- I = ( Itv ` G )
mirval.l 
|- L = ( LineG ` G )
mirval.s 
|- S = ( pInvG ` G )
mirval.g 
|- ( ph -> G e. TarskiG )
midexlem.m 
|- M = ( S ` x )
midexlem.a 
|- ( ph -> A e. P )
midexlem.b 
|- ( ph -> B e. P )
midexlem.c 
|- ( ph -> C e. P )
midexlem.1 
|- ( ph -> ( C .- A ) = ( C .- B ) )
Assertion midexlem 
|- ( ph -> E. x e. P B = ( M ` A ) )

Proof

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