Metamath Proof Explorer

Theorem opphllem5

Description: Second part of Lemma 9.4 of Schwabhauser p. 68. (Contributed by Thierry Arnoux, 2-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 )
opphllem5.v 
|- ( ph -> V e. P )
opphllem5.1 
|- ( ph -> U ( K ` R ) A )
opphllem5.2 
|- ( ph -> V ( K ` S ) C )
Assertion opphllem5 
|- ( 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 opphllem5.u 
 |-  ( ph -> U e. P )
19 opphllem5.v 
 |-  ( ph -> V e. P )
20 opphllem5.1 
 |-  ( ph -> U ( K ` R ) A )
21 opphllem5.2 
 |-  ( ph -> V ( K ` S ) C )
22 1 5 3 7 6 12 tglnpt 
 |-  ( ph -> R e. P )
23 1 3 8 18 10 22 7 20 hlne2 
 |-  ( ph -> A =/= R )
24 1 3 5 7 10 22 23 tglinecom 
 |-  ( ph -> ( A L R ) = ( R L A ) )
25 16 24 breqtrd 
 |-  ( ph -> D ( perpG ` G ) ( R L A ) )
26 1 3 8 18 10 22 7 20 hlcomd 
 |-  ( ph -> A ( K ` R ) U )
27 1 2 3 5 7 6 8 12 10 18 25 26 hlperpnel 
 |-  ( ph -> -. U e. D )
28 27 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> -. U e. D )
29 1 5 3 7 6 13 tglnpt 
 |-  ( ph -> S e. P )
30 1 3 8 19 11 29 7 21 hlne2 
 |-  ( ph -> C =/= S )
31 1 3 5 7 11 29 30 tglinecom 
 |-  ( ph -> ( C L S ) = ( S L C ) )
32 17 31 breqtrd 
 |-  ( ph -> D ( perpG ` G ) ( S L C ) )
33 1 3 8 19 11 29 7 21 hlcomd 
 |-  ( ph -> C ( K ` S ) V )
34 1 2 3 5 7 6 8 13 11 19 32 33 hlperpnel 
 |-  ( ph -> -. V e. D )
35 34 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> -. V e. D )
36 simplr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> t e. D )
37 simpr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R = t ) -> R = t )
38 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
39 7 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> G e. TarskiG )
40 11 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> C e. P )
41 22 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R e. P )
42 7 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> G e. TarskiG )
43 6 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> D e. ran L )
44 1 5 3 42 43 36 tglnpt 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> t e. P )
45 44 adantr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> t e. P )
46 10 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> A e. P )
47 29 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> S e. P )
48 simpllr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R = S )
49 1 3 5 7 11 29 30 tglinerflx2 
 |-  ( ph -> S e. ( C L S ) )
50 49 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> S e. ( C L S ) )
51 48 50 eqeltrd 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R e. ( C L S ) )
52 51 adantr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R e. ( C L S ) )
53 5 7 17 perpln2 
 |-  ( ph -> ( C L S ) e. ran L )
54 1 2 3 5 7 6 53 17 perpcom 
 |-  ( ph -> ( C L S ) ( perpG ` G ) D )
55 54 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> ( C L S ) ( perpG ` G ) D )
56 simpr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R =/= t )
57 6 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> D e. ran L )
58 12 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R e. D )
59 simpllr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> t e. D )
60 1 3 5 39 41 45 56 56 57 58 59 tglinethru 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> D = ( R L t ) )
61 55 60 breqtrd 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> ( C L S ) ( perpG ` G ) ( R L t ) )
62 1 2 3 5 39 40 47 52 45 61 perprag 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> <" C R t "> e. ( raG ` G ) )
63 1 3 5 7 10 22 23 tglinerflx2 
 |-  ( ph -> R e. ( A L R ) )
64 63 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R e. ( A L R ) )
65 5 7 16 perpln2 
 |-  ( ph -> ( A L R ) e. ran L )
