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

Theorem mideulem 23841
Description: Lemma for mideu 23842. We can assume mideulem.9 "without loss of generality" (Contributed by Thierry Arnoux, 25-Nov-2019.)
Hypotheses
Ref Expression
colperpex.p  |-  P  =  ( Base `  G
)
colperpex.d  |-  .-  =  ( dist `  G )
colperpex.i  |-  I  =  (Itv `  G )
colperpex.l  |-  L  =  (LineG `  G )
colperpex.g  |-  ( ph  ->  G  e. TarskiG )
mideu.s  |-  S  =  (pInvG `  G )
mideu.1  |-  ( ph  ->  A  e.  P )
mideu.2  |-  ( ph  ->  B  e.  P )
mideulem.1  |-  ( ph  ->  A  =/=  B )
mideulem.2  |-  ( ph  ->  Q  e.  P )
mideulem.3  |-  ( ph  ->  O  e.  P )
mideulem.4  |-  ( ph  ->  T  e.  P )
mideulem.5  |-  ( ph  ->  ( A L B ) (⟂G `  G
) ( Q L B ) )
mideulem.6  |-  ( ph  ->  ( A L B ) (⟂G `  G
) ( A L O ) )
mideulem.7  |-  ( ph  ->  T  e.  ( A L B ) )
mideulem.8  |-  ( ph  ->  T  e.  ( Q I O ) )
mideulem.9  |-  ( ph  ->  ( A  .-  O
) (≤G `  G
) ( B  .-  Q ) )
Assertion
Ref Expression
mideulem  |-  ( ph  ->  E. x  e.  P  B  =  ( ( S `  x ) `  A ) )
Distinct variable groups:    x,  .-    x, A   
x, B    x, I    x, O    x, P    x, Q    x, T    ph, x
Allowed substitution hints:    S( x)    G( x)    L( x)

Proof of Theorem mideulem
Dummy variables  m  r  s  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 colperpex.p . . . 4  |-  P  =  ( Base `  G
)
2 colperpex.d . . . 4  |-  .-  =  ( dist `  G )
3 colperpex.i . . . 4  |-  I  =  (Itv `  G )
4 colperpex.l . . . 4  |-  L  =  (LineG `  G )
5 mideu.s . . . 4  |-  S  =  (pInvG `  G )
6 colperpex.g . . . . . 6  |-  ( ph  ->  G  e. TarskiG )
76ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  G  e. TarskiG )
87adantr 465 . . . 4  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  G  e. TarskiG )
9 eqid 2467 . . . 4  |-  ( S `
 x )  =  ( S `  x
)
10 mideu.2 . . . . . 6  |-  ( ph  ->  B  e.  P )
1110ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  B  e.  P
)
1211adantr 465 . . . 4  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  B  e.  P )
13 mideulem.3 . . . . . 6  |-  ( ph  ->  O  e.  P )
1413ad2antrr 725 . . . . 5  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  O  e.  P
)
1514adantr 465 . . . 4  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  O  e.  P )
16 mideu.1 . . . . 5  |-  ( ph  ->  A  e.  P )
1716ad3antrrr 729 . . . 4  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  A  e.  P )
18 simplr 754 . . . . 5  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  r  e.  P
)
1918adantr 465 . . . 4  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  -> 
r  e.  P )
20 simprl 755 . . . 4  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  x  e.  P )
21 mideulem.1 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  =/=  B )
2221necomd 2738 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  =/=  A )
2322neneqd 2669 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  B  =  A )
2423adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  -.  B  =  A )
25 mideulem.6 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A L B ) (⟂G `  G
) ( A L O ) )
264, 6, 25perpln2 23824 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A L O )  e.  ran  L
)
271, 3, 4, 6, 16, 13, 26tglnne 23750 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  =/=  O )
2827necomd 2738 . . . . . . . . . . . . . 14  |-  ( ph  ->  O  =/=  A )
2928neneqd 2669 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  O  =  A )
3029adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  -.  O  =  A )
3124, 30jca 532 . . . . . . . . . . 11  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  ( -.  B  =  A  /\  -.  O  =  A
) )
326adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  G  e. TarskiG )
3310adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  B  e.  P )
3416adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  A  e.  P )
3513adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  O  e.  P )
361, 3, 4, 6, 10, 16, 22tglinerflx2 23756 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  e.  ( B L A ) )
371, 3, 4, 6, 16, 10, 21tglinecom 23757 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A L B )  =  ( B L A ) )
3837, 25eqbrtrrd 4469 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( B L A ) (⟂G `  G
) ( A L O ) )
391, 2, 3, 4, 6, 10, 16, 36, 13, 38perprag 23833 . . . . . . . . . . . . . 14  |-  ( ph  ->  <" B A O ">  e.  (∟G `  G ) )
4039adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  <" B A O ">  e.  (∟G `  G ) )
41 simpr 461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  O  e.  ( B L A ) )
4241orcd 392 . . . . . . . . . . . . 13  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  ( O  e.  ( B L A )  \/  B  =  A ) )
431, 2, 3, 4, 5, 32, 33, 34, 35, 40, 42ragflat3 23819 . . . . . . . . . . . 12  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  ( B  =  A  \/  O  =  A ) )
44 oran 496 . . . . . . . . . . . 12  |-  ( ( B  =  A  \/  O  =  A )  <->  -.  ( -.  B  =  A  /\  -.  O  =  A ) )
4543, 44sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  O  e.  ( B L A ) )  ->  -.  ( -.  B  =  A  /\  -.  O  =  A ) )
4631, 45pm2.65da 576 . . . . . . . . . 10  |-  ( ph  ->  -.  O  e.  ( B L A ) )
4746ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  -.  O  e.  ( B L A ) )
4847adantr 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  -.  O  e.  ( B L A ) )
4937ad3antrrr 729 . . . . . . . 8  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  -> 
( A L B )  =  ( B L A ) )
5048, 49neleqtrrd 2580 . . . . . . 7  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  -.  O  e.  ( A L B ) )
5121ad3antrrr 729 . . . . . . . 8  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  A  =/=  B )
5251neneqd 2669 . . . . . . 7  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  -.  A  =  B
)
5350, 52jca 532 . . . . . 6  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  -> 
( -.  O  e.  ( A L B )  /\  -.  A  =  B ) )
54 pm4.56 495 . . . . . 6  |-  ( ( -.  O  e.  ( A L B )  /\  -.  A  =  B )  <->  -.  ( O  e.  ( A L B )  \/  A  =  B ) )
5553, 54sylib 196 . . . . 5  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  -.  ( O  e.  ( A L B )  \/  A  =  B ) )
561, 4, 3, 8, 17, 12, 15, 55ncolrot2 23706 . . . 4  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  -.  ( B  e.  ( O L A )  \/  O  =  A ) )
57 simprrr 764 . . . . . 6  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  x  e.  ( r
I O ) )
581, 2, 3, 8, 19, 20, 15, 57tgbtwncom 23635 . . . . 5  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  x  e.  ( O I r ) )
59 mideulem.4 . . . . . . . . 9  |-  ( ph  ->  T  e.  P )
6059ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  T  e.  P
)
6160adantr 465 . . . . . . 7  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  T  e.  P )
62 mideulem.7 . . . . . . . 8  |-  ( ph  ->  T  e.  ( A L B ) )
6362ad3antrrr 729 . . . . . . 7  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  T  e.  ( A L B ) )
64 simprrl 763 . . . . . . 7  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  x  e.  ( T I B ) )
651, 3, 4, 8, 61, 17, 12, 20, 63, 64coltr3 23770 . . . . . 6  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  x  e.  ( A L B ) )
6637ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  ( A L B )  =  ( B L A ) )
6747, 66neleqtrrd 2580 . . . . . . 7  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  -.  O  e.  ( A L B ) )
6867adantr 465 . . . . . 6  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  -.  O  e.  ( A L B ) )
69 nelne2 2797 . . . . . 6  |-  ( ( x  e.  ( A L B )  /\  -.  O  e.  ( A L B ) )  ->  x  =/=  O
)
7065, 68, 69syl2anc 661 . . . . 5  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  x  =/=  O )
711, 2, 3, 8, 15, 20, 19, 58, 70tgbtwnne 23637 . . . 4  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  O  =/=  r )
721, 2, 3, 4, 5, 6, 10, 16, 13israg 23810 . . . . . . . 8  |-  ( ph  ->  ( <" B A O ">  e.  (∟G `  G )  <->  ( B  .-  O )  =  ( B  .-  ( ( S `  A ) `
 O ) ) ) )
