MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  midexlem Structured version   Unicode version

Theorem midexlem 23934
Description: Lemma for the existence of a middle point. Lemma 7.25 of [Schwabhauser] p. 55. This proof of the existence of a midpoint requires the existence of a third point  C equidistant to  A and  B This condition will be removed later. Because the operation notation  ( A (midG `  G ) B ) for a midpoint implies its uniqueness, it cannot be used until uniqueness is proven, and until then, an equivalent mirror point notation  B  =  ( M `  A ) has to be used. See mideu 23977 for the existence and uniqueness of the midpoint. (Contributed by Thierry Arnoux, 25-Aug-2019.)
Hypotheses
Ref Expression
mirval.p  |-  P  =  ( Base `  G
)
mirval.d  |-  .-  =  ( dist `  G )
mirval.i  |-  I  =  (Itv `  G )
mirval.l  |-  L  =  (LineG `  G )
mirval.s  |-  S  =  (pInvG `  G )
mirval.g  |-  ( ph  ->  G  e. TarskiG )
midexlem.m  |-  M  =  ( S `  x
)
midexlem.a  |-  ( ph  ->  A  e.  P )
midexlem.b  |-  ( ph  ->  B  e.  P )
midexlem.c  |-  ( ph  ->  C  e.  P )
midexlem.1  |-  ( ph  ->  ( C  .-  A
)  =  ( C 
.-  B ) )
Assertion
Ref Expression
midexlem  |-  ( ph  ->  E. x  e.  P  B  =  ( M `  A ) )
Distinct variable groups:    x,  .-    x, A   
x, B    x, C    x, I    x, L    x, P    x, S    ph, x
Allowed substitution hints:    G( x)    M( x)

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