Metamath Proof Explorer

Theorem lmieu

Description: Uniqueness of the line mirror point. Theorem 10.2 of Schwabhauser p. 88. (Contributed by Thierry Arnoux, 1-Dec-2019)

Ref Expression
Hypotheses ismid.p 
|- P = ( Base ` G )
ismid.d 
|- .- = ( dist ` G )
ismid.i 
|- I = ( Itv ` G )
ismid.g 
|- ( ph -> G e. TarskiG )
ismid.1 
|- ( ph -> G TarskiGDim>= 2 )
lmieu.l 
|- L = ( LineG ` G )
lmieu.1 
|- ( ph -> D e. ran L )
lmieu.a 
|- ( ph -> A e. P )
Assertion lmieu 
|- ( ph -> E! b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )

Proof

Step Hyp Ref Expression
1 ismid.p 
 |-  P = ( Base ` G )
2 ismid.d 
 |-  .- = ( dist ` G )
3 ismid.i 
 |-  I = ( Itv ` G )
4 ismid.g 
 |-  ( ph -> G e. TarskiG )
5 ismid.1 
 |-  ( ph -> G TarskiGDim>= 2 )
6 lmieu.l 
 |-  L = ( LineG ` G )
7 lmieu.1 
 |-  ( ph -> D e. ran L )
8 lmieu.a 
 |-  ( ph -> A e. P )
9 8 adantr 
 |-  ( ( ph /\ A e. D ) -> A e. P )
10 simpr 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> -. A = b )
11 eqidd 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> ( A ( midG ` G ) b ) = ( A ( midG ` G ) b ) )
12 4 ad4antr 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> G e. TarskiG )
13 5 ad4antr 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> G TarskiGDim>= 2 )
14 9 ad3antrrr 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> A e. P )
15 simpllr 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> b e. P )
16 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
17 1 2 3 12 13 14 15 midcl 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> ( A ( midG ` G ) b ) e. P )
18 1 2 3 12 13 14 15 16 17 ismidb 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> ( b = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) b ) ) ` A ) <-> ( A ( midG ` G ) b ) = ( A ( midG ` G ) b ) ) )
19 11 18 mpbird 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> b = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) b ) ) ` A ) )
20 19 adantr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> b = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) b ) ) ` A ) )
21 12 adantr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> G e. TarskiG )
22 7 ad4antr 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> D e. ran L )
23 22 adantr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> D e. ran L )
24 14 adantr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> A e. P )
25 15 adantr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> b e. P )
26 10 neqned 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> A =/= b )
27 26 adantr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> A =/= b )
28 1 3 6 21 24 25 27 tgelrnln 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> ( A L b ) e. ran L )
29 simpr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> D =/= ( A L b ) )
30 simp-4r 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> A e. D )
31 30 adantr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> A e. D )
32 1 3 6 21 24 25 27 tglinerflx1 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> A e. ( A L b ) )
33 31 32 elind 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> A e. ( D i^i ( A L b ) ) )
34 simpllr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> ( A ( midG ` G ) b ) e. D )
35 1 2 3 12 13 14 15 midbtwn 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> ( A ( midG ` G ) b ) e. ( A I b ) )
36 1 3 6 12 14 15 17 26 35 btwnlng1 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> ( A ( midG ` G ) b ) e. ( A L b ) )
37 36 adantr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> ( A ( midG ` G ) b ) e. ( A L b ) )
38 34 37 elind 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> ( A ( midG ` G ) b ) e. ( D i^i ( A L b ) ) )
39 1 3 6 21 23 28 29 33 38 tglineineq 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> A = ( A ( midG ` G ) b ) )
40 39 fveq2d 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> ( ( pInvG ` G ) ` A ) = ( ( pInvG ` G ) ` ( A ( midG ` G ) b ) ) )
41 40 fveq1d 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> ( ( ( pInvG ` G ) ` A ) ` A ) = ( ( ( pInvG ` G ) ` ( A ( midG ` G ) b ) ) ` A ) )
42 eqid 
 |-  ( ( pInvG ` G ) ` A ) = ( ( pInvG ` G ) ` A )
43 1 2 3 6 16 21 24 42 mircinv 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> ( ( ( pInvG ` G ) ` A ) ` A ) = A )
44 20 41 43 3eqtr2rd 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D =/= ( A L b ) ) -> A = b )
45 10 44 mtand 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> -. D =/= ( A L b ) )
46 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D ( perpG ` G ) ( A L b ) ) -> G e. TarskiG )
47 7 ad5antr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D ( perpG ` G ) ( A L b ) ) -> D e. ran L )
48 nne 
 |-  ( -. D =/= ( A L b ) <-> D = ( A L b ) )
49 45 48 sylib 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> D = ( A L b ) )
50 49 adantr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D ( perpG ` G ) ( A L b ) ) -> D = ( A L b ) )
51 50 47 eqeltrrd 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D ( perpG ` G ) ( A L b ) ) -> ( A L b ) e. ran L )
52 simpr 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D ( perpG ` G ) ( A L b ) ) -> D ( perpG ` G ) ( A L b ) )
53 1 2 3 6 46 47 51 52 perpneq 
 |-  ( ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) /\ D ( perpG ` G ) ( A L b ) ) -> D =/= ( A L b ) )
54 45 53 mtand 
 |-  ( ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) /\ -. A = b ) -> -. D ( perpG ` G ) ( A L b ) )
55 54 ex 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) -> ( -. A = b -> -. D ( perpG ` G ) ( A L b ) ) )
56 55 con4d 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) -> ( D ( perpG ` G ) ( A L b ) -> A = b ) )
57 idd 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) -> ( A = b -> A = b ) )
58 56 57 jaod 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( A ( midG ` G ) b ) e. D ) -> ( ( D ( perpG ` G ) ( A L b ) \/ A = b ) -> A = b ) )
59 58 impr 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> A = b )
60 59 eqcomd 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> b = A )
61 simpr 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ b = A ) -> b = A )
62 61 oveq2d 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ b = A ) -> ( A ( midG ` G ) b ) = ( A ( midG ` G ) A ) )
63 1 2 3 4 5 8 8 midid 
 |-  ( ph -> ( A ( midG ` G ) A ) = A )
