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

Theorem opphllem6 24244
Description: First part of Lemma 9.4 of [Schwabhauser] p. 68. (Contributed by Thierry Arnoux, 3-Mar-2020.)
Hypotheses
Ref Expression
hpg.p  |-  P  =  ( Base `  G
)
hpg.d  |-  .-  =  ( dist `  G )
hpg.i  |-  I  =  (Itv `  G )
hpg.o  |-  O  =  { <. a ,  b
>.  |  ( (
a  e.  ( P 
\  D )  /\  b  e.  ( P  \  D ) )  /\  E. t  e.  D  t  e.  ( a I b ) ) }
opphl.l  |-  L  =  (LineG `  G )
opphl.d  |-  ( ph  ->  D  e.  ran  L
)
opphl.g  |-  ( ph  ->  G  e. TarskiG )
opphl.k  |-  K  =  ( c  e.  P  |->  { <. a ,  b
>.  |  ( (
a  e.  P  /\  b  e.  P )  /\  ( a  =/=  c  /\  b  =/=  c  /\  ( a  e.  ( c I b )  \/  b  e.  ( c I a ) ) ) ) } )
opphllem5.n  |-  N  =  ( (pInvG `  G
) `  M )
opphllem5.a  |-  ( ph  ->  A  e.  P )
opphllem5.c  |-  ( ph  ->  C  e.  P )
opphllem5.r  |-  ( ph  ->  R  e.  D )
opphllem5.s  |-  ( ph  ->  S  e.  D )
opphllem5.m  |-  ( ph  ->  M  e.  P )
opphllem5.o  |-  ( ph  ->  A O C )
opphllem5.p  |-  ( ph  ->  D (⟂G `  G
) ( A L R ) )
opphllem5.q  |-  ( ph  ->  D (⟂G `  G
) ( C L S ) )
opphllem5.u  |-  ( ph  ->  U  e.  P )
opphllem6.v  |-  ( ph  ->  ( N `  R
)  =  S )
Assertion
Ref Expression
opphllem6  |-  ( ph  ->  ( U ( K `
 R ) A  <-> 
( N `  U
) ( K `  S ) C ) )
Distinct variable groups:    A, a,
b, c, t    D, a, b, t    C, a, b, c, t    G, a, b, c, t    L, a, b, t    I, a, b, c, t    t, K    M, a, b, c, t    t, O    N, a, b, c, t    P, a, b, c, t    R, a, b, c, t    S, a, b, c, t    U, a, b, c, t    ph, a,
b, t    .- , a, b, t
Allowed substitution hints:    ph( c)    D( c)    K( a, b, c)    L( c)    .- ( c)    O( a, b, c)