66 1 2 3 5 7 6 65 16 perpcom 
 |-  ( ph -> ( A L R ) ( perpG ` G ) D )
67 66 ad4antr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> ( A L R ) ( perpG ` G ) D )
68 67 60 breqtrd 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> ( A L R ) ( perpG ` G ) ( R L t ) )
69 1 2 3 5 39 46 41 64 45 68 perprag 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> <" A R t "> e. ( raG ` G ) )
70 simplr 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> t e. ( A I C ) )
71 1 2 3 39 46 45 40 70 tgbtwncom 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> t e. ( C I A ) )
72 1 2 3 5 38 39 40 41 45 46 62 69 71 ragflat2 
 |-  ( ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) /\ R =/= t ) -> R = t )
73 37 72 pm2.61dane 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R = t )
74 10 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> A e. P )
75 18 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> U e. P )
76 19 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> V e. P )
77 22 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R e. P )
78 26 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> A ( K ` R ) U )
79 11 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> C e. P )
80 21 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> V ( K ` S ) C )
81 48 fveq2d 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> ( K ` R ) = ( K ` S ) )
82 81 breqd 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> ( V ( K ` R ) C <-> V ( K ` S ) C ) )
83 80 82 mpbird 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> V ( K ` R ) C )
84 1 3 8 76 79 77 42 83 hlcomd 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> C ( K ` R ) V )
85 simpr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> t e. ( A I C ) )
86 73 85 eqeltrd 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R e. ( A I C ) )
87 1 2 3 42 74 77 79 86 tgbtwncom 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R e. ( C I A ) )
88 1 3 8 79 76 74 42 77 84 87 btwnhl 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R e. ( V I A ) )
89 1 2 3 42 76 77 74 88 tgbtwncom 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R e. ( A I V ) )
90 1 3 8 74 75 76 42 77 78 89 btwnhl 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> R e. ( U I V ) )
91 73 90 eqeltrrd 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> t e. ( U I V ) )
92 rspe 
 |-  ( ( t e. D /\ t e. ( U I V ) ) -> E. t e. D t e. ( U I V ) )
93 36 91 92 syl2anc 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> E. t e. D t e. ( U I V ) )
94 28 35 93 jca31 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> ( ( -. U e. D /\ -. V e. D ) /\ E. t e. D t e. ( U I V ) ) )
95 1 2 3 4 18 19 islnopp 
 |-  ( ph -> ( U O V <-> ( ( -. U e. D /\ -. V e. D ) /\ E. t e. D t e. ( U I V ) ) ) )
96 95 ad3antrrr 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> ( U O V <-> ( ( -. U e. D /\ -. V e. D ) /\ E. t e. D t e. ( U I V ) ) ) )
97 94 96 mpbird 
 |-  ( ( ( ( ph /\ R = S ) /\ t e. D ) /\ t e. ( A I C ) ) -> U O V )
98 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 ) ) ) )
99 15 98 mpbid 
 |-  ( ph -> ( ( -. A e. D /\ -. C e. D ) /\ E. t e. D t e. ( A I C ) ) )
100 99 simprd 
 |-  ( ph -> E. t e. D t e. ( A I C ) )
101 100 adantr 
 |-  ( ( ph /\ R = S ) -> E. t e. D t e. ( A I C ) )
102 97 101 r19.29a 
 |-  ( ( ph /\ R = S ) -> U O V )
103 6 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> D e. ran L )
104 7 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> G e. TarskiG )
105 eqid 
 |-  ( ( pInvG ` G ) ` m ) = ( ( pInvG ` G ) ` m )
106 10 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> A e. P )
107 11 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> C e. P )
108 12 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> R e. D )
109 13 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> S e. D )
110 simpllr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> m e. P )
111 15 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> A O C )
112 16 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> D ( perpG ` G ) ( A L R ) )
113 17 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> D ( perpG ` G ) ( C L S ) )
114 simpr 
 |-  ( ( ph /\ R =/= S ) -> R =/= S )
