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

Theorem midexlem 23084
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 existence, it cannot be used until the existence is proven, and until then, an equivalent mirror point notation  B  =  ( M `  A ) has to be used. (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 5689 . . . . . . . . 9  |-  ( x  =  C  ->  ( S `  x )  =  ( S `  C ) )
42, 3syl5eq 2485 . . . . . . . 8  |-  ( x  =  C  ->  M  =  ( S `  C ) )
54fveq1d 5691 . . . . . . 7  |-  ( x  =  C  ->  ( M `  A )  =  ( ( S `
 C ) `  A ) )
65eqeq2d 2452 . . . . . 6  |-  ( x  =  C  ->  ( B  =  ( M `  A )  <->  B  =  ( ( S `  C ) `  A
) ) )
76rspcev 3071 . . . . 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 23069 . . . . . . 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 2474 . . . . 5  |-  ( (
ph  /\  A  =  B )  ->  B  =  ( ( S `
 A ) `  A ) )
23 fveq2 5689 . . . . . . . . 9  |-  ( x  =  A  ->  ( S `  x )  =  ( S `  A ) )
242, 23syl5eq 2485 . . . . . . . 8  |-  ( x  =  A  ->  M  =  ( S `  A ) )
2524fveq1d 5691 . . . . . . 7  |-  ( x  =  A  ->  ( M `  A )  =  ( ( S `
 A ) `  A ) )
2625eqeq2d 2452 . . . . . 6  |-  ( x  =  A  ->  ( B  =  ( M `  A )  <->  B  =  ( ( S `  A ) `  A
) ) )
2726rspcev 3071 . . . . 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 23080 . . 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 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 )
5857adantr 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 )
5958ad2antrr 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 )
601adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  -.  ( C  e.  ( A L B )  \/  A  =  B ) )  ->  C  e.  P )
6160ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  -.  ( C  e.  ( A L B )  \/  A  =  B ) )  /\  p  e.  P )  /\  ( A  e.  ( C I p )  /\  A  =/=  p ) )  ->  C  e.  P
)
6261ad2antrr 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
)
6362ad2antrr 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 )
6463adantr 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 )
6564ad2antrr 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 )
6646ad2antrr 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 2441 . . . . . . . . 9  |-  (cgrG `  G )  =  (cgrG `  G )
6855ad2antrr 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 )
6951ad2antrr 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 )
7133adantr 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 ) )
7312, 14, 15, 41, 60, 47, 71, 72ncolne1 23030 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  ( C  e.  ( A L B )  \/  A  =  B ) )  ->  C  =/=  A )
7473ad7antr 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 )
7574ad2antrr 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 )
7675adantr 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 )
7776necomd 2693 . . . . . . . . . . 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 )
7870, 77eqnetrd 2624 . . . . . . . . . 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 )
7956adantr 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 )
8059adantr 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 )
8169adantr 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 )
8265adantr 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
)
8483ad3antrrr 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 )
8584ad2antrr 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 )
8685adantr 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 )
8772ad9antr 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 ) )
8856adantr 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 )
8965adantr 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 )
9069adantr 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 )
9168adantr 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 ) )
9312, 15, 14, 88, 89, 90, 91, 92colrot1 22991 . . . . . . . . . . . . . . . . . 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 ) )
9493ex 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 ) ) )
9594con3d 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 ) ) )
9687, 95mpd 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 ) )
9717adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( C  e.  ( B L A )  \/  B  =  A ) )  ->  G  e. TarskiG )
9833adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( C  e.  ( B L A )  \/  B  =  A ) )  ->  B  e.  P )
9910adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( C  e.  ( B L A )  \/  B  =  A ) )  ->  A  e.  P )
1001adantr 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 ) )
10212, 15, 14, 97, 98, 99, 100, 101colcom 22990 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( C  e.  ( B L A )  \/  B  =  A ) )  -> 
( C  e.  ( A L B )  \/  A  =  B ) )
103102ex 434 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( C  e.  ( B L A )  \/  B  =  A )  ->  ( C  e.  ( A L B )  \/  A  =  B ) ) )
104103con3d 133 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( -.  ( C  e.  ( A L B )  \/  A  =  B )  ->  -.  ( C  e.  ( B L A )  \/  B  =  A ) ) )
105104imp 429 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  -.  ( C  e.  ( A L B )  \/  A  =  B ) )  ->  -.  ( C  e.  ( B L A )  \/  B  =  A ) )
106105ad9antr 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 ) )
10712, 14, 15, 56, 65, 68, 69, 106ncolne1 23030 . . . . . . . . . . . . . . . . 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 )
108107necomd 2693 . . . . . . . . . . . . . . . 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 ) )
110109ad3antrrr 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 ) )
111110ad2antrr 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 ) )
11212, 14, 15, 56, 65, 68, 85, 107, 111btwnlng3 23026 . . . . . . . . . . . . . . . 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 ) )
11312, 14, 15, 56, 68, 65, 85, 108, 112lncom 23027 . . . . . . . . . . . . . . 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 ) )
11456adantr 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 )
11565adantr 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 )
11668adantr 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 )
117111adantr 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 )
119118oveq2d 6105 . . . . . . . . . . . . . . . . . . 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 ) )
120117, 119eleqtrd 2517 . . . . . . . . . . . . . . . . . 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 ) )
12112, 13, 14, 114, 115, 116, 120axtgbtwnid 22925 . . . . . . . . . . . . . . . . 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 )
122107adantr 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 )
123122neneqd 2622 . . . . . . . . . . . . . . . . 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 )
124121, 123pm2.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 )
125124neneqad 2679 . . . . . . . . . . . . . . 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 )
12612, 14, 15, 56, 68, 65, 69, 85, 96, 113, 125ncolncol 23049 . . . . . . . . . . . . . 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 ) )
12756adantr 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 )
12869adantr 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 )
12965adantr 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 )
13085adantr 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 ) )
13212, 15, 14, 127, 128, 129, 130, 131colcom 22990 . . . . . . . . . . . . . . . 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 ) )
133132ex 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 ) ) )
134133con3d 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 ) ) )
135126, 134mpd 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 ) )
136135adantr 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
)
138137ad2antrr 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
)
139138ad2antrr 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 )
140139adantr 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 )
141140ad2antrr 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 ) ) )
143142simprd 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 ) )
144143eqcomd 2446 . . . . . . . . . . . . . . . . . . 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 ) )
145144ad2antrr 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
) )
14612, 13, 14, 56, 69, 141, 68, 85, 145tgcgrcomlr 22932 . . . . . . . . . . . . . . . . 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 ) )
148147ad5antr 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 ) )
149148simprd 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 )
150149necomd 2693 . . . . . . . . . . . . . . . . 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 )
15112, 13, 14, 56, 141, 69, 85, 68, 146, 150tgcgrneq 22935 . . . . . . . . . . . . . . . 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 )
15212, 14, 15, 56, 65, 68, 69, 85, 106, 112, 151ncolncol 23049 . . . . . . . . . . . . . . 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 ) )
15312, 14, 15, 56, 85, 68, 69, 152ncolne2 23031 . . . . . . . . . . . . . 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 )
154153necomd 2693 . . . . . . . . . . . . . . . 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 )
155154neneqd 2622 . . . . . . . . . . . . . . 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 ) ) )
157156ad2antrr 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 ) ) )
158157simpld 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 ) )
15912, 15, 14, 56, 69, 85, 59, 158btwncolg1 22987 . . . . . . . . . . . . . . . . 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 ) )
160159orcomd 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 ) ) )
161160ord 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 ) ) )  /\