Theorem midexlem 23770

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 23807 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.

Step	Hyp	Ref	Expression
1		midexlem.c	. . . . 5 |- ( ph -> C e. P )
2		midexlem.m	. . . . . . . . 9 |- M = ( S ` x )
3		fveq2 5857	. . . . . . . . 9 |- ( x = C -> ( S ` x ) = ( S ` C ) )
4	2, 3	syl5eq 2513	. . . . . . . 8 |- ( x = C -> M = ( S ` C ) )
5	4	fveq1d 5859	. . . . . . 7 |- ( x = C -> ( M ` A ) = ( ( S ` C ) ` A ) )
6	5	eqeq2d 2474	. . . . . 6 |- ( x = C -> ( B = ( M ` A ) <-> B = ( ( S ` C ) ` A ) ) )
7	6	rspcev 3207	. . . . 5 |- ( ( C e. P /\ B = ( ( S ` C ) ` A ) ) -> E. x e. P B = ( M ` A ) )
8	1, 7	sylan 471	. . . 4 |- ( ( ph /\ B = ( ( S ` C ) ` A ) ) -> E. x e. P B = ( M ` A ) )
9	8	adantlr 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 )
11	10	adantr 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 2460	. . . . . . . 8 |- ( S ` A ) = ( S ` A )
19	12, 13, 14, 15, 16, 17, 10, 18	mircinv 23754	. . . . . . 7 |- ( ph -> ( ( S ` A ) ` A ) = A )
20	19	adantr 465	. . . . . 6 |- ( ( ph /\ A = B ) -> ( ( S ` A ) ` A ) = A )
21		simpr 461	. . . . . 6 |- ( ( ph /\ A = B ) -> A = B )
22	20, 21	eqtr2d 2502	. . . . 5 |- ( ( ph /\ A = B ) -> B = ( ( S ` A ) ` A ) )
23		fveq2 5857	. . . . . . . . 9 |- ( x = A -> ( S ` x ) = ( S ` A ) )
24	2, 23	syl5eq 2513	. . . . . . . 8 |- ( x = A -> M = ( S ` A ) )
25	24	fveq1d 5859	. . . . . . 7 |- ( x = A -> ( M ` A ) = ( ( S ` A ) ` A ) )
26	25	eqeq2d 2474	. . . . . 6 |- ( x = A -> ( B = ( M ` A ) <-> B = ( ( S ` A ) ` A ) ) )
27	26	rspcev 3207	. . . . 5 |- ( ( A e. P /\ B = ( ( S ` A ) ` A ) ) -> E. x e. P B = ( M ` A ) )
28	11, 22, 27	syl2anc 661	. . . 4 |- ( ( ph /\ A = B ) -> E. x e. P B = ( M ` A ) )
29	28	adantlr 714	. . 3 |- ( ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) /\ A = B ) -> E. x e. P B = ( M ` A ) )
30	17	adantr 465	. . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> G e. TarskiG )
31		eqid 2460	. . . 4 |- ( S ` C ) = ( S ` C )
32	10	adantr 465	. . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> A e. P )
33		midexlem.b	. . . . 5 |- ( ph -> B e. P )
34	33	adantr 465	. . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> B e. P )
35	1	adantr 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 ) )
38	37	adantr 465	. . . 4 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> ( C .- A ) = ( C .- B ) )
39	12, 13, 14, 15, 16, 30, 31, 32, 34, 35, 36, 38	colmid 23766	. . 3 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> ( B = ( ( S ` C ) ` A ) \/ A = B ) )
40	9, 29, 39	mpjaodan 784	. 2 |- ( ( ph /\ ( C e. ( A L B ) \/ A = B ) ) -> E. x e. P B = ( M ` A ) )
41	17	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> G e. TarskiG )
42	41	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> G e. TarskiG )
43	42	ad2antrr 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 )
44	43	ad2antrr 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 )
45	44	adantr 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 )
47	10	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> A e. P )
48	47	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> A e. P )
49	48	ad2antrr 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 )
50	49	ad2antrr 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 )
51	50	adantr 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 )
52	33	ad3antrrr 729	. . . . . . . . . 10 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> B e. P )
53	52	ad2antrr 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 )
54	53	ad2antrr 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 )
55	54	adantr 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 )
56	45	ad2antrr 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		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 ) ) ) -> r e. P )
58	57	adantr 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 ) ) ) ) -> r e. P )
59	58	ad2antrr 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 )
60	1	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> C e. P )
61	60	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> C e. P )
62	61	ad2antrr 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 )
63	62	ad2antrr 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 )
64	63	adantr 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 )
65	64	ad2antrr 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 )
66	46	ad2antrr 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 )
67		eqid 2460	. . . . . . . . 9 |- (cgrG ` G ) = (cgrG ` G )
68	55	ad2antrr 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 )
69	51	ad2antrr 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 )
70		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 )
71	33	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> B e. P )
72		simpr 461	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> -. ( C e. ( A L B ) \/ A = B ) )
73	12, 14, 15, 41, 60, 47, 71, 72	ncolne1 23712	. . . . . . . . . . . . . . 15 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> C =/= A )
74	73	ad7antr 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 )
75	74	ad2antrr 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 )
76	75	adantr 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 )
77	76	necomd 2731	. . . . . . . . . . 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 )
78	70, 77	eqnetrd 2753	. . . . . . . . . 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 )
79	56	adantr 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 )
80	59	adantr 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 )
81	69	adantr 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 )
82	65	adantr 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 )
83		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 )
84	83	ad3antrrr 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 )
85	84	ad2antrr 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 )
86	85	adantr 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 )
87	72	ad9antr 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 ) )
88	56	adantr 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 "> ) ) /\ ( B e. ( C L A ) \/ C = A ) ) -> G e. TarskiG )
89	65	adantr 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 "> ) ) /\ ( B e. ( C L A ) \/ C = A ) ) -> C e. P )
90	69	adantr 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 "> ) ) /\ ( B e. ( C L A ) \/ C = A ) ) -> A e. P )
91	68	adantr 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 "> ) ) /\ ( B e. ( C L A ) \/ C = A ) ) -> B e. P )
92		simpr 461	. . . . . . . . . . . . . . . . . . 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 "> ) ) /\ ( B e. ( C L A ) \/ C = A ) ) -> ( B e. ( C L A ) \/ C = A ) )
93	12, 15, 14, 88, 89, 90, 91, 92	colrot1 23667	. . . . . . . . . . . . . . . . . 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 e. ( C L A ) \/ C = A ) ) -> ( C e. ( A L B ) \/ A = B ) )
94	93	ex 434	. . . . . . . . . . . . . . . . 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 L A ) \/ C = A ) -> ( C e. ( A L B ) \/ A = B ) ) )
95	94	con3d 133	. . . . . . . . . . . . . . . 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 ) -> -. ( B e. ( C L A ) \/ C = A ) ) )
96	87, 95	mpd 15	. . . . . . . . . . . . . . 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 ) )
97	17	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> G e. TarskiG )
98	33	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> B e. P )
99	10	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> A e. P )
100	1	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> C e. P )
101		simpr 461	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> ( C e. ( B L A ) \/ B = A ) )
102	12, 15, 14, 97, 98, 99, 100, 101	colcom 23666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( C e. ( B L A ) \/ B = A ) ) -> ( C e. ( A L B ) \/ A = B ) )
103	102	ex 434	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( C e. ( B L A ) \/ B = A ) -> ( C e. ( A L B ) \/ A = B ) ) )
104	103	con3d 133	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( -. ( C e. ( A L B ) \/ A = B ) -> -. ( C e. ( B L A ) \/ B = A ) ) )
105	104	imp 429	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) -> -. ( C e. ( B L A ) \/ B = A ) )
106	105	ad9antr 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 ) )
107	12, 14, 15, 56, 65, 68, 69, 106	ncolne1 23712	. . . . . . . . . . . . . . . . 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 )
108	107	necomd 2731	. . . . . . . . . . . . . . . 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 )
109		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 ) )
110	109	ad3antrrr 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 ) )
111	110	ad2antrr 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 ) )
112	12, 14, 15, 56, 65, 68, 85, 107, 111	btwnlng3 23708	. . . . . . . . . . . . . . . 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 ) )
113	12, 14, 15, 56, 68, 65, 85, 108, 112	lncom 23709	. . . . . . . . . . . . . . 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 ) )
114	56	adantr 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 )
115	65	adantr 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 )
116	68	adantr 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 )
117	111	adantr 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 ) )
118		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 )
119	118	oveq2d 6291	. . . . . . . . . . . . . . . . . . 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 ) )
120	117, 119	eleqtrd 2550	. . . . . . . . . . . . . . . . . 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 ) )
121	12, 13, 14, 114, 115, 116, 120	axtgbtwnid 23584	. . . . . . . . . . . . . . . . 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 )
122	107	adantr 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 )
123	122	neneqd 2662	. . . . . . . . . . . . . . . . 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 )
124	121, 123	pm2.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 )
125	124	neqned 2663	. . . . . . . . . . . . . . 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 )
126	12, 14, 15, 56, 68, 65, 69, 85, 96, 113, 125	ncolncol 23732	. . . . . . . . . . . . . 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 ) )
127	56	adantr 465	. . . . . . . . . . . . . . . . 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 e. ( A L C ) \/ A = C ) ) -> G e. TarskiG )
128	69	adantr 465	. . . . . . . . . . . . . . . . 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 e. ( A L C ) \/ A = C ) ) -> A e. P )
129	65	adantr 465	. . . . . . . . . . . . . . . . 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 e. ( A L C ) \/ A = C ) ) -> C e. P )
130	85	adantr 465	. . . . . . . . . . . . . . . . 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 e. ( A L C ) \/ A = C ) ) -> q e. P )
131		simpr 461	. . . . . . . . . . . . . . . . 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 e. ( A L C ) \/ A = C ) ) -> ( q e. ( A L C ) \/ A = C ) )
132	12, 15, 14, 127, 128, 129, 130, 131	colcom 23666	. . . . . . . . . . . . . . . 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. ( A L C ) \/ A = C ) ) -> ( q e. ( C L A ) \/ C = A ) )
133	132	ex 434	. . . . . . . . . . . . . . 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. ( A L C ) \/ A = C ) -> ( q e. ( C L A ) \/ C = A ) ) )
134	133	con3d 133	. . . . . . . . . . . . . 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 ) -> -. ( q e. ( A L C ) \/ A = C ) ) )
135	126, 134	mpd 15	. . . . . . . . . . . . 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 ) )
136	135	adantr 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 ) )
137		simplr 754	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ -. ( C e. ( A L B ) \/ A = B ) ) /\ p e. P ) /\ ( A e. ( C I p ) /\ A =/= p ) ) -> p e. P )
138	137	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 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 )
139	138	ad2antrr 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 )
140	139	adantr 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 )
141	140	ad2antrr 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 )
142		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 ) ) )
143	142	simprd 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 ) )
144	143	eqcomd 2468	. . . . . . . . . . . . . . . . . . 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 ) )
145	144	ad2antrr 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 ) )
146	12, 13, 14, 56, 69, 141, 68, 85, 145	tgcgrcomlr 23592	. . . . . . . . . . . . . . . . 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 ) )
147		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 ) )
148	147	ad5antr 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 ) )
149	148	simprd 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 )
150	149	necomd 2731	. . . . . . . . . . . . . . . . 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 )
151	12, 13, 14, 56, 141, 69, 85, 68, 146, 150	tgcgrneq 23595	. . . . . . . . . . . . . . . 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 )
152	12, 14, 15, 56, 65, 68, 69, 85, 106, 112, 151	ncolncol 23732	. . . . . . . . . . . . . . 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 ) )
153	12, 14, 15, 56, 85, 68, 69, 152	ncolne2 23713	. . . . . . . . . . . . . 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 )
154	153	necomd 2731	. . . . . . . . . . . . . . . 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 =/= q )
155	154	neneqd 2662	. . . . . . . . . . . . . . 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 )
156		simplr 754	. . . . . . . . . . . . . . . . . . . 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 ) ) ) ) -> ( r e. ( A I q ) /\ r e. ( B I p ) ) )
157	156	ad2antrr 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 ) ) ) /\ ( x e. P /\ ( x e. ( 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 ) ) )
158	157	simpld 459	. . . . . . . . . . . . . . . . . 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. ( A I q ) )
159	12, 15, 14, 56, 69, 85, 59, 158	btwncolg1 23663	. . . . . . . . . . . . . . . . 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 e. ( A L q ) \/ A = q ) )
160	159	orcomd 388	. . . . . . . . . . . . . . . 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 = q \/ r e. ( A L q ) ) )
161	160	ord 377	. . . . . . . . . . . . . . 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 ) )