MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  midexlem Structured version   Unicode version
Theorem midexlem 23934
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 (midG ` G ) B ) for a midpoint implies its uniqueness, it cannot be used until uniqueness is proven, and until then, an equivalent mirror point notation B = ( M ` A ) has to be used. See mideu 23977 for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019.)
Hypotheses
Ref Expression
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
Ref Expression
midexlem |- ( ph -> E. x e. P B = ( M ` A ) )
Distinct variable groups:   x, .-   x, A   x, B   x, C   x, I   x, L   x, P   x, S   ph, x
Allowed substitution hints:   G( x)   M( x)
Proof of Theorem midexlem
Dummy variables p q r s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 midexlem.c . . . . 5 |- ( ph -> C e. P )
2 midexlem.m . . . . . . . . 9 |- M = ( S ` x )
3 fveq2 5852 . . . . . . . . 9 |- ( x = C -> ( S ` x ) = ( S ` C ) )
42, 3syl5eq 2494 . . . . . . . 8 |- ( x = C -> M = ( S ` C ) )
54fveq1d 5854 . . . . . . 7 |- ( x = C -> ( M ` A ) = ( ( S ` C ) ` A ) )
65eqeq2d 2455 . . . . . 6 |- ( x = C -> ( B = ( M ` A ) <-> B = ( ( S ` C ) ` A ) ) )
76rspcev 3194 . . . . 5 |- ( ( C e. P /\ B = ( ( S ` C ) ` A ) ) -> E. x e. P B = ( M ` A ) )
81, 7sylan 471 . . . 4 |- ( ( ph /\ B = ( ( S ` C ) ` A ) ) -> E. x e. P B = ( M ` A ) )
98adantlr 714 . . 3 |- ( ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) /\ B = ( ( S ` C ) ` A ) ) -> E. x e. P B = ( M ` A ) )
10 midexlem.a . . . . . 6 |- ( ph -> A e. P )
1110adantr 465 . . . . 5 |- ( ( ph /\ A = B ) -> A e. P )
12 mirval.p . . . . . . . 8 |- P = ( Base ` G )
13 mirval.d . . . . . . . 8 |- .- = ( dist ` G )
14 mirval.i . . . . . . . 8 |- I = (Itv ` G )
15 mirval.l . . . . . . . 8 |- L = (LineG ` G )
16 mirval.s . . . . . . . 8 |- S = (pInvG ` G )
17 mirval.g . . . . . . . 8 |- ( ph -> G e. TarskiG )
18 eqid 2441 . . . . . . . 8 |- ( S ` A ) = ( S ` A )
1912, 13, 14, 15, 16, 17, 10, 18mircinv 23913 . . . . . . 7 |- ( ph -> ( ( S ` A ) ` A ) = A )
2019adantr 465 . . . . . 6 |- ( ( ph /\ A = B ) -> ( ( S ` A ) ` A ) = A )
21 simpr 461 . . . . . 6 |- ( ( ph /\ A = B ) -> A = B )
2220, 21eqtr2d 2483 . . . . 5 |- ( ( ph /\ A = B ) -> B = ( ( S ` A ) ` A ) )
23 fveq2 5852 . . . . . . . . 9 |- ( x = A -> ( S ` x ) = ( S ` A ) )
242, 23syl5eq 2494 . . . . . . . 8 |- ( x = A -> M = ( S ` A ) )
2524fveq1d 5854 . . . . . . 7 |- ( x = A -> ( M ` A ) = ( ( S ` A ) ` A ) )
2625eqeq2d 2455 . . . . . 6 |- ( x = A -> ( B = ( M ` A ) <-> B = ( ( S ` A ) ` A ) ) )
2726rspcev 3194 . . . . 5 |- ( ( A e. P /\ B = ( ( S ` A ) ` A ) ) -> E. x e. P B = ( M ` A ) )
2811, 22, 27syl2anc 661 . . . 4 |- ( ( ph /\ A = B ) -> E. x e. P B = ( M ` A ) )
2928adantlr 714 . . 3 |- ( ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) /\ A = B ) -> E. x e. P B = ( M ` A ) )
3017adantr 465 . . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> G e. TarskiG )
31 eqid 2441 . . . 4 |- ( S ` C ) = ( S ` C )
3210adantr 465 . . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> A e. P )
33 midexlem.b . . . . 5 |- ( ph -> B e. P )
3433adantr 465 . . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> B e. P )
351adantr 465 . . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> C e. P )
36 simpr 461 . . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> ( C e. ( A L B ) \/ A = B ) )
37 midexlem.1 . . . . 5 |- ( ph -> ( C .- A ) = ( C .- B ) )
3837adantr 465 . . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> ( C .- A ) = ( C .- B ) )
3912, 13, 14, 15, 16, 30, 31, 32, 34, 35, 36, 38colmid 23930 . . 3 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> ( B = ( ( S ` C ) ` A ) \/ A = B ) )
409, 29, 39mpjaodan 784 . 2 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> E. x e. P B = ( M ` A ) )
4117adantr 465 . . . . . . . . . . 11 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> G e. TarskiG )
4241ad2antrr 725 . . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> G e. TarskiG )
4342ad2antrr 725 . . . . . . . . 9 |- ( ( ( ( ( ( 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 )
4443ad2antrr 725 . . . . . . . 8 |- ( ( ( ( ( ( ( ( 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 )
4544adantr 465 . . . . . . 7 |- ( ( ( ( ( ( ( ( ( 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 )
46 simprl 755 . . . . . . 7 |- ( ( ( ( ( ( ( ( ( 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 )
4710adantr 465 . . . . . . . . . . 11 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> A e. P )
4847ad2antrr 725 . . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> A e. P )
4948ad2antrr 725 . . . . . . . . 9 |- ( ( ( ( ( ( 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 )
5049ad2antrr 725 . . . . . . . 8 |- ( ( ( ( ( ( ( ( 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 )
5150adantr 465 . . . . . . 7 |- ( ( ( ( ( ( ( ( ( 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 )
5233ad3antrrr 729 . . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> B e. P )
5352ad2antrr 725 . . . . . . . . 9 |- ( ( ( ( ( ( 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 )
5453ad2antrr 725 . . . . . . . 8 |- ( ( ( ( ( ( ( ( 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 )
5554adantr 465 . . . . . . 7 |- ( ( ( ( ( ( ( ( ( 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 )
5645ad2antrr 725 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
57 simpllr 758 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( 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 )
5857ad2antrr 725 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
591adantr 465 . . . . . . . . . . . . . 14 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> C e. P )
6059ad2antrr 725 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> C e. P )
6160ad2antrr 725 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
6261ad2antrr 725 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( 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 )
6362adantr 465 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( 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 )
6463ad2antrr 725 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
6546ad2antrr 725 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
66 eqid 2441 . . . . . . . . 9 |- (cgrG ` G ) = (cgrG ` G )
6755ad2antrr 725 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
6851ad2antrr 725 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
69 simpr 461 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
7033adantr 465 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> B e. P )
71 simpr 461 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> -. ( C e. ( A L B ) \/ A = B ) )
7212, 14, 15, 41, 59, 47, 70, 71ncolne1 23870 . . . . . . . . . . . . . . 15 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> C =/= A )
7372ad7antr 737 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( 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 )
7473ad2antrr 725 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
7574adantr 465 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
7675necomd 2712 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
7769, 76eqnetrd 2734 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
7856adantr 465 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
7958adantr 465 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
8068adantr 465 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
8164adantr 465 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
82 simplr 754 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 )
8382ad3antrrr 729 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( 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 )
8483ad2antrr 725 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
8584adantr 465 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
8671ad9antr 741 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
8712, 15, 14, 56, 68, 67, 64, 86ncolrot2 23815 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
8817adantr 465 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> G e. TarskiG )
8933adantr 465 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> B e. P )
9010adantr 465 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> A e. P )
911adantr 465 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> C e. P )
92 simpr 461 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> ( C e. ( B L A ) \/ B = A ) )
9312, 15, 14, 88, 89, 90, 91, 92colcom 23810 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> ( C e. ( A L B ) \/ A = B ) )
9493stoic1a 1590 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> -. ( C e. ( B L A ) \/ B = A ) )
9594ad9antr 741 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
9612, 14, 15, 56, 64, 67, 68, 95ncolne1 23870 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
9796necomd 2712 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
98 simprl 755 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( 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 ) )
9998ad3antrrr 729 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( 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 ) )
10099ad2antrr 725 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
10112, 14, 15, 56, 64, 67, 84, 96, 100btwnlng3 23866 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
10212, 14, 15, 56, 67, 64, 84, 97, 101lncom 23867 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
10356adantr 465 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
10464adantr 465 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
10567adantr 465 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
106100adantr 465 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 ) )
107 simpr 461 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
108107oveq2d 6293 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 ) )
109106, 108eleqtrd 2531 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 ) )
11012, 13, 14, 103, 104, 105, 109axtgbtwnid 23728 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
11196adantr 465 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
112111neneqd 2643 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
113110, 112pm2.65da 576 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
114113neqned 2644 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
11512, 14, 15, 56, 67, 64, 68, 84, 87, 102, 114ncolncol 23891 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
11612, 15, 14, 56, 64, 68, 84, 115ncolcom 23813 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
117116adantr 465 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 ) )
118 simp-4r 766 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( 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 )
119118ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( 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 )
120119adantr 465 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( 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 )
121120ad2antrr 725 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
122 simp-4r 766 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( ( 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 ) ) )
123122simprd 463 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ( ( 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 ) )
124123eqcomd 2449 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( 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 ) )
125124ad2antrr 725 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
12612, 13, 14, 56, 68, 121, 67, 84, 125tgcgrcomlr 23736 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
127 simpllr 758 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( 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 ) )
128127ad5antr 733 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
129128simprd 463 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
130129necomd 2712 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
13112, 13, 14, 56, 121, 68, 84, 67, 126, 130tgcgrneq 23739 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
13212, 14, 15, 56, 64, 67, 68, 84, 95, 101, 131ncolncol 23891 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
13312, 14, 15, 56, 84, 67, 68, 132ncolne2 23871 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
134133necomd 2712 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
135 simp-4r 766 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) ) )
136135simpld 459 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
13712, 14, 15, 56, 68, 84, 58, 134, 136btwnlng1 23864 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
13812, 14, 15, 56, 84, 68, 58, 133, 137lncom 23867 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
139138adantr 465 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 ) )
140 simpr 461 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
14112, 14, 15, 78, 85, 80, 81, 79, 117, 139, 140ncolncol 23891 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 ) )
14212, 14, 15, 78, 79, 80, 81, 141ncolne2 23871 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( ( ( ( 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 )
14377, 142pm2.61dane 2759 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
144 simpllr 758 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) ) ) )
145144simprd 463 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) ) )
146145simprd 463 . . . . . . . . . 10 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
14712, 15, 14, 56, 58, 65, 64, 146btwncolg3 23809 . . . . . . . . 9 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
148 simplr 754 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( 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 )
149 simplr 754 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( 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 ) ) )
150149simprd 463 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( 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 ) )
151150ad2antrr 725 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
152 simprl 755 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
153127simpld 459 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) )
154153ad2antrr 725 . . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ( 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 ) )
155154adantr 465 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( 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 ) )
15637ad8antr 739 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( 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 ) )
157156eqcomd 2449 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( 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 ) )
15812, 13, 14, 45, 51, 55axtgcgrrflx 23724 . . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ( ( 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 ) )
15912, 13, 14, 45, 63, 51, 120, 63, 55, 83, 55, 51, 73, 155, 99, 156, 124, 157, 158axtg5seg 23727 . . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( ( 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 ) )
16012, 13, 14, 45, 120, 55, 83, 51, 159tgcgrcomlr 23736 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( 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 ) )
161160ad2antrr 725 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( ( ( ( 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 ) )
162 simprr 756 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( ( ( ( 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