Proof of Theorem opphllem6
StepHypRef Expression
1 hpg.p . . . 4  |-  P  =  ( Base `  G
)
2 hpg.d . . . 4  |-  .-  =  ( dist `  G )
3 hpg.i . . . 4  |-  I  =  (Itv `  G )
4 opphl.l . . . 4  |-  L  =  (LineG `  G )
5 eqid 2382 . . . 4  |-  (pInvG `  G )  =  (pInvG `  G )
6 opphl.g . . . . 5  |-  ( ph  ->  G  e. TarskiG )
76adantr 463 . . . 4  |-  ( (
ph  /\  R  =  S )  ->  G  e. TarskiG )
8 opphllem5.n . . . 4  |-  N  =  ( (pInvG `  G
) `  M )
9 opphl.k . . . 4  |-  K  =  ( c  e.  P  |->  { <. a ,  b
>.  |  ( (
a  e.  P  /\  b  e.  P )  /\  ( a  =/=  c  /\  b  =/=  c  /\  ( a  e.  ( c I b )  \/  b  e.  ( c I a ) ) ) ) } )
10 opphllem5.m . . . . 5  |-  ( ph  ->  M  e.  P )
1110adantr 463 . . . 4  |-  ( (
ph  /\  R  =  S )  ->  M  e.  P )
12 opphllem5.a . . . . 5  |-  ( ph  ->  A  e.  P )
1312adantr 463 . . . 4  |-  ( (
ph  /\  R  =  S )  ->  A  e.  P )
14 opphllem5.c . . . . 5  |-  ( ph  ->  C  e.  P )
1514adantr 463 . . . 4  |-  ( (
ph  /\  R  =  S )  ->  C  e.  P )
16 opphllem5.u . . . . 5  |-  ( ph  ->  U  e.  P )
1716adantr 463 . . . 4  |-  ( (
ph  /\  R  =  S )  ->  U  e.  P )
18 opphl.d . . . . . . . 8  |-  ( ph  ->  D  e.  ran  L
)
19 opphllem5.r . . . . . . . 8  |-  ( ph  ->  R  e.  D )
201, 4, 3, 6, 18, 19tglnpt 24056 . . . . . . 7  |-  ( ph  ->  R  e.  P )
21 opphllem5.p . . . . . . . 8  |-  ( ph  ->  D (⟂G `  G
) ( A L R ) )
224, 6, 21perpln2 24208 . . . . . . 7  |-  ( ph  ->  ( A L R )  e.  ran  L
)
231, 3, 4, 6, 12, 20, 22tglnne 24128 . . . . . 6  |-  ( ph  ->  A  =/=  R )
2423adantr 463 . . . . 5  |-  ( (
ph  /\  R  =  S )  ->  A  =/=  R )
25 opphllem6.v . . . . . . . 8  |-  ( ph  ->  ( N `  R
)  =  S )
2625adantr 463 . . . . . . 7  |-  ( (
ph  /\  R  =  S )  ->  ( N `  R )  =  S )
27 simpr 459 . . . . . . 7  |-  ( (
ph  /\  R  =  S )  ->  R  =  S )
2826, 27eqtr4d 2426 . . . . . 6  |-  ( (
ph  /\  R  =  S )  ->  ( N `  R )  =  R )
291, 2, 3, 4, 5, 6, 10, 8, 20mirinv 24167 . . . . . . 7  |-  ( ph  ->  ( ( N `  R )  =  R  <-> 
M  =  R ) )
3029adantr 463 . . . . . 6  |-  ( (
ph  /\  R  =  S )  ->  (
( N `  R
)  =  R  <->  M  =  R ) )
3128, 30mpbid 210 . . . . 5  |-  ( (
ph  /\  R  =  S )  ->  M  =  R )
3224, 31neeqtrrd 2682 . . . 4  |-  ( (
ph  /\  R  =  S )  ->  A  =/=  M )
33 opphllem5.s . . . . . . . 8  |-  ( ph  ->  S  e.  D )
341, 4, 3, 6, 18, 33tglnpt 24056 . . . . . . 7  |-  ( ph  ->  S  e.  P )
35 opphllem5.q . . . . . . . 8  |-  ( ph  ->  D (⟂G `  G
) ( C L S ) )
364, 6, 35perpln2 24208 . . . . . . 7  |-  ( ph  ->  ( C L S )  e.  ran  L
)
371, 3, 4, 6, 14, 34, 36tglnne 24128 . . . . . 6  |-  ( ph  ->  C  =/=  S )
3837adantr 463 . . . . 5  |-  ( (
ph  /\  R  =  S )  ->  C  =/=  S )
3931, 27eqtrd 2423 . . . . 5  |-  ( (
ph  /\  R  =  S )  ->  M  =  S )
4038, 39neeqtrrd 2682 . . . 4  |-  ( (
ph  /\  R  =  S )  ->  C  =/=  M )
41 simpr 459 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =  t )  ->  R  =  t )
426ad3antrrr 727 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  G  e. TarskiG )
4342adantr 463 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  G  e. TarskiG )
4414ad3antrrr 727 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  C  e.  P )
4544adantr 463 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  C  e.  P )
4620ad3antrrr 727 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  R  e.  P )
4746adantr 463 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  R  e.  P )
4818ad3antrrr 727 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  D  e.  ran  L )
49 simplr 753 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  t  e.  D )
501, 4, 3, 42, 48, 49tglnpt 24056 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  t  e.  P )
5150adantr 463 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  t  e.  P )
5212ad3antrrr 727 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  A  e.  P )
5352adantr 463 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  A  e.  P )
5434ad3antrrr 727 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  S  e.  P )
5554adantr 463 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  S  e.  P )
56 simpllr 758 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  R  =  S )
571, 3, 4, 6, 14, 34, 37tglinerflx2 24134 . . . . . . . . . . . . 13  |-  ( ph  ->  S  e.  ( C L S ) )
5857ad3antrrr 727 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  S  e.  ( C L S ) )
5956, 58eqeltrd 2470 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  R  e.  ( C L S ) )
6059adantr 463 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  R  e.  ( C L S ) )
611, 3, 4, 6, 14, 34, 37tgelrnln 24130 . . . . . . . . . . . . 13  |-  ( ph  ->  ( C L S )  e.  ran  L
)
621, 2, 3, 4, 6, 18, 61, 35perpcom 24210 . . . . . . . . . . . 12  |-  ( ph  ->  ( C L S ) (⟂G `  G
) D )
6362ad4antr 729 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  ( C L S ) (⟂G `  G ) D )
64 simpr 459 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  R  =/=  t )
6548adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  D  e.  ran  L )
6619ad3antrrr 727 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  R  e.  D )
6766adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  R  e.  D )
6849adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  t  e.  D )
691, 3, 4, 43, 47, 51, 64, 64, 65, 67, 68tglinethru 24136 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  D  =  ( R L t ) )
7063, 69breqtrd 4391 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  ( C L S ) (⟂G `  G ) ( R L t ) )
711, 2, 3, 4, 43, 45, 55, 60, 51, 70perprag 24220 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  <" C R t ">  e.  (∟G `  G )
)
721, 3, 4, 6, 12, 20, 23tglinerflx2 24134 . . . . . . . . . . . 12  |-  ( ph  ->  R  e.  ( A L R ) )
7372ad3antrrr 727 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  R  e.  ( A L R ) )
7473adantr 463 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  R  e.  ( A L R ) )
751, 3, 4, 6, 12, 20, 23tgelrnln 24130 . . . . . . . . . . . . 13  |-  ( ph  ->  ( A L R )  e.  ran  L
)
761, 2, 3, 4, 6, 18, 75, 21perpcom 24210 . . . . . . . . . . . 12  |-  ( ph  ->  ( A L R ) (⟂G `  G
) D )
7776ad4antr 729 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  ( A L R ) (⟂G `  G ) D )
7877, 69breqtrd 4391 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  ( A L R ) (⟂G `  G ) ( R L t ) )
791, 2, 3, 4, 43, 53, 47, 74, 51, 78perprag 24220 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  <" A R t ">  e.  (∟G `  G )
)
80 simplr 753 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  t  e.  ( A I C ) )
811, 2, 3, 43, 53, 51, 45, 80tgbtwncom 23999 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  t  e.  ( C I A ) )
821, 2, 3, 4, 5, 43, 45, 47, 51, 53, 71, 79, 81ragflat2 24200 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  /\  R  =/=  t )  ->  R  =  t )
8341, 82pm2.61dane 2700 . . . . . . 7  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  R  =  t )
84 simpr 459 . . . . . . 7  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  t  e.  ( A I C ) )
8583, 84eqeltrd 2470 . . . . . 6  |-  ( ( ( ( ph  /\  R  =  S )  /\  t  e.  D
)  /\  t  e.  ( A I C ) )  ->  R  e.  ( A I C ) )
86 opphllem5.o . . . . . . . . 9  |-  ( ph  ->  A O C )
87 hpg.o . . . . . . . . . 10  |-  O  =  { <. a ,  b
>.  |  ( (
a  e.  ( P 
\  D )  /\  b  e.  ( P  \  D ) )  /\  E. t  e.  D  t  e.  ( a I b ) ) }
881, 2, 3, 87, 12, 14islnopp 24233 . . . . . . . . 9  |-  ( ph  ->  ( A O C  <-> 
( ( -.  A  e.  D  /\  -.  C  e.  D )  /\  E. t  e.  D  t  e.  ( A I C ) ) ) )
8986, 88mpbid 210 . . . . . . . 8  |-  ( ph  ->  ( ( -.  A  e.  D  /\  -.  C  e.  D )  /\  E. t  e.  D  t  e.  ( A I C ) ) )
9089simprd 461 . . . . . . 7  |-  ( ph  ->  E. t  e.  D  t  e.  ( A I C ) )
9190adantr 463 . . . . . 6  |-  ( (
ph  /\  R  =  S )  ->  E. t  e.  D  t  e.  ( A I C ) )
9285, 91r19.29a 2924 . . . . 5  |-  ( (
ph  /\  R  =  S )  ->  R  e.  ( A I C ) )
9331, 92eqeltrd 2470 . . . 4  |-  ( (
ph  /\  R  =  S )  ->  M  e.  ( A I C ) )
941, 2, 3, 4, 5, 7, 8, 9, 11, 13, 15, 17, 32, 40, 93mirbtwnhl 24180 . . 3  |-  ( (
ph  /\  R  =  S )  ->  ( U ( K `  M ) A  <->  ( N `  U ) ( K `
 M ) C ) )