64 63 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ b = A ) -> ( A ( midG ` G ) A ) = A )
65 62 64 eqtrd 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ b = A ) -> ( A ( midG ` G ) b ) = A )
66 simpllr 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ b = A ) -> A e. D )
67 65 66 eqeltrd 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ b = A ) -> ( A ( midG ` G ) b ) e. D )
68 61 eqcomd 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ b = A ) -> A = b )
69 68 olcd 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ b = A ) -> ( D ( perpG ` G ) ( A L b ) \/ A = b ) )
70 67 69 jca 
 |-  ( ( ( ( ph /\ A e. D ) /\ b e. P ) /\ b = A ) -> ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )
71 60 70 impbida 
 |-  ( ( ( ph /\ A e. D ) /\ b e. P ) -> ( ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) <-> b = A ) )
72 71 ralrimiva 
 |-  ( ( ph /\ A e. D ) -> A. b e. P ( ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) <-> b = A ) )
73 reu6i 
 |-  ( ( A e. P /\ A. b e. P ( ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) <-> b = A ) ) -> E! b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )
74 9 72 73 syl2anc 
 |-  ( ( ph /\ A e. D ) -> E! b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )
75 4 adantr 
 |-  ( ( ph /\ -. A e. D ) -> G e. TarskiG )
76 75 ad2antrr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) -> G e. TarskiG )
77 7 adantr 
 |-  ( ( ph /\ -. A e. D ) -> D e. ran L )