7339, 72mpbid 210 . . . . . . 7  |-  ( ph  ->  ( B  .-  O
)  =  ( B 
.-  ( ( S `
 A ) `  O ) ) )
7473ad5antr 733 . . . . . 6  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  -> 
( B  .-  O
)  =  ( B 
.-  ( ( S `
 A ) `  O ) ) )
758ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  G  e. TarskiG )
76 eqid 2467 . . . . . . . . 9  |-  ( S `
 A )  =  ( S `  A
)
771, 2, 3, 4, 5, 8, 17, 76, 15mircl 23783 . . . . . . . 8  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  -> 
( ( S `  A ) `  O
)  e.  P )
7877ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  -> 
( ( S `  A ) `  O
)  e.  P )
7917ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  A  e.  P )
8015ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  O  e.  P )
8119ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  -> 
r  e.  P )
8212ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  B  e.  P )
83 simplr 754 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  -> 
s  e.  P )
841, 2, 3, 4, 5, 75, 79, 76, 80mirbtwn 23780 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  A  e.  ( (
( S `  A
) `  O )
I O ) )
85 eqid 2467 . . . . . . . . 9  |-  ( S `
 B )  =  ( S `  B
)
861, 2, 3, 4, 5, 75, 82, 85, 83mirbtwn 23780 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  B  e.  ( (
( S `  B
) `  s )
I s ) )
87 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
r  =  ( ( S `  m ) `
 s ) )