9531fveq2d 5778 . . . 4  |-  ( (
ph  /\  R  =  S )  ->  ( K `  M )  =  ( K `  R ) )
9695breqd 4378 . . 3  |-  ( (
ph  /\  R  =  S )  ->  ( U ( K `  M ) A  <->  U ( K `  R ) A ) )
9739fveq2d 5778 . . . 4  |-  ( (
ph  /\  R  =  S )  ->  ( K `  M )  =  ( K `  S ) )
9897breqd 4378 . . 3  |-  ( (
ph  /\  R  =  S )  ->  (
( N `  U
) ( K `  M ) C  <->  ( N `  U ) ( K `
 S ) C ) )
9994, 96, 983bitr3d 283 . 2  |-  ( (
ph  /\  R  =  S )  ->  ( U ( K `  R ) A  <->  ( N `  U ) ( K `
 S ) C ) )
10018ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  D  e.  ran  L )
1016ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  G  e. TarskiG )
10212ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  A  e.  P
)
10314ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  C  e.  P
)
10419ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  R  e.  D
)
10533ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  S  e.  D
)
10610ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  M  e.  P
)
10786ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  A O C )
10821ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  D (⟂G `  G
) ( A L R ) )
10935ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  D (⟂G `  G
) ( C L S ) )
110 simpr 459 . . . . 5  |-  ( (
ph  /\  R  =/=  S )  ->  R  =/=  S )
111110adantr 463 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  R  =/=  S
)
112 simpr 459 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )
11316ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  U  e.  P
)
11425ad2antrr 723 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  ( N `  R )  =  S )
1151, 2, 3, 87, 4, 100, 101, 9, 8, 102, 103, 104, 105, 106, 107, 108, 109, 111, 112, 113, 114opphllem3 24241 . . 3  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( S  .-  C ) (≤G `  G ) ( R 
.-  A ) )  ->  ( U ( K `  R ) A  <->  ( N `  U ) ( K `
 S ) C ) )
