MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  midexlem Structured version   Visualization version   Unicode version
Theorem midexlem 25587
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 25630 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 6191 . . . . . . . . 9 |- ( x = C -> ( S ` x ) = ( S ` C ) )
42, 3syl5eq 2668 . . . . . . . 8 |- ( x = C -> M = ( S ` C ) )
54fveq1d 6193 . . . . . . 7 |- ( x = C -> ( M ` A ) = ( ( S ` C ) ` A ) )
65eqeq2d 2632 . . . . . 6 |- ( x = C -> ( B = ( M ` A ) <-> B = ( ( S ` C ) ` A ) ) )
76rspcev 3309 . . . . 5 |- ( ( C e. P /\ B = ( ( S ` C ) ` A ) ) -> E. x e. P B = ( M ` A ) )
81, 7sylan 488 . . . 4 |- ( ( ph /\ B = ( ( S ` C ) ` A ) ) -> E. x e. P B = ( M ` A ) )
98adantlr 751 . . 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 481 . . . . 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 2622 . . . . . . . 8 |- ( S ` A ) = ( S ` A )
1912, 13, 14, 15, 16, 17, 10, 18mircinv 25563 . . . . . . 7 |- ( ph -> ( ( S ` A ) ` A ) = A )
2019adantr 481 . . . . . 6 |- ( ( ph /\ A = B ) -> ( ( S ` A ) ` A ) = A )
21 simpr 477 . . . . . 6 |- ( ( ph /\ A = B ) -> A = B )
2220, 21eqtr2d 2657 . . . . 5 |- ( ( ph /\ A = B ) -> B = ( ( S ` A ) ` A ) )
23 fveq2 6191 . . . . . . . . 9 |- ( x = A -> ( S ` x ) = ( S ` A ) )
242, 23syl5eq 2668 . . . . . . . 8 |- ( x = A -> M = ( S ` A ) )
2524fveq1d 6193 . . . . . . 7 |- ( x = A -> ( M ` A ) = ( ( S ` A ) ` A ) )
2625eqeq2d 2632 . . . . . 6 |- ( x = A -> ( B = ( M ` A ) <-> B = ( ( S ` A ) ` A ) ) )
2726rspcev 3309 . . . . 5 |- ( ( A e. P /\ B = ( ( S ` A ) ` A ) ) -> E. x e. P B = ( M ` A ) )
2811, 22, 27syl2anc 693 . . . 4 |- ( ( ph /\ A = B ) -> E. x e. P B = ( M ` A ) )
2928adantlr 751 . . 3 |- ( ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) /\ A = B ) -> E. x e. P B = ( M ` A ) )
3017adantr 481 . . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> G e. TarskiG )
31 eqid 2622 . . . 4 |- ( S ` C ) = ( S ` C )
3210adantr 481 . . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> A e. P )
33 midexlem.b . . . . 5 |- ( ph -> B e. P )
3433adantr 481 . . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> B e. P )
351adantr 481 . . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> C e. P )
36 simpr 477 . . . 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 481 . . . 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 25583 . . 3 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> ( B = ( ( S ` C ) ` A ) \/ A = B ) )
409, 29, 39mpjaodan 827 . 2 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> E. x e. P B = ( M ` A ) )
4117adantr 481 . . . . . . . . . . 11 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> G e. TarskiG )
4241ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> G e. TarskiG )
4342ad2antrr 762 . . . . . . . . 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 762 . . . . . . . 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 481 . . . . . . 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 794 . . . . . . 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 481 . . . . . . . . . . 11 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> A e. P )
4847ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> A e. P )
4948ad2antrr 762 . . . . . . . . 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 762 . . . . . . . 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 481 . . . . . . 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 766 . . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> B e. P )
5352ad2antrr 762 . . . . . . . . 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 762 . . . . . . . 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 481 . . . . . . 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 762 . . . . . . . . 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 799 . . . . . . . . . 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 762 . . . . . . . . 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 481 . . . . . . . . . . . . . 14 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> C e. P )
6059ad2antrr 762 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> C e. P )
6160ad2antrr 762 . . . . . . . . . . . 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 762 . . . . . . . . . . 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 481 . . . . . . . . . 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 762 . . . . . . . . 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 762 . . . . . . . . 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 2622 . . . . . . . . 9 |- (cgrG ` G ) = (cgrG ` G )
6755ad2antrr 762 . . . . . . . . 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 762 . . . . . . . . 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 477 . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> B e. P )
71 simpr 477 . . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> -. ( C e. ( A L B ) \/ A = B ) )
7212, 14, 15, 41, 59, 47, 70, 71ncolne1 25520 . . . . . . . . . . . . . . 15 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> C =/= A )
7372ad7antr 774 . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . 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 481 . . . . . . . . . . . 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 2849 . . . . . . . . . . 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 2861 . . . . . . . . . 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 481 . . . . . . . . . . 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 481 . . . . . . . . . . 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 481 . . . . . . . . . . 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 481 . . . . . . . . . . 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 792 . . . . . . . . . . . . . . 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 766 . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . 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 481 . . . . . . . . . . . 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 778 . . . . . . . . . . . . . . . 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 25458 . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> G e. TarskiG )
8933adantr 481 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> B e. P )
9010adantr 481 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> A e. P )
911adantr 481 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> C e. P )
92 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> ( C e. ( B L A ) \/ B = A ) )
9312, 15, 14, 88, 89, 90, 91, 92colcom 25453 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> ( C e. ( A L B ) \/ A = B ) )
9493stoic1a 1697 . . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> -. ( C e. ( B L A ) \/ B = A ) )
9594ad9antr 778 . . . . . . . . . . . . . . . . . 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 25520 . . . . . . . . . . . . . . . . 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 2849 . . . . . . . . . . . . . . . 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 794 . . . . . . . . . . . . . . . . . . 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 766 . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . 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 25516 . . . . . . . . . . . . . . . 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 25517 . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . 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 6666 . . . . . . . . . . . . . . . . . . 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 2703 . . . . . . . . . . . . . . . . . 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 25365 . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . 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 2799 . . . . . . . . . . . . . . . . 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 600 . . . . . . . . . . . . . . . 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 2801 . . . . . . . . . . . . . . 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 25541 . . . . . . . . . . . . . 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 25456 . . . . . . . . . . . . 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 481 . . . . . . . . . . . 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 807 . . . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . 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 807 . . . . . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . . . . . 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 2628 . . . . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . . . . 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 25375 . . . . . . . . . . . . . . . . 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 799 . . . . . . . . . . . . . . . . . . . 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 770 . . . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . . . 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 2849 . . . . . . . . . . . . . . . . 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 25378 . . . . . . . . . . . . . . . 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 25541 . . . . . . . . . . . . . . 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 25521 . . . . . . . . . . . . . 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 2849 . . . . . . . . . . . . . . 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 807 . . . . . . . . . . . . . . . 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 475 . . . . . . . . . . . . . . 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 25514 . . . . . . . . . . . . . 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 25517 . . . . . . . . . . . . 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 481 . . . . . . . . . . . 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 477 . . . . . . . . . . . 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 25541 . . . . . . . . . . 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 25521 . . . . . . . . . 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 2881 . . . . . . . . 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 799 . . . . . . . . . . . 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 479 . . . . . . . . . . 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 479 . . . . . . . . . 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 25452 . . . . . . . . 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 792 . . . . . . . . . . 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 792 . . . . . . . . . . . . 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 479 . . . . . . . . . . . 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 762 . . . . . . . . . . 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 794 . . . . . . . . . . 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 475 . . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . 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 776 . . . . . . . . . . . . . 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 2628 . . . . . . . . . . . . . 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 25361 . . . . . . . . . . . . . 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 25364 . . . . . . . . . . . . 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 25375 . . . . . . . . . . . 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 762 . . . . . . . . . . 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 796 . . . . . . . . . . . 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 "> ) ) -> <" B r p "> (cgrG ` G ) <" A s q "> )
16312, 13, 14, 66, 56, 67, 58, 121, 68, 148, 84, 162cgr3simp2 25416 . . . . . . . . . . 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 .- p ) = ( s .- q ) )
16412, 13, 14, 56, 67, 68axtgcgrrflx 25361 . . . . . . . . . . 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 .- A ) = ( A .- B ) )
16512, 13, 14, 56, 67, 58, 121, 68, 68, 148, 84, 67, 151, 152, 161, 163, 164, 126tgifscgr 25403 . . . . . . . . . 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 ) = ( s .- B ) )
166 simp-10l 818 . . . . . . . . . . . . 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 "> ) ) -> ph )
167128simpld 475 . . . . . . . . . . . . . . 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 e. ( C I p ) )
16812, 14, 15, 56, 64, 68, 121, 74, 167btwnlng3 25516 . . . . . . . . . . . . . 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 "> ) ) -> p e. ( C L A ) )
16912, 14, 15, 56, 64, 68, 67, 121, 86, 168, 130ncolncol 25541 . . . . . . . . . . . . 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 "> ) ) -> -. ( p e. ( A L B ) \/ A = B ) )
17017ad2antrr 762 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. P ) /\ ( B e. ( p L A ) \/ p = A ) ) -> G e. TarskiG )
171 simplr 792 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. P ) /\ ( B e. ( p L A ) \/ p = A ) ) -> p e. P )
17210ad2antrr 762 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. P ) /\ ( B e. ( p L A ) \/ p = A ) ) -> A e. P )
17333ad2antrr 762 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. P ) /\ ( B e. ( p L A ) \/ p = A ) ) -> B e. P )
174 simpr 477 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ p e. P ) /\ ( B e. ( p L A ) \/ p = A ) ) -> ( B e. ( p L A ) \/ p = A ) )
17512, 15, 14, 170, 171, 172, 173, 174colrot1 25454 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ p e. P ) /\ ( B e. ( p L A ) \/ p = A ) ) -> ( p e. ( A L B ) \/ A = B ) )
176175stoic1a 1697 . . . . . . . . . . . . 13 |- ( ( ( ph /\ p e. P ) /\ -. ( p e. ( A L B ) \/ A = B ) ) -> -. ( B e. ( p L A ) \/ p = A ) )
177166, 121, 169, 176syl21anc 1325 . . . . . . . . . . . 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 "> ) ) -> -. ( B e. ( p L A ) \/ p = A ) )
17812, 14, 15, 56, 121, 68, 67, 169ncolne2 25521 . . . . . . . . . . . . . . 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 "> ) ) -> p =/= B )
179178necomd 2849 . . . . . . . . . . . . . 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 "> ) ) -> B =/= p )
180179neneqd 2799 . . . . . . . . . . . . 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 "> ) ) -> -. B = p )
18112, 15, 14, 56, 68, 84, 58, 136btwncolg1 25450 . . . . . . . . . . . . . . . 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 L q ) \/ A = q ) )
18212, 13, 14, 56, 58, 68, 148, 67, 165tgcgrcomlr 25375 . . . . . . . . . . . . . . . . 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 "> ) ) -> ( A .- r ) = ( B .- s ) )
183123ad2antrr 762 . . . . . . . . . . . . . . . . . 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 "> ) ) -> ( B .- q ) = ( A .- p ) )
18412, 13, 14, 56, 121, 84axtgcgrrflx 25361 . . . . . . . . . . . . . . . . . 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 "> ) ) -> ( p .- q ) = ( q .- p ) )
18512, 13, 14, 56, 67, 58, 121, 84, 68, 148, 84, 121, 151, 152, 161, 163, 183, 184tgifscgr 25403 . . . . . . . . . . . . . . . . 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 "> ) ) -> ( r .- q ) = ( s .- p ) )
18612, 13, 14, 56, 68, 148, 84, 152tgbtwncom 25383 . . . . . . . . . . . . . . . . . 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 "> ) ) -> s e. ( q I A ) )
18712, 13, 14, 45, 55, 57, 120, 150tgbtwncom 25383 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) -> r e. ( p I B ) )
188187ad2antrr 762 . . . . . . . . . . . . . . . . . 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 "> ) ) -> r e. ( p I B ) )
189163eqcomd 2628 . . . . . . . . . . . . . . . . . . 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 "> ) ) -> ( s .- q ) = ( r .- p ) )
19012, 13, 14, 56, 148, 84, 58, 121, 189tgcgrcomlr 25375 . . . . . . . . . . . . . . . . . 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 .- s ) = ( p .- r ) )
19112, 13, 14, 66, 56, 67, 58, 121, 68, 148, 84, 162cgr3simp1 25415 . . . . . . . . . . . . . . . . . . . 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 "> ) ) -> ( B .- r ) = ( A .- s ) )
192191eqcomd 2628 . . . . . . . . . . . . . . . . . . 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 .- s ) = ( B .- r ) )
19312, 13, 14, 56, 68, 148, 67, 58, 192tgcgrcomlr 25375 . . . . . . . . . . . . . . . . . 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 "> ) ) -> ( s .- A ) = ( r .- B ) )
19412, 13, 14, 56, 84, 148, 68, 121, 58, 67, 186, 188, 190, 193tgcgrextend 25380 . . . . . . . . . . . . . . . . 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 .- A ) = ( p .- B ) )
19512, 13, 66, 56, 68, 58, 84, 67, 148, 121, 182, 185, 194trgcgr 25411 . . . . . . . . . . . . . . . 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 "> ) ) -> <" A r q "> (cgrG ` G ) <" B s p "> )
19612, 15, 14, 56, 68, 58, 84, 66, 67, 148, 121, 181, 195lnxfr 25461 . . . . . . . . . . . . . . 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 "> ) ) -> ( s e. ( B L p ) \/ B = p ) )
197196orcomd 403 . . . . . . . . . . . . . 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 "> ) ) -> ( B = p \/ s e. ( B L p ) ) )
198197ord 392 . . . . . . . . . . . . 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 "> ) ) -> ( -. B = p -> s e. ( B L p ) ) )
199180, 198mpd 15 . . . . . . . . . . . 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 "> ) ) -> s e. ( B L p ) )
20012, 14, 15, 56, 67, 121, 58, 179, 151btwnlng1 25514 . . . . . . . . . . . 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 e. ( B L p ) )
20112, 14, 15, 56, 68, 84, 148, 134, 152btwnlng1 25514 . . . . . . . . . . . 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 "> ) ) -> s e. ( A L q ) )
20212, 14, 15, 56, 67, 121, 68, 84, 177, 199, 200, 201, 137tglineinteq 25540 . . . . . . . . . . 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 = r )
203202oveq1d 6665 . . . . . . . . . 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 "> ) ) -> ( s .- B ) = ( r .- B ) )
204165, 203eqtr2d 2657 . . . . . . . . 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 .- B ) = ( r .- A ) )
205157ad2antrr 762 . . . . . . . . 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 .- B ) = ( C .- A ) )
20612, 15, 14, 56, 58, 64, 65, 66, 67, 68, 13, 143, 147, 204, 205lncgr 25464 . . . . . . . 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 ) ) ) /\ ( 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 ) )
20712, 13, 14, 66, 45, 55, 57, 120, 51, 83, 150, 160tgcgrxfr 25413 . . . . . . . 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 ) ) ) /\ ( 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 "> ) )
208206, 207r19.29a 3078 . . . . . . 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 .- B ) = ( x .- A ) )
209 simprrl 804 . . . . . . . 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 ) ) ) /\ ( x e. P /\ ( x e. ( A I B ) /\ x e. ( r I C ) ) ) ) -> x e. ( A I B ) )
21012, 13, 14, 45, 51, 46, 55, 209tgbtwncom 25383 . . . . . . 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. ( B I A ) )
21112, 13, 14, 15, 16, 45, 46, 2, 51, 55, 208, 210ismir 25554 . . . . . 6 |- ( ( ( ( ( ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ 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 ) )
212 simplr 792 . . . . . . 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 ) ) ) -> r e. P )
213 simprr 796 . . . . . . 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 ) ) ) -> r e. ( B I p ) )
21412, 13, 14, 44, 62, 54, 119, 50, 212, 154, 213axtgpasch 25366 . . . . . 6 |- ( ( ( ( ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ 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 ) ) )
215211, 214reximddv 3018 . . . . 5 |- ( ( ( ( ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ 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 ) )
21612, 13, 14, 43, 61, 49, 118, 153tgbtwncom 25383 . . . . . 6 |- ( ( ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ 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 ) )
21712, 13, 14, 43, 61, 53, 82, 98tgbtwncom 25383 . . . . . 6 |- ( ( ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ 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 ) )
21812, 13, 14, 43, 118, 82, 61, 49, 53, 216, 217axtgpasch 25366 . . . . 5 |- ( ( ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ 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 ) ) )
219215, 218r19.29a 3078 . . . 4 |- ( ( ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ 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 ) )
220 simplr 792 . . . . 5 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> p e. P )
22112, 13, 14, 42, 60, 52, 48, 220axtgsegcon 25363 . . . 4 |- ( ( ( ( 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 ) ) )
222219, 221r19.29a 3078 . . 3 |- ( ( ( ( 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 ) )
223 fvex 6201 . . . . . . 7 |- ( Base ` G ) e. _V
22412, 223eqeltri 2697 . . . . . 6 |- P e. _V
225224a1i 11 . . . . 5 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> P e. _V )
226225, 59, 47, 72nehash2 13256 . . . 4 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> 2 <_ ( # ` P ) )
22712, 13, 14, 41, 59, 47, 226tgbtwndiff 25401 . . 3 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> E. p e. P ( A e. ( C I p ) /\ A =/= p ) )
228222, 227r19.29a 3078 . 2 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> E. x e. P B = ( M ` A ) )
22940, 228pm2.61dan 832 1 |- ( ph -> E. x e. P B = ( M ` A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   E.wrex 2913   _Vcvv 3200   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   <"cs3 13587   Basecbs 15857   distcds 15950  TarskiGcstrkg 25329  Itvcitv 25335  LineGclng 25336  cgrGccgrg 25405  pInvGcmir 25547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-hash 13118  df-word 13299  df-concat 13301  df-s1 13302  df-s2 13593  df-s3 13594  df-trkgc 25347  df-trkgb 25348  df-trkgcb 25349  df-trkg 25352  df-cgrg 25406  df-mir 25548
This theorem is referenced by:  footex  25613  colperpexlem3  25624  opphllem  25627
  Copyright terms: Public domain W3C validator