Metamath Proof Explorer

Theorem opphllem

Description: Lemma 8.24 of Schwabhauser p. 66. This is used later for mideulem and later for opphl . (Contributed by Thierry Arnoux, 21-Dec-2019)

Ref Expression
Hypotheses 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 ) ( perpG ` G ) ( Q L B ) )
mideulem.6 
|- ( ph -> ( A L B ) ( perpG ` G ) ( A L O ) )
mideulem.7 
|- ( ph -> T e. ( A L B ) )
mideulem.8 
|- ( ph -> T e. ( Q I O ) )
opphllem.1 
|- ( ph -> R e. P )
opphllem.2 
|- ( ph -> R e. ( B I Q ) )
opphllem.3 
|- ( ph -> ( A .- O ) = ( B .- R ) )
Assertion opphllem 
|- ( ph -> E. x e. P ( B = ( ( S ` x ) ` A ) /\ O = ( ( S ` x ) ` R ) ) )

Proof

Step Hyp Ref Expression
1 colperpex.p 
 |-  P = ( Base ` G )
2 colperpex.d 
 |-  .- = ( dist ` G )
3 colperpex.i 
 |-  I = ( Itv ` G )
4 colperpex.l 
 |-  L = ( LineG ` G )
5 colperpex.g 
 |-  ( ph -> G e. TarskiG )
6 mideu.s 
 |-  S = ( pInvG ` G )
7 mideu.1 
 |-  ( ph -> A e. P )
8 mideu.2 
 |-  ( ph -> B e. P )
9 mideulem.1 
 |-  ( ph -> A =/= B )
10 mideulem.2 
 |-  ( ph -> Q e. P )
11 mideulem.3 
 |-  ( ph -> O e. P )
12 mideulem.4 
 |-  ( ph -> T e. P )
13 mideulem.5 
 |-  ( ph -> ( A L B ) ( perpG ` G ) ( Q L B ) )
14 mideulem.6 
 |-  ( ph -> ( A L B ) ( perpG ` G ) ( A L O ) )
15 mideulem.7 
 |-  ( ph -> T e. ( A L B ) )
16 mideulem.8 
 |-  ( ph -> T e. ( Q I O ) )
17 opphllem.1 
 |-  ( ph -> R e. P )
18 opphllem.2 
 |-  ( ph -> R e. ( B I Q ) )
19 opphllem.3 
 |-  ( ph -> ( A .- O ) = ( B .- R ) )
20 5 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> G e. TarskiG )
21 eqid 
 |-  ( S ` x ) = ( S ` x )
22 8 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> B e. P )
23 11 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> O e. P )
24 7 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> A e. P )
25 17 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> R e. P )
26 simprl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> x e. P )
27 9 necomd 
 |-  ( ph -> B =/= A )
28 27 neneqd 
 |-  ( ph -> -. B = A )
29 28 adantr 
 |-  ( ( ph /\ O e. ( B L A ) ) -> -. B = A )
30 4 5 14 perpln2 
 |-  ( ph -> ( A L O ) e. ran L )
31 1 3 4 5 7 11 30 tglnne 
 |-  ( ph -> A =/= O )
32 31 necomd 
 |-  ( ph -> O =/= A )
33 32 neneqd 
 |-  ( ph -> -. O = A )
34 33 adantr 
 |-  ( ( ph /\ O e. ( B L A ) ) -> -. O = A )
35 29 34 jca 
 |-  ( ( ph /\ O e. ( B L A ) ) -> ( -. B = A /\ -. O = A ) )
36 5 adantr 
 |-  ( ( ph /\ O e. ( B L A ) ) -> G e. TarskiG )
37 8 adantr 
 |-  ( ( ph /\ O e. ( B L A ) ) -> B e. P )
38 7 adantr 
 |-  ( ( ph /\ O e. ( B L A ) ) -> A e. P )
39 11 adantr 
 |-  ( ( ph /\ O e. ( B L A ) ) -> O e. P )
40 1 3 4 5 8 7 27 tglinerflx2 
 |-  ( ph -> A e. ( B L A ) )
41 1 3 4 5 7 8 9 tglinecom 
 |-  ( ph -> ( A L B ) = ( B L A ) )
42 41 14 eqbrtrrd 
 |-  ( ph -> ( B L A ) ( perpG ` G ) ( A L O ) )
43 1 2 3 4 5 8 7 40 11 42 perprag 
 |-  ( ph -> <" B A O "> e. ( raG ` G ) )
44 43 adantr 
 |-  ( ( ph /\ O e. ( B L A ) ) -> <" B A O "> e. ( raG ` G ) )
45 simpr 
 |-  ( ( ph /\ O e. ( B L A ) ) -> O e. ( B L A ) )
46 45 orcd 
 |-  ( ( ph /\ O e. ( B L A ) ) -> ( O e. ( B L A ) \/ B = A ) )
47 1 2 3 4 6 36 37 38 39 44 46 ragflat3 
 |-  ( ( ph /\ O e. ( B L A ) ) -> ( B = A \/ O = A ) )
48 oran 
 |-  ( ( B = A \/ O = A ) <-> -. ( -. B = A /\ -. O = A ) )
49 47 48 sylib 
 |-  ( ( ph /\ O e. ( B L A ) ) -> -. ( -. B = A /\ -. O = A ) )
50 35 49 pm2.65da 
 |-  ( ph -> -. O e. ( B L A ) )
51 50 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> -. O e. ( B L A ) )
52 41 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( A L B ) = ( B L A ) )
53 51 52 neleqtrrd 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> -. O e. ( A L B ) )
54 9 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> A =/= B )
55 54 neneqd 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> -. A = B )
56 53 55 jca 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( -. O e. ( A L B ) /\ -. A = B ) )
57 pm4.56 
 |-  ( ( -. O e. ( A L B ) /\ -. A = B ) <-> -. ( O e. ( A L B ) \/ A = B ) )