11618ad2antrr 723 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  D  e.  ran  L )
1176adantr 463 . . . . . 6  |-  ( (
ph  /\  R  =/=  S )  ->  G  e. TarskiG )
118117adantr 463 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  G  e. TarskiG )
11914ad2antrr 723 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  C  e.  P
)
12012adantr 463 . . . . . 6  |-  ( (
ph  /\  R  =/=  S )  ->  A  e.  P )
121120adantr 463 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  A  e.  P
)
12233adantr 463 . . . . . 6  |-  ( (
ph  /\  R  =/=  S )  ->  S  e.  D )
123122adantr 463 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  S  e.  D
)
12419adantr 463 . . . . . 6  |-  ( (
ph  /\  R  =/=  S )  ->  R  e.  D )
125124adantr 463 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  R  e.  D
)
12610ad2antrr 723 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  M  e.  P
)
12786ad2antrr 723 . . . . . 6  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  A O C )
1281, 2, 3, 87, 4, 116, 118, 121, 119, 127oppcom 24236 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  C O A )
12935ad2antrr 723 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  D (⟂G `  G
) ( C L S ) )
13021adantr 463 . . . . . 6  |-  ( (
ph  /\  R  =/=  S )  ->  D (⟂G `  G ) ( A L R ) )
131130adantr 463 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  D (⟂G `  G
) ( A L R ) )
132110necomd 2653 . . . . . 6  |-  ( (
ph  /\  R  =/=  S )  ->  S  =/=  R )
133132adantr 463 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  S  =/=  R
)
134 simpr 459 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )
13516ad2antrr 723 . . . . . 6  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  U  e.  P
)
1361, 2, 3, 4, 5, 118, 126, 8, 135mircl 24162 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  ( N `  U )  e.  P
)
13720adantr 463 . . . . . . 7  |-  ( (
ph  /\  R  =/=  S )  ->  R  e.  P )
138137adantr 463 . . . . . 6  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  R  e.  P
)
13925ad2antrr 723 . . . . . 6  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  ( N `  R )  =  S )
1401, 2, 3, 4, 5, 118, 126, 8, 138, 139mircom 24164 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  ( N `  S )  =  R )
1411, 2, 3, 87, 4, 116, 118, 9, 8, 119, 121, 123, 125, 126, 128, 129, 131, 133, 134, 136, 140opphllem3 24241 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  ( ( N `
 U ) ( K `  S ) C  <->  ( N `  ( N `  U ) ) ( K `  R ) A ) )
1421, 2, 3, 4, 5, 118, 126, 8, 135mirmir 24163 . . . . 5  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  ( N `  ( N `  U ) )  =  U )
143142breq1d 4377 . . . 4  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  ( ( N `
 ( N `  U ) ) ( K `  R ) A  <->  U ( K `  R ) A ) )
144141, 143bitr2d 254 . . 3  |-  ( ( ( ph  /\  R  =/=  S )  /\  ( R  .-  A ) (≤G `  G ) ( S 
.-  C ) )  ->  ( U ( K `  R ) A  <->  ( N `  U ) ( K `
 S ) C ) )
145 eqid 2382 . . . . 5  |-  (≤G `  G )  =  (≤G `  G )
1461, 2, 3, 145, 6, 34, 14, 20, 12legtrid 24098 . . . 4  |-  ( ph  ->  ( ( S  .-  C ) (≤G `  G ) ( R 
.-  A )  \/  ( R  .-  A
) (≤G `  G
) ( S  .-  C ) ) )
147146adantr 463 . . 3  |-  ( (
ph  /\  R  =/=  S )  ->  ( ( S  .-  C ) (≤G `  G ) ( R 
.-  A )  \/  ( R  .-  A
) (≤G `  G
) ( S  .-  C ) ) )
148115, 144, 147mpjaodan 784 . 2  |-  ( (
ph  /\  R  =/=  S )  ->  ( U
( K `  R
) A  <->  ( N `  U ) ( K `
 S ) C ) )