78 77 ad2antrr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) -> D e. ran L )
79 simplr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) -> x e. D )
80 1 6 3 76 78 79 tglnpt 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) -> x e. P )
81 eqid 
 |-  ( ( pInvG ` G ) ` x ) = ( ( pInvG ` G ) ` x )
82 8 adantr 
 |-  ( ( ph /\ -. A e. D ) -> A e. P )
83 82 ad2antrr 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) -> A e. P )
84 1 2 3 6 16 76 80 81 83 mircl 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) -> ( ( ( pInvG ` G ) ` x ) ` A ) e. P )
85 oveq2 
 |-  ( x = ( A ( midG ` G ) b ) -> ( A L x ) = ( A L ( A ( midG ` G ) b ) ) )
86 85 breq1d 
 |-  ( x = ( A ( midG ` G ) b ) -> ( ( A L x ) ( perpG ` G ) D <-> ( A L ( A ( midG ` G ) b ) ) ( perpG ` G ) D ) )
87 simprl 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A ( midG ` G ) b ) e. D )
88 simpr 
 |-  ( ( ph /\ -. A e. D ) -> -. A e. D )
89 1 2 3 6 75 77 82 88 foot 
 |-  ( ( ph /\ -. A e. D ) -> E! x e. D ( A L x ) ( perpG ` G ) D )
90 reurmo 
 |-  ( E! x e. D ( A L x ) ( perpG ` G ) D -> E* x e. D ( A L x ) ( perpG ` G ) D )
91 89 90 syl 
 |-  ( ( ph /\ -. A e. D ) -> E* x e. D ( A L x ) ( perpG ` G ) D )