58 56 57 sylib 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> -. ( O e. ( A L B ) \/ A = B ) )
59 1 4 3 20 24 22 23 58 ncolrot2 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> -. ( B e. ( O L A ) \/ O = A ) )
60 simprrr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> x e. ( R I O ) )
61 1 2 3 20 25 26 23 60 tgbtwncom 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> x e. ( O I R ) )
62 12 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> T e. P )
63 15 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> T e. ( A L B ) )
64 simprrl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> x e. ( T I B ) )
65 1 3 4 20 62 24 22 26 63 64 coltr3 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> x e. ( A L B ) )
66 50 41 neleqtrrd 
 |-  ( ph -> -. O e. ( A L B ) )
67 66 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> -. O e. ( A L B ) )
68 nelne2 
 |-  ( ( x e. ( A L B ) /\ -. O e. ( A L B ) ) -> x =/= O )
69 65 67 68 syl2anc 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> x =/= O )
70 1 2 3 20 23 26 25 61 69 tgbtwnne 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> O =/= R )
71 1 2 3 4 6 5 8 7 11 israg 
 |-  ( ph -> ( <" B A O "> e. ( raG ` G ) <-> ( B .- O ) = ( B .- ( ( S ` A ) ` O ) ) ) )
72 43 71 mpbid 
 |-  ( ph -> ( B .- O ) = ( B .- ( ( S ` A ) ` O ) ) )
73 72 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 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 ) ) )
74 5 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 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 )
75 eqid 
 |-  ( S ` A ) = ( S ` A )
76 1 2 3 4 6 20 24 75 23 mircl 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( ( S ` A ) ` O ) e. P )
77 76 ad2antrr 
 |-  ( ( ( ( ph /\ ( 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 )
78 7 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 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 )
79 11 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 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 )
80 17 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 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 )
81 8 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 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 )
82 simplr 
 |-  ( ( ( ( ph /\ ( 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 )
83 1 2 3 4 6 74 78 75 79 mirbtwn 
 |-  ( ( ( ( ph /\ ( 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 ) )
84 eqid 
 |-  ( S ` B ) = ( S ` B )
85 1 2 3 4 6 74 81 84 82 mirbtwn 
 |-  ( ( ( ( ph /\ ( 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 ) )
86 simpr 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) )
87 74 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( 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 )
88 78 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( 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 )
89 81 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( 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 )
90 54 ad4antr 
 |-  ( ( ( ( ( ( ph /\ ( 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 )
91 10 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) ) -> Q e. P )
92 79 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( 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 )
93 62 ad4antr 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) ) -> T e. P )
94 13 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) ( perpG ` G ) ( Q L B ) )
95 14 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) ( perpG ` G ) ( A L O ) )
96 63 ad4antr 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) ) -> T e. ( A L B ) )
97 16 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) ) -> T e. ( Q I O ) )
98 80 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( 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 )
99 18 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( 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. ( B I Q ) )
100 19 ad5antr 
 |-  ( ( ( ( ( ( ph /\ ( 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 .- O ) = ( B .- R ) )
101 26 ad2antrr 
 |-  ( ( ( ( ph /\ ( 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 )
102 101 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( 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 )
103 simp-5r 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) ) ) )
104 103 simprd 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) ) )
105 104 simpld 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) )
106 104 simprd 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) )
107 82 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( 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 )
108 simpllr 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) ) )
109 108 simpld 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) )
110 simprr 
 |-  ( ( ( ( ph /\ ( 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 ) )
111 110 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) )
112 simplr 
 |-  ( ( ( ( ( ( ph /\ ( 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 )
113 1 2 3 4 87 6 88 89 90 91 92 93 94 95 96 97 98 99 100 102 105 106 107 109 111 112 86 mideulem2 
 |-  ( ( ( ( ( ( ph /\ ( 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 = m )
114 113 eqcomd 
 |-  ( ( ( ( ( ( ph /\ ( 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 = B )
115 114 fveq2d 
 |-  ( ( ( ( ( ( ph /\ ( 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 ` B ) )