14999, 148pm2.61dane 2700 1  |-  ( ph  ->  ( U ( K `
 R ) A  <-> 
( N `  U
) ( K `  S ) C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367    /\ w3a 971    = wceq 1399    e. wcel 1826    =/= wne 2577   E.wrex 2733    \ cdif 3386   class class class wbr 4367   {copab 4424    |-> cmpt 4425   ran crn 4914   ` cfv 5496  (class class class)co 6196   Basecbs 14634   distcds 14711  TarskiGcstrkg 23942  Itvcitv 23949  LineGclng 23950  ≤Gcleg 24089  pInvGcmir 24153  ⟂Gcperpg 24192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-cnex 9459  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479  ax-pre-mulgt0 9480
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-om 6600  df-1st 6699  df-2nd 6700  df-recs 6960  df-rdg 6994  df-1o 7048  df-oadd 7052  df-er 7229  df-map 7340  df-pm 7341  df-en 7436  df-dom 7437  df-sdom 7438  df-fin 7439  df-card 8233  df-cda 8461  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-sub 9720  df-neg 9721  df-nn 10453  df-2 10511  df-3 10512  df-n0 10713  df-z 10782  df-uz 11002  df-fz 11594  df-fzo 11718  df-hash 12308  df-word 12446  df-concat 12448  df-s1 12449  df-s2 12724  df-s3 12725  df-trkgc 23961  df-trkgb 23962  df-trkgcb 23963  df-trkg 23967  df-cgrg 24023  df-leg 24090  df-mir 24154  df-rag 24191  df-perpg 24193
This theorem is referenced by:  opphl  24245
  Copyright terms: Public domain W3C validator