Metamath Proof Explorer

Theorem opphllem6

Description: First part of Lemma 9.4 of Schwabhauser p. 68. (Contributed by Thierry Arnoux, 3-Mar-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 ) )
opphllem5.u 
|- ( ph -> U e. P )
opphllem6.v 
|- ( ph -> ( N ` R ) = S )
Assertion opphllem6 
|- ( ph -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )

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 opphllem5.u 
 |-  ( ph -> U e. P )
19 opphllem6.v 
 |-  ( ph -> ( N ` R ) = S )
20 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
21 7 adantr 
 |-  ( ( ph /\ R = S ) -> G e. TarskiG )
22 14 adantr 
 |-  ( ( ph /\ R = S ) -> M e. P )
23 10 adantr 
 |-  ( ( ph /\ R = S ) -> A e. P )
24 11 adantr 
 |-  ( ( ph /\ R = S ) -> C e. P )
25 18 adantr 
 |-  ( ( ph /\ R = S ) -> U e. P )
26 1 5 3 7 6 12 tglnpt 
 |-  ( ph -> R e. P )
27 5 7 16 perpln2 
 |-  ( ph -> ( A L R ) e. ran L )
28 1 3 5 7 10 26 27 tglnne 
 |-  ( ph -> A =/= R )
29 28 adantr 
 |-  ( ( ph /\ R = S ) -> A =/= R )
30 19 adantr 
 |-  ( ( ph /\ R = S ) -> ( N ` R ) = S )
31 simpr 
 |-  ( ( ph /\ R = S ) -> R = S )
32 30 31 eqtr4d 
 |-  ( ( ph /\ R = S ) -> ( N ` R ) = R )
33 1 2 3 5 20 7 14 9 26 mirinv 
 |-  ( ph -> ( ( N ` R ) = R <-> M = R ) )
34 33 adantr 
 |-  ( ( ph /\ R = S ) -> ( ( N ` R ) = R <-> M = R ) )
35 32 34 mpbid 
 |-  ( ( ph /\ R = S ) -> M = R )
36 29 35 neeqtrrd 
 |-  ( ( ph /\ R = S ) -> A =/= M )
37 1 5 3 7 6 13 tglnpt 
 |-  ( ph -> S e. P )
38 5 7 17 perpln2 
 |-  ( ph -> ( C L S ) e. ran L )
39 1 3 5 7 11 37 38 tglnne 
 |-  ( ph -> C =/= S )
40 39 adantr 
 |-  ( ( ph /\ R = S ) -> C =/= S )
41 35 31 eqtrd 
 |-  ( ( ph /\ R = S ) -> M = S )
42 40 41 neeqtrrd 
 |-  ( ( ph /\ R = S ) -> C =/= M )
43 simpr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R = t ) -> R = t )
44 7 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> G e. TarskiG )
45 11 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> C e. P )
46 26 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R e. P )
47 7 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> G e. TarskiG )
48 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> D e. ran L )
49 simplr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> t e. D )
50 1 5 3 47 48 49 tglnpt 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> t e. P )
51 50 adantr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> t e. P )
52 10 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> A e. P )
53 37 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> S e. P )
54 simpllr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R = S )
55 1 3 5 7 11 37 39 tglinerflx2 
 |-  ( ph -> S e. ( C L S ) )
56 55 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> S e. ( C L S ) )
57 54 56 eqeltrd 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R e. ( C L S ) )
58 57 adantr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R e. ( C L S ) )
59 1 2 3 5 7 6 38 17 perpcom 
 |-  ( ph -> ( C L S ) ( perpG ` G ) D )
60 59 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> ( C L S ) ( perpG ` G ) D )
61 simpr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R =/= t )
62 6 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> D e. ran L )
63 12 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R e. D )
64 simpllr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> t e. D )
65 1 3 5 44 46 51 61 61 62 63 64 tglinethru 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> D = ( R L t ) )
66 60 65 breqtrd 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> ( C L S ) ( perpG ` G ) ( R L t ) )
67 1 2 3 5 44 45 53 58 51 66 perprag 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> <" C R t "> e. ( raG ` G ) )
68 1 3 5 7 10 26 28 tglinerflx2 
 |-  ( ph -> R e. ( A L R ) )
69 68 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R e. ( A L R ) )
70 1 2 3 5 7 6 27 16 perpcom 
 |-  ( ph -> ( A L R ) ( perpG ` G ) D )
71 70 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> ( A L R ) ( perpG ` G ) D )
72 71 65 breqtrd 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> ( A L R ) ( perpG ` G ) ( R L t ) )
73 1 2 3 5 44 52 46 69 51 72 perprag 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> <" A R t "> e. ( raG ` G ) )
74 simplr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> t e. ( A I C ) )
75 1 2 3 44 52 51 45 74 tgbtwncom 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> t e. ( C I A ) )
76 1 2 3 5 20 44 45 46 51 52 67 73 75 ragflat2 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R = t )
77 43 76 pm2.61dane 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R = t )
78 simpr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> t e. ( A I C ) )
79 77 78 eqeltrd 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R e. ( A I C ) )
80 1 2 3 4 10 11 islnopp 
 |-  ( ph -> ( A O C <-> ( ( -. A e. D /\ -. C e. D ) /\ E. t e. D t e. ( A I C ) ) ) )