116 115 fveq1d 
 |-  ( ( ( ( ( ( ph /\ ( 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 ) = ( ( S ` B ) ` s ) )
117 86 116 eqtrd 
 |-  ( ( ( ( ( ( ph /\ ( 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 ` B ) ` s ) )
118 eqid 
 |-  ( S ` m ) = ( S ` m )
119 1 2 3 4 6 74 118 82 80 101 110 midexlem 
 |-  ( ( ( ( ph /\ ( 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 ) ) ) -> E. m e. P R = ( ( S ` m ) ` s ) )
120 117 119 r19.29a 
 |-  ( ( ( ( ph /\ ( 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 = ( ( S ` B ) ` s ) )
121 120 oveq1d 
 |-  ( ( ( ( ph /\ ( 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 I s ) = ( ( ( S ` B ) ` s ) I s ) )
122 85 121 eleqtrrd 
 |-  ( ( ( ( ph /\ ( 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. ( R I s ) )
123 1 2 3 4 6 74 78 75 79 mircgr 
 |-  ( ( ( ( ph /\ ( 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 .- ( ( S ` A ) ` O ) ) = ( A .- O ) )
124 19 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 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 .- O ) = ( B .- R ) )
125 123 124 eqtrd 
 |-  ( ( ( ( ph /\ ( 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 .- ( ( S ` A ) ` O ) ) = ( B .- R ) )
126 1 2 3 74 78 77 81 80 125 tgcgrcomlr 
 |-  ( ( ( ( ph /\ ( 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 ) .- A ) = ( R .- B ) )
127 120 oveq2d 
 |-  ( ( ( ( ph /\ ( 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 .- R ) = ( B .- ( ( S ` B ) ` s ) ) )
128 1 2 3 4 6 74 81 84 82 mircgr 
 |-  ( ( ( ( ph /\ ( 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 .- ( ( S ` B ) ` s ) ) = ( B .- s ) )
129 124 127 128 3eqtrd 
 |-  ( ( ( ( ph /\ ( 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 .- O ) = ( B .- s ) )
130 1 2 3 74 77 78 79 80 81 82 83 122 126 129 tgcgrextend 
 |-  ( ( ( ( ph /\ ( 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 ) .- O ) = ( R .- s ) )
131 1 2 3 74 77 80 axtgcgrrflx 
 |-  ( ( ( ( ph /\ ( 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 ) .- R ) = ( R .- ( ( S ` A ) ` O ) ) )
132 1 2 3 74 79 80 axtgcgrrflx 
 |-  ( ( ( ( ph /\ ( 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 .- R ) = ( R .- O ) )
133 60 ad2antrr 
 |-  ( ( ( ( ph /\ ( 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. ( R I O ) )
134 simprl 
 |-  ( ( ( ( ph /\ ( 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. ( ( ( S ` A ) ` O ) I s ) )
135 1 2 3 74 77 101 82 134 tgbtwncom 
 |-  ( ( ( ( ph /\ ( 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. ( s I ( ( S ` A ) ` O ) ) )
136 1 2 3 74 101 82 101 80 110 tgcgrcomlr 
 |-  ( ( ( ( ph /\ ( 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 .- x ) = ( R .- x ) )
137 136 eqcomd 
 |-  ( ( ( ( ph /\ ( 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 .- x ) = ( s .- x ) )
138 43 ad3antrrr 
 |-  ( ( ( ( ph /\ ( 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. ( raG ` G ) )
139 54 necomd 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> B =/= A )
140 139 ad2antrr 
 |-  ( ( ( ( ph /\ ( 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 )
141 65 ad2antrr 
 |-  ( ( ( ( ph /\ ( 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 ) )
142 141 orcd 
 |-  ( ( ( ( ph /\ ( 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 ) )
143 1 4 3 74 78 81 101 142 colcom 
 |-  ( ( ( ( ph /\ ( 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 ) )
144 1 4 3 74 81 78 101 143 colrot1 
 |-  ( ( ( ( ph /\ ( 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 ) )
145 1 2 3 4 6 74 81 78 79 101 138 140 144 ragcol 
 |-  ( ( ( ( ph /\ ( 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. ( raG ` G ) )
146 1 2 3 4 6 74 101 78 79 israg 
 |-  ( ( ( ( ph /\ ( 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. ( raG ` G ) <-> ( x .- O ) = ( x .- ( ( S ` A ) ` O ) ) ) )
147 145 146 mpbid 
 |-  ( ( ( ( ph /\ ( 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 ) ) )
148 1 2 3 74 80 101 79 82 101 77 133 135 137 147 tgcgrextend 
 |-  ( ( ( ( ph /\ ( 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 .- O ) = ( s .- ( ( S ` A ) ` O ) ) )
149 132 148 eqtrd 
 |-  ( ( ( ( ph /\ ( 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 .- R ) = ( s .- ( ( S ` A ) ` O ) ) )
150 1 2 3 74 77 78 79 80 80 81 82 77 83 122 130 129 131 149 tgifscgr 
 |-  ( ( ( ( ph /\ ( 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 .- R ) = ( B .- ( ( S ` A ) ` O ) ) )
151 73 150 eqtr4d 
 |-  ( ( ( ( ph /\ ( 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 ) = ( A .- R ) )
152 1 2 3 20 76 26 26 25 axtgsegcon 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> E. s e. P ( x e. ( ( ( S ` A ) ` O ) I s ) /\ ( x .- s ) = ( x .- R ) ) )
153 151 152 r19.29a 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( B .- O ) = ( A .- R ) )
154 19 adantr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( A .- O ) = ( B .- R ) )
155 1 2 3 20 24 23 22 25 154 tgcgrcomlr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( O .- A ) = ( R .- B ) )
156 143 152 r19.29a 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( x e. ( B L A ) \/ B = A ) )
157 1 4 3 20 23 25 26 61 btwncolg1 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( x e. ( O L R ) \/ O = R ) )
158 1 2 3 4 6 20 21 22 23 24 25 26 59 70 153 155 156 157 symquadlem 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> B = ( ( S ` x ) ` A ) )
159 1 2 3 4 6 20 26 21 24 mirbtwn 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> x e. ( ( ( S ` x ) ` A ) I A ) )
160 158 oveq1d 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( B I A ) = ( ( ( S ` x ) ` A ) I A ) )
161 159 160 eleqtrrd 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> x e. ( B I A ) )
162 1 2 3 20 22 26 24 161 tgbtwncom 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> x e. ( A I B ) )
163 1 2 3 20 24 22 axtgcgrrflx 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( A .- B ) = ( B .- A ) )
164 158 oveq2d 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( x .- B ) = ( x .- ( ( S ` x ) ` A ) ) )
165 1 2 3 4 6 20 26 21 24 mircgr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( x .- ( ( S ` x ) ` A ) ) = ( x .- A ) )
166 164 165 eqtrd 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( x .- B ) = ( x .- A ) )
167 1 2 3 20 24 26 22 23 22 26 24 25 162 161 163 166 154 153 tgifscgr 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( x .- O ) = ( x .- R ) )
168 1 2 3 4 6 20 26 21 25 23 167 61 ismir 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> O = ( ( S ` x ) ` R ) )
169 158 168 jca 
 |-  ( ( ph /\ ( x e. P /\ ( x e. ( T I B ) /\ x e. ( R I O ) ) ) ) -> ( B = ( ( S ` x ) ` A ) /\ O = ( ( S ` x ) ` R ) ) )
170 1 2 3 5 10 12 11 16 tgbtwncom 
 |-  ( ph -> T e. ( O I Q ) )
171 1 2 3 5 11 8 10 12 17 170 18 axtgpasch 
 |-  ( ph -> E. x e. P ( x e. ( T I B ) /\ x e. ( R I O ) ) )
172 169 171 reximddv 
 |-  ( ph -> E. x e. P ( B = ( ( S ` x ) ` A ) /\ O = ( ( S ` x ) ` R ) ) )