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