88 oveq2 6292 . . . . . . . . . . . . . . . 16  |-  ( y  =  B  ->  (
r L y )  =  ( r L B ) )
8988breq1d 4457 . . . . . . . . . . . . . . 15  |-  ( y  =  B  ->  (
( r L y ) (⟂G `  G
) ( A L B )  <->  ( r L B ) (⟂G `  G
) ( A L B ) ) )
90 oveq2 6292 . . . . . . . . . . . . . . . 16  |-  ( y  =  m  ->  (
r L y )  =  ( r L m ) )
9190breq1d 4457 . . . . . . . . . . . . . . 15  |-  ( y  =  m  ->  (
( r L y ) (⟂G `  G
) ( A L B )  <->  ( r L m ) (⟂G `  G ) ( A L B ) ) )
9275ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  G  e. TarskiG )
931, 3, 4, 6, 16, 10, 21tgelrnln 23752 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( A L B )  e.  ran  L
)
9493ad7antr 737 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( A L B )  e.  ran  L
)
9581ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
r  e.  P )
9621ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  A  =/=  B )
9796neneqd 2669 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  -.  A  =  B )
9816ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  A  e.  P
)
99 simprr 756 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  ( A  .-  O )  =  ( B  .-  r ) )
10027ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  A  =/=  O
)
1011, 2, 3, 7, 98, 14, 11, 18, 99, 100tgcgrneq 23630 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  B  =/=  r
)
102101adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  B  =/=  r )
103102necomd 2738 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  r  =/=  B )
104103neneqd 2669 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  -.  r  =  B )
10597, 104jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  ( -.  A  =  B  /\  -.  r  =  B ) )
1067adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  G  e. TarskiG )
10716ad3antrrr 729 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  A  e.  P )
10811adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  B  e.  P )
10918adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  r  e.  P )
110 mideulem.2 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  Q  e.  P )
111110ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  Q  e.  P
)
112 mideulem.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( A L B ) (⟂G `  G
) ( Q L B ) )
1134, 6, 112perpln2 23824 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( Q L B )  e.  ran  L
)
1141, 3, 4, 6, 110, 10, 113tglnne 23750 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  Q  =/=  B )
1151, 3, 4, 6, 110, 10, 114tglinerflx2 23756 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  B  e.  ( Q L B ) )
1161, 2, 3, 4, 6, 93, 113, 112perpcom 23826 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( Q L B ) (⟂G `  G
) ( A L B ) )
117116, 37breqtrd 4471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( Q L B ) (⟂G `  G
) ( B L A ) )
1181, 2, 3, 4, 6, 110, 10, 115, 16, 117perprag 23833 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  <" Q B A ">  e.  (∟G `  G ) )
119118ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  <" Q B A ">  e.  (∟G `  G ) )
120114ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  Q  =/=  B
)
121 simprl 755 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  r  e.  ( B I Q ) )
1221, 4, 3, 7, 11, 18, 111, 121btwncolg3 23700 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  ( Q  e.  ( B L r )  \/  B  =  r ) )
1231, 2, 3, 4, 5, 7, 111, 11, 98, 18, 119, 120, 122ragcol 23812 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  <" r B A ">  e.  (∟G `  G ) )
1241, 2, 3, 4, 5, 7, 18, 11, 98, 123ragcom 23811 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  <" A B r ">  e.  (∟G `  G ) )
125124adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  <" A B r ">  e.  (∟G `  G )
)
126 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  r  e.  ( A L B ) )
127126orcd 392 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  (
r  e.  ( A L B )  \/  A  =  B ) )
1281, 2, 3, 4, 5, 106, 107, 108, 109, 125, 127ragflat3 23819 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  ( A  =  B  \/  r  =  B )
)
129 oran 496 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  =  B  \/  r  =  B )  <->  -.  ( -.  A  =  B  /\  -.  r  =  B ) )
130128, 129sylib 196 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  r  e.  ( A L B ) )  ->  -.  ( -.  A  =  B  /\  -.  r  =  B ) )
131105, 130pm2.65da 576 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  -.  r  e.  ( A L B ) )
132131ad5antr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  -.  r  e.  ( A L B ) )
1331, 2, 3, 4, 92, 94, 95, 132foot 23832 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  E! y  e.  ( A L B ) ( r L y ) (⟂G `  G )
( A L B ) )
13479ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  A  e.  P )
13582ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  B  e.  P )
13651ad4antr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  A  =/=  B )
1371, 3, 4, 92, 134, 135, 136tglinerflx2 23756 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  B  e.  ( A L B ) )
13820ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  x  e.  P )
139138ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  x  e.  P )
140 oveq2 6292 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  A  ->  (
r L y )  =  ( r L A ) )
141140breq1d 4457 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  A  ->  (
( r L y ) (⟂G `  G
) ( A L B )  <->  ( r L A ) (⟂G `  G
) ( A L B ) ) )
14293ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  ( A L B )  e.  ran  L )
1431, 2, 3, 4, 7, 142, 18, 131foot 23832 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  E! y  e.  ( A L B ) ( r L y ) (⟂G `  G
) ( A L B ) )
144143ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  E! y  e.  ( A L B ) ( r L y ) (⟂G `  G
) ( A L B ) )
14521ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  A  =/=  B
)
1461, 3, 4, 7, 98, 11, 145tglinerflx1 23755 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  A  e.  ( A L B ) )
147146ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  A  e.  ( A L B ) )
1481, 3, 4, 7, 98, 11, 145tglinerflx2 23756 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  B  e.  ( A L B ) )
149148ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  B  e.  ( A L B ) )
1508adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  G  e. TarskiG )
15118ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  r  e.  P )
15217adantr 465 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  A  e.  P )
153145neneqd 2669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  -.  A  =  B )
154131, 153jca 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  ( -.  r  e.  ( A L B )  /\  -.  A  =  B ) )
155 pm4.56 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( -.  r  e.  ( A L B )  /\  -.  A  =  B )  <->  -.  (
r  e.  ( A L B )  \/  A  =  B ) )
156154, 155sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  -.  ( r  e.  ( A L B )  \/  A  =  B ) )
1571, 3, 4, 7, 18, 98, 11, 156ncolne1 23747 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  r  =/=  A
)
158157ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  r  =/=  A )
159158necomd 2738 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  A  =/=  r )
160159necomd 2738 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  r  =/=  A )
1611, 3, 4, 150, 151, 152, 160tglinecom 23757 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( r L A )  =  ( A L r ) )
16214ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  O  e.  P )
16328ad4antr 731 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  O  =/=  A )
16420adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  x  e.  P )
165 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  x  =  A )
166165, 159eqnetrd 2760 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  x  =/=  r )
16771adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  O  =/=  r )
168167necomd 2738 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  r  =/=  O )
169 simplrr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) )
170169simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  x  e.  ( r I O ) )
1711, 3, 4, 150, 151, 162, 164, 168, 170btwnlng1 23741 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  x  e.  ( r L O ) )
1721, 3, 4, 150, 164, 151, 162, 166, 171, 168lnrot2 23746 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  O  e.  ( x L r ) )
173165oveq1d 6299 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( x L r )  =  ( A L r ) )
174172, 173eleqtrd 2557 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  O  e.  ( A L r ) )
1751, 3, 4, 150, 152, 151, 159, 162, 163, 174tglineelsb2 23754 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( A L r )  =  ( A L O ) )
176161, 175eqtrd 2508 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( r L A )  =  ( A L O ) )
1771, 2, 3, 4, 6, 93, 26, 25perpcom 23826 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( A L O ) (⟂G `  G
) ( A L B ) )
178177ad4antr 731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( A L O ) (⟂G `  G
) ( A L B ) )
179176, 178eqbrtrd 4467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( r L A ) (⟂G `  G
) ( A L B ) )
180142ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( A L B )  e.  ran  L
)
181101necomd 2738 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  r  =/=  B
)
1821, 3, 4, 7, 18, 11, 181tgelrnln 23752 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  ( r L B )  e.  ran  L )
183182ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( r L B )  e.  ran  L
)
1841, 3, 4, 7, 18, 11, 181tglinerflx2 23756 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  B  e.  ( r L B ) )
185148, 184elind 3688 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  B  e.  ( ( A L B )  i^i  ( r L B ) ) )
1861, 3, 4, 7, 18, 11, 181tglinerflx1 23755 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  r  e.  ( r L B ) )
1871, 2, 3, 4, 7, 142, 182, 185, 146, 186, 145, 181, 124ragperp 23830 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  ->  ( A L B ) (⟂G `  G
) ( r L B ) )
188187ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( A L B ) (⟂G `  G
) ( r L B ) )
1891, 2, 3, 4, 150, 180, 183, 188perpcom 23826 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  ( r L B ) (⟂G `  G
) ( A L B ) )
190141, 89, 144, 147, 149, 179, 189reu2eqd 3300 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  A  =  B )
19151adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  A  =/=  B )
192191neneqd 2669 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  x  =  A )  ->  -.  A  =  B )
193190, 192pm2.65da 576 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  -.  x  =  A
)
194193neqned 2670 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  x  =/=  A )
195194ad4antr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  x  =/=  A )
19665ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  x  e.  ( A L B ) )
197196ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  x  e.  ( A L B ) )
198 simplr 754 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  m  e.  P )
199195necomd 2738 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  A  =/=  x )
200 eqid 2467 . . . . . . . . . . . . . . . . . 18  |-  ( S `
 m )  =  ( S `  m
)
20180ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  O  e.  P )
20277ad4antr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( ( S `  A ) `  O
)  e.  P )
20383ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
s  e.  P )
204 simp-5r 768 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )
205204simprd 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) )
206205simprd 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  x  e.  ( r
I O ) )
2071, 2, 3, 92, 95, 139, 201, 206tgbtwncom 23635 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  x  e.  ( O I r ) )
208 simpllr 758 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )
209208simpld 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  x  e.  ( (
( S `  A
) `  O )
I s ) )
21039ad5antr 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  <" B A O ">  e.  (∟G `  G ) )
21151necomd 2738 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  ->  B  =/=  A )
212211ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  B  =/=  A )
213196orcd 392 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  -> 
( x  e.  ( A L B )  \/  A  =  B ) )
2141, 4, 3, 75, 79, 82, 138, 213colcom 23701 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  -> 
( x  e.  ( B L A )  \/  B  =  A ) )
2151, 4, 3, 75, 82, 79, 138, 214colrot1 23702 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  -> 
( B  e.  ( A L x )  \/  A  =  x ) )
2161, 2, 3, 4, 5, 75, 82, 79, 80, 138, 210, 212, 215ragcol 23812 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  ->  <" x A O ">  e.  (∟G `  G ) )
2171, 2, 3, 4, 5, 75, 138, 79, 80israg 23810 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  -> 
( <" x A O ">  e.  (∟G `  G )  <->  ( x  .-  O )  =  ( x  .-  ( ( S `  A ) `
 O ) ) ) )