92 91 ad4antr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> E* x e. D ( A L x ) ( perpG ` G ) D )
93 79 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> x e. D )
94 simpllr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A L x ) ( perpG ` G ) D )
95 76 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> G e. TarskiG )
96 83 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> A e. P )
97 simplr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> b e. P )
98 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> G TarskiGDim>= 2 )
99 1 2 3 95 98 96 97 midcl 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A ( midG ` G ) b ) e. P )
100 1 2 3 95 98 96 97 midbtwn 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A ( midG ` G ) b ) e. ( A I b ) )
101 88 ad4antr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> -. A e. D )
102 nelne2 
 |-  ( ( ( A ( midG ` G ) b ) e. D /\ -. A e. D ) -> ( A ( midG ` G ) b ) =/= A )
103 87 101 102 syl2anc 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A ( midG ` G ) b ) =/= A )
104 1 2 3 95 96 99 97 100 103 tgbtwnne 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> A =/= b )
105 1 3 6 95 96 97 99 104 100 btwnlng1 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A ( midG ` G ) b ) e. ( A L b ) )
106 1 3 6 95 96 97 104 99 103 105 tglineelsb2 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A L b ) = ( A L ( A ( midG ` G ) b ) ) )
107 78 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> D e. ran L )
108 1 3 6 95 96 97 104 tgelrnln 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A L b ) e. ran L )
109 104 neneqd 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> -. A = b )
110 simprr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( D ( perpG ` G ) ( A L b ) \/ A = b ) )
111 110 orcomd 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A = b \/ D ( perpG ` G ) ( A L b ) ) )
112 111 ord 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( -. A = b -> D ( perpG ` G ) ( A L b ) ) )
113 109 112 mpd 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> D ( perpG ` G ) ( A L b ) )
114 1 2 3 6 95 107 108 113 perpcom 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A L b ) ( perpG ` G ) D )
115 106 114 eqbrtrrd 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A L ( A ( midG ` G ) b ) ) ( perpG ` G ) D )
116 86 87 92 93 94 115 rmoi2 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> x = ( A ( midG ` G ) b ) )
117 116 eqcomd 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( A ( midG ` G ) b ) = x )
118 80 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> x e. P )
119 1 2 3 95 98 96 97 16 118 ismidb 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> ( b = ( ( ( pInvG ` G ) ` x ) ` A ) <-> ( A ( midG ` G ) b ) = x ) )
120 117 119 mpbird 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) ) -> b = ( ( ( pInvG ` G ) ` x ) ` A ) )
121 simpr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> b = ( ( ( pInvG ` G ) ` x ) ` A ) )
122 76 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> G e. TarskiG )
123 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> G TarskiGDim>= 2 )
124 83 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> A e. P )
125 simplr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> b e. P )
126 80 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> x e. P )
127 1 2 3 122 123 124 125 16 126 ismidb 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> ( b = ( ( ( pInvG ` G ) ` x ) ` A ) <-> ( A ( midG ` G ) b ) = x ) )
128 121 127 mpbid 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> ( A ( midG ` G ) b ) = x )
129 79 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> x e. D )
130 128 129 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> ( A ( midG ` G ) b ) e. D )
131 122 adantr 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> G e. TarskiG )
132 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> ( A L x ) ( perpG ` G ) D )
133 6 131 132 perpln1 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> ( A L x ) e. ran L )
134 78 ad3antrrr 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> D e. ran L )
135 1 2 3 6 131 133 134 132 perpcom 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> D ( perpG ` G ) ( A L x ) )
136 124 adantr 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> A e. P )
137 126 adantr 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> x e. P )
138 1 3 6 131 136 137 133 tglnne 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> A =/= x )
139 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> b e. P )
140 simpr 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> A =/= b )
141 140 necomd 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> b =/= A )
142 1 2 3 6 16 131 137 81 136 mirbtwn 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> x e. ( ( ( ( pInvG ` G ) ` x ) ` A ) I A ) )
143 simplr 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> b = ( ( ( pInvG ` G ) ` x ) ` A ) )
144 143 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> ( b I A ) = ( ( ( ( pInvG ` G ) ` x ) ` A ) I A ) )
145 142 144 eleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> x e. ( b I A ) )
146 1 3 6 131 139 136 137 141 145 btwnlng1 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> x e. ( b L A ) )
147 1 3 6 131 136 137 139 138 146 141 lnrot1 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> b e. ( A L x ) )
148 1 3 6 131 136 137 138 139 141 147 tglineelsb2 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> ( A L x ) = ( A L b ) )
149 135 148 breqtrd 
 |-  ( ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) /\ A =/= b ) -> D ( perpG ` G ) ( A L b ) )
150 149 ex 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> ( A =/= b -> D ( perpG ` G ) ( A L b ) ) )
151 150 necon1bd 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> ( -. D ( perpG ` G ) ( A L b ) -> A = b ) )
152 151 orrd 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> ( D ( perpG ` G ) ( A L b ) \/ A = b ) )
153 130 152 jca 
 |-  ( ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) /\ b = ( ( ( pInvG ` G ) ` x ) ` A ) ) -> ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )
154 120 153 impbida 
 |-  ( ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) /\ b e. P ) -> ( ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) <-> b = ( ( ( pInvG ` G ) ` x ) ` A ) ) )
155 154 ralrimiva 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) -> A. b e. P ( ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) <-> b = ( ( ( pInvG ` G ) ` x ) ` A ) ) )
156 reu6i 
 |-  ( ( ( ( ( pInvG ` G ) ` x ) ` A ) e. P /\ A. b e. P ( ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) <-> b = ( ( ( pInvG ` G ) ` x ) ` A ) ) ) -> E! b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )
157 84 155 156 syl2anc 
 |-  ( ( ( ( ph /\ -. A e. D ) /\ x e. D ) /\ ( A L x ) ( perpG ` G ) D ) -> E! b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )
158 1 2 3 6 75 77 82 88 footex 
 |-  ( ( ph /\ -. A e. D ) -> E. x e. D ( A L x ) ( perpG ` G ) D )
159 157 158 r19.29a 
 |-  ( ( ph /\ -. A e. D ) -> E! b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )
160 74 159 pm2.61dan 
 |-  ( ph -> E! b e. P ( ( A ( midG ` G ) b ) e. D /\ ( D ( perpG ` G ) ( A L b ) \/ A = b ) ) )