Metamath Proof Explorer

Theorem opphllem4

Description: Lemma for opphl . (Contributed by Thierry Arnoux, 22-Feb-2020)

Ref Expression
Hypotheses 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 = ( hlG ` G )
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 ( perpG ` G ) ( A L R ) )
opphllem5.q 
|- ( ph -> D ( perpG ` G ) ( C L S ) )
opphllem3.t 
|- ( ph -> R =/= S )
opphllem3.l 
|- ( ph -> ( S .- C ) ( leG ` G ) ( R .- A ) )
opphllem3.u 
|- ( ph -> U e. P )
opphllem3.v 
|- ( ph -> ( N ` R ) = S )
opphllem4.u 
|- ( ph -> V e. P )
opphllem4.1 
|- ( ph -> U ( K ` R ) A )
opphllem4.2 
|- ( ph -> V ( K ` S ) C )
Assertion opphllem4 
|- ( ph -> U O V )

Proof

Step Hyp Ref Expression
1 hpg.p 
 |-  P = ( Base ` G )
2 hpg.d 
 |-  .- = ( dist ` G )
3 hpg.i 
 |-  I = ( Itv ` G )
4 hpg.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
5 opphl.l 
 |-  L = ( LineG ` G )
6 opphl.d 
 |-  ( ph -> D e. ran L )
7 opphl.g 
 |-  ( ph -> G e. TarskiG )
8 opphl.k 
 |-  K = ( hlG ` G )
9 opphllem5.n 
 |-  N = ( ( pInvG ` G ) ` M )
10 opphllem5.a 
 |-  ( ph -> A e. P )
11 opphllem5.c 
 |-  ( ph -> C e. P )
12 opphllem5.r 
 |-  ( ph -> R e. D )
13 opphllem5.s 
 |-  ( ph -> S e. D )
14 opphllem5.m 
 |-  ( ph -> M e. P )
15 opphllem5.o 
 |-  ( ph -> A O C )
16 opphllem5.p 
 |-  ( ph -> D ( perpG ` G ) ( A L R ) )
17 opphllem5.q 
 |-  ( ph -> D ( perpG ` G ) ( C L S ) )
18 opphllem3.t 
 |-  ( ph -> R =/= S )
19 opphllem3.l 
 |-  ( ph -> ( S .- C ) ( leG ` G ) ( R .- A ) )
20 opphllem3.u 
 |-  ( ph -> U e. P )
21 opphllem3.v 
 |-  ( ph -> ( N ` R ) = S )
22 opphllem4.u 
 |-  ( ph -> V e. P )
23 opphllem4.1 
 |-  ( ph -> U ( K ` R ) A )
24 opphllem4.2 
 |-  ( ph -> V ( K ` S ) C )
25 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
26 1 2 3 5 25 7 14 9 20 mircl 
 |-  ( ph -> ( N ` U ) e. P )
27 1 5 3 7 6 13 tglnpt 
 |-  ( ph -> S e. P )
28 1 5 3 7 6 12 tglnpt 
 |-  ( ph -> R e. P )
29 18 necomd 
 |-  ( ph -> S =/= R )
30 1 2 3 5 25 7 14 9 28 mirbtwn 
 |-  ( ph -> M e. ( ( N ` R ) I R ) )
31 21 oveq1d 
 |-  ( ph -> ( ( N ` R ) I R ) = ( S I R ) )
32 30 31 eleqtrd 
 |-  ( ph -> M e. ( S I R ) )
33 1 3 5 7 27 28 14 29 32 btwnlng1 
 |-  ( ph -> M e. ( S L R ) )
34 1 3 5 7 27 28 29 29 6 13 12 tglinethru 
 |-  ( ph -> D = ( S L R ) )
35 33 34 eleqtrrd 
 |-  ( ph -> M e. D )
36 1 2 3 4 5 6 7 10 11 15 oppne1 
 |-  ( ph -> -. A e. D )
37 1 3 8 20 10 28 7 23 hlne1 
 |-  ( ph -> U =/= R )
38 37 necomd 
 |-  ( ph -> R =/= U )
39 1 3 8 20 10 28 7 5 23 hlln 
 |-  ( ph -> U e. ( A L R ) )
40 1 3 8 20 10 28 7 23 hlne2 
 |-  ( ph -> A =/= R )
41 1 3 5 7 28 20 10 38 39 40 lnrot1 
 |-  ( ph -> A e. ( R L U ) )
42 41 adantr 
 |-  ( ( ph /\ U e. D ) -> A e. ( R L U ) )
43 7 adantr 
 |-  ( ( ph /\ U e. D ) -> G e. TarskiG )
44 28 adantr 
 |-  ( ( ph /\ U e. D ) -> R e. P )
45 20 adantr 
 |-  ( ( ph /\ U e. D ) -> U e. P )
46 38 adantr 
 |-  ( ( ph /\ U e. D ) -> R =/= U )
47 6 adantr 
 |-  ( ( ph /\ U e. D ) -> D e. ran L )
48 12 adantr 
 |-  ( ( ph /\ U e. D ) -> R e. D )
49 simpr 
 |-  ( ( ph /\ U e. D ) -> U e. D )
50 1 3 5 43 44 45 46 46 47 48 49 tglinethru 
 |-  ( ( ph /\ U e. D ) -> D = ( R L U ) )
51 42 50 eleqtrrd 
 |-  ( ( ph /\ U e. D ) -> A e. D )
52 36 51 mtand 
 |-  ( ph -> -. U e. D )
53 7 adantr 
 |-  ( ( ph /\ ( N ` U ) e. D ) -> G e. TarskiG )
54 14 adantr 
 |-  ( ( ph /\ ( N ` U ) e. D ) -> M e. P )
55 20 adantr 
 |-  ( ( ph /\ ( N ` U ) e. D ) -> U e. P )
56 1 2 3 5 25 53 54 9 55 mirmir 
 |-  ( ( ph /\ ( N ` U ) e. D ) -> ( N ` ( N ` U ) ) = U )
57 6 adantr 
 |-  ( ( ph /\ ( N ` U ) e. D ) -> D e. ran L )
58 35 adantr 
 |-  ( ( ph /\ ( N ` U ) e. D ) -> M e. D )
59 simpr 
 |-  ( ( ph /\ ( N ` U ) e. D ) -> ( N ` U ) e. D )
60 1 2 3 5 25 53 9 57 58 59 mirln 
 |-  ( ( ph /\ ( N ` U ) e. D ) -> ( N ` ( N ` U ) ) e. D )