115 114 ad3antrrr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> R =/= S )
116 simpr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> ( S .- C ) ( leG ` G ) ( R .- A ) )
117 18 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> U e. P )
118 simplr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> S = ( ( ( pInvG ` G ) ` m ) ` R ) )
119 118 eqcomd 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> ( ( ( pInvG ` G ) ` m ) ` R ) = S )
120 19 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> V e. P )
121 20 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> U ( K ` R ) A )
122 21 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> V ( K ` S ) C )
123 1 2 3 4 5 103 104 8 105 106 107 108 109 110 111 112 113 115 116 117 119 120 121 122 opphllem4 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( S .- C ) ( leG ` G ) ( R .- A ) ) -> U O V )
124 6 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> D e. ran L )
125 7 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> G e. TarskiG )
126 19 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> V e. P )
127 18 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> U e. P )
128 11 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> C e. P )
129 10 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> A e. P )
130 13 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> S e. D )
131 12 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> R e. D )
132 simpllr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> m e. P )
133 15 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> A O C )
134 1 2 3 4 5 124 125 129 128 133 oppcom 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> C O A )
135 17 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> D ( perpG ` G ) ( C L S ) )
136 16 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> D ( perpG ` G ) ( A L R ) )
137 114 necomd 
 |-  ( ( ph /\ R =/= S ) -> S =/= R )
138 137 ad3antrrr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> S =/= R )
139 simpr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( R .- A ) ( leG ` G ) ( S .- C ) )
140 22 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> R e. P )
141 simplr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> S = ( ( ( pInvG ` G ) ` m ) ` R ) )
142 141 eqcomd 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( ( ( pInvG ` G ) ` m ) ` R ) = S )
143 1 2 3 5 38 125 132 105 140 142 mircom 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> ( ( ( pInvG ` G ) ` m ) ` S ) = R )
144 21 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> V ( K ` S ) C )
145 20 ad4antr 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> U ( K ` R ) A )
146 1 2 3 4 5 124 125 8 105 128 129 130 131 132 134 135 136 138 139 126 143 127 144 145 opphllem4 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> V O U )
147 1 2 3 4 5 124 125 126 127 146 oppcom 
 |-  ( ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) /\ ( R .- A ) ( leG ` G ) ( S .- C ) ) -> U O V )
148 eqid 
 |-  ( leG ` G ) = ( leG ` G )
149 1 2 3 148 7 29 11 22 10 legtrid 
 |-  ( ph -> ( ( S .- C ) ( leG ` G ) ( R .- A ) \/ ( R .- A ) ( leG ` G ) ( S .- C ) ) )
150 149 ad3antrrr 
 |-  ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) -> ( ( S .- C ) ( leG ` G ) ( R .- A ) \/ ( R .- A ) ( leG ` G ) ( S .- C ) ) )
151 123 147 150 mpjaodan 
 |-  ( ( ( ( ph /\ R =/= S ) /\ m e. P ) /\ S = ( ( ( pInvG ` G ) ` m ) ` R ) ) -> U O V )
152 7 adantr 
 |-  ( ( ph /\ R =/= S ) -> G e. TarskiG )
153 22 adantr 
 |-  ( ( ph /\ R =/= S ) -> R e. P )
154 29 adantr 
 |-  ( ( ph /\ R =/= S ) -> S e. P )
155 1 2 3 4 5 6 7 10 11 15 opptgdim2 
 |-  ( ph -> G TarskiGDim>= 2 )
156 155 adantr 
 |-  ( ( ph /\ R =/= S ) -> G TarskiGDim>= 2 )
157 1 2 3 5 152 38 153 154 156 midex 
 |-  ( ( ph /\ R =/= S ) -> E. m e. P S = ( ( ( pInvG ` G ) ` m ) ` R ) )
158 151 157 r19.29a 
 |-  ( ( ph /\ R =/= S ) -> U O V )
159 102 158 pm2.61dane 
 |-  ( ph -> U O V )