81 15 80 mpbid 
 |-  ( ph -> ( ( -. A e. D /\ -. C e. D ) /\ E. t e. D t e. ( A I C ) ) )
82 81 simprd 
 |-  ( ph -> E. t e. D t e. ( A I C ) )
83 82 adantr 
 |-  ( ( ph /\ R = S ) -> E. t e. D t e. ( A I C ) )
84 79 83 r19.29a 
 |-  ( ( ph /\ R = S ) -> R e. ( A I C ) )
85 35 84 eqeltrd 
 |-  ( ( ph /\ R = S ) -> M e. ( A I C ) )
86 1 2 3 5 20 21 9 8 22 23 24 25 36 42 85 mirbtwnhl 
 |-  ( ( ph /\ R = S ) -> ( U ( K ` M ) A <-> ( N ` U ) ( K ` M ) C ) )
87 35 fveq2d 
 |-  ( ( ph /\ R = S ) -> ( K ` M ) = ( K ` R ) )
88 87 breqd 
 |-  ( ( ph /\ R = S ) -> ( U ( K ` M ) A <-> U ( K ` R ) A ) )
89 41 fveq2d 
 |-  ( ( ph /\ R = S ) -> ( K ` M ) = ( K ` S ) )
90 89 breqd 
 |-  ( ( ph /\ R = S ) -> ( ( N ` U ) ( K ` M ) C <-> ( N ` U ) ( K ` S ) C ) )
91 86 88 90 3bitr3d 
 |-  ( ( ph /\ R = S ) -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )
92 6 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> D e. ran L )
93 7 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> G e. TarskiG )
94 10 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> A e. P )
95 11 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> C e. P )
96 12 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> R e. D )
97 13 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> S e. D )
98 14 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> M e. P )
99 15 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> A O C )
100 16 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> D ( perpG ` G ) ( A L R ) )
101 17 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> D ( perpG ` G ) ( C L S ) )
102 simplr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> R =/= S )
103 simpr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> ( S .- C ) ( leG ` G ) ( R .- A ) )
104 18 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> U e. P )
105 19 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> ( N ` R ) = S )
106 1 2 3 4 5 92 93 8 9 94 95 96 97 98 99 100 101 102 103 104 105 opphllem3 
 |-  ( ( ( ph /\ R =/= S ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )
107 6 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> D e. ran L )
108 7 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> G e. TarskiG )
109 11 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> C e. P )
110 10 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> A e. P )
111 13 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> S e. D )
112 12 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> R e. D )
113 14 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> M e. P )
114 15 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> A O C )
115 1 2 3 4 5 107 108 110 109 114 oppcom 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> C O A )
116 17 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> D ( perpG ` G ) ( C L S ) )
117 16 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> D ( perpG ` G ) ( A L R ) )
118 simpr 
 |-  ( ( ph /\ R =/= S ) -> R =/= S )
119 118 necomd 
 |-  ( ( ph /\ R =/= S ) -> S =/= R )
120 119 adantr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> S =/= R )
121 simpr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( R .- A ) ( leG ` G ) ( S .- C ) )
122 18 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> U e. P )
123 1 2 3 5 20 108 113 9 122 mircl 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( N ` U ) e. P )
124 26 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> R e. P )
125 19 ad2antrr 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( N ` R ) = S )
126 1 2 3 5 20 108 113 9 124 125 mircom 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( N ` S ) = R )
127 1 2 3 4 5 107 108 8 9 109 110 111 112 113 115 116 117 120 121 123 126 opphllem3 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( ( N ` U ) ( K ` S ) C <-> ( N ` ( N ` U ) ) ( K ` R ) A ) )
128 1 2 3 5 20 108 113 9 122 mirmir 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( N ` ( N ` U ) ) = U )
129 128 breq1d 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( ( N ` ( N ` U ) ) ( K ` R ) A <-> U ( K ` R ) A ) )
130 127 129 bitr2d 
 |-  ( ( ( ph /\ R =/= S ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )
131 eqid 
 |-  ( leG ` G ) = ( leG ` G )
132 1 2 3 131 7 37 11 26 10 legtrid 
 |-  ( ph -> ( ( S .- C ) ( leG ` G ) ( R .- A ) \/ ( R .- A ) ( leG ` G ) ( S .- C ) ) )
133 132 adantr 
 |-  ( ( ph /\ R =/= S ) -> ( ( S .- C ) ( leG ` G ) ( R .- A ) \/ ( R .- A ) ( leG ` G ) ( S .- C ) ) )
134 106 130 133 mpjaodan 
 |-  ( ( ph /\ R =/= S ) -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )
135 91 134 pm2.61dane 
 |-  ( ph -> ( U ( K ` R ) A <-> ( N ` U ) ( K ` S ) C ) )