61 56 60 eqeltrrd 
 |-  ( ( ph /\ ( N ` U ) e. D ) -> U e. D )
62 52 61 mtand 
 |-  ( ph -> -. ( N ` U ) e. D )
63 1 2 3 5 25 7 14 9 20 mirbtwn 
 |-  ( ph -> M e. ( ( N ` U ) I U ) )
64 1 2 3 4 26 20 35 62 52 63 islnoppd 
 |-  ( ph -> ( N ` U ) O U )
65 eqidd 
 |-  ( ph -> ( N ` U ) = ( N ` U ) )
66 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 opphllem3 
 |-  ( ph -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )
67 23 66 mpbid 
 |-  ( ph -> ( N ` U ) ( K ` S ) C )
68 1 3 8 22 11 27 7 24 hlcomd 
 |-  ( ph -> C ( K ` S ) V )
69 1 3 8 26 11 22 7 27 67 68 hltr 
 |-  ( ph -> ( N ` U ) ( K ` S ) V )
70 1 3 8 26 22 27 7 ishlg 
 |-  ( ph -> ( ( N ` U ) ( K ` S ) V <-> ( ( N ` U ) =/= S /\ V =/= S /\ ( ( N ` U ) e. ( S I V ) \/ V e. ( S I ( N ` U ) ) ) ) ) )
71 69 70 mpbid 
 |-  ( ph -> ( ( N ` U ) =/= S /\ V =/= S /\ ( ( N ` U ) e. ( S I V ) \/ V e. ( S I ( N ` U ) ) ) ) )
72 71 simp1d 
 |-  ( ph -> ( N ` U ) =/= S )
73 1 3 8 11 22 27 7 68 hlne2 
 |-  ( ph -> V =/= S )
74 71 simp3d 
 |-  ( ph -> ( ( N ` U ) e. ( S I V ) \/ V e. ( S I ( N ` U ) ) ) )
75 1 2 3 4 5 6 7 9 26 22 20 13 64 35 65 72 73 74 opphllem2 
 |-  ( ph -> V O U )
76 1 2 3 4 5 6 7 22 20 75 oppcom 
 |-  ( ph -> U O V )