218216, 217mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  -> 
( x  .-  O
)  =  ( x 
.-  ( ( S `
 A ) `  O ) ) )
219218ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( x  .-  O
)  =  ( x 
.-  ( ( S `
 A ) `  O ) ) )
220 simprr 756 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  r  e.  P )  /\  (
r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P
)  /\  ( x  e.  ( ( ( S `
 A ) `  O ) I s )  /\  ( x 
.-  s )  =  ( x  .-  r
) ) )  -> 
( x  .-  s
)  =  ( x 
.-  r ) )
221220ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( x  .-  s
)  =  ( x 
.-  r ) )
222221eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( x  .-  r
)  =  ( x 
.-  s ) )
223 eqidd 2468 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( ( S `  A ) `  O
)  =  ( ( S `  A ) `
 O ) )
22487eqcomd 2475 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( ( S `  m ) `  s
)  =  r )
2251, 2, 3, 4, 5, 92, 198, 200, 203, 224mircom 23785 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( ( S `  m ) `  r
)  =  s )
226225eqcomd 2475 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
s  =  ( ( S `  m ) `
 r ) )
2271, 2, 3, 4, 5, 92, 76, 200, 201, 202, 139, 95, 203, 134, 198, 207, 209, 219, 222, 223, 226krippen 23804 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  x  e.  ( A I m ) )
2281, 3, 4, 92, 134, 139, 198, 199, 227btwnlng3 23743 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  m  e.  ( A L x ) )
2291, 3, 4, 92, 134, 135, 136, 139, 195, 197, 198, 228tglineeltr 23753 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  m  e.  ( A L B ) )
230182ad5antr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( r L B )  e.  ran  L
)
231187ad5antr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( A L B ) (⟂G `  G
) ( r L B ) )
2321, 2, 3, 4, 92, 94, 230, 231perpcom 23826 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( r L B ) (⟂G `  G
) ( A L B ) )
233 nelne2 2797 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  e.  ( A L B )  /\  -.  r  e.  ( A L B ) )  ->  m  =/=  r
)
234229, 132, 233syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  m  =/=  r )
235234necomd 2738 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
r  =/=  m )
2361, 3, 4, 92, 95, 198, 235tgelrnln 23752 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
( r L m )  e.  ran  L
)
2371, 3, 4, 92, 95, 198, 235tglinerflx2 23756 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  m  e.  ( r L m ) )
238229, 237elind 3688 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  ->  m  e.  ( ( A L B )  i^i  ( r L m ) ) )
2391, 3, 4, 92, 95, 198, 235tglinerflx1 23755 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A  .-  O )  =  ( B  .-  r ) ) )  /\  (
x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  -> 
r  e.  ( r L m ) )
240 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  /\  m  =  x )  ->  m  =  x )
24192adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  /\  m  =  x )  ->  G  e. TarskiG )
242198adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  /\  m  =  x )  ->  m  e.  P )
243134adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  /\  m  =  x )  ->  A  e.  P )
244201adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  /\  m  =  x )  ->  O  e.  P )
245202adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  /\  m  =  x )  ->  ( ( S `  A ) `  O
)  e.  P )
246219adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( ( ( ( ph  /\  r  e.  P )  /\  ( r  e.  ( B I Q )  /\  ( A 
.-  O )  =  ( B  .-  r
) ) )  /\  ( x  e.  P  /\  ( x  e.  ( T I B )  /\  x  e.  ( r I O ) ) ) )  /\  s  e.  P )  /\  ( x  e.  ( ( ( S `  A ) `  O
) I s )  /\  ( x  .-  s )  =  ( x  .-  r ) ) )  /\  m  e.  P )  /\  r  =  ( ( S `
 m ) `  s ) )  /\  m  =  x )  ->  (