Metamath Proof Explorer

Theorem mirreu3

Description: Existential uniqueness of the mirror point. Theorem 7.8 of Schwabhauser p. 49. (Contributed by Thierry Arnoux, 30-May-2019)

Ref Expression
Hypotheses mirreu.p 
|- P = ( Base ` G )
mirreu.d 
|- .- = ( dist ` G )
mirreu.i 
|- I = ( Itv ` G )
mirreu.g 
|- ( ph -> G e. TarskiG )
mirreu.a 
|- ( ph -> A e. P )
mirreu.m 
|- ( ph -> M e. P )
Assertion mirreu3 
|- ( ph -> E! b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )

Proof

Step Hyp Ref Expression
1 mirreu.p 
 |-  P = ( Base ` G )
2 mirreu.d 
 |-  .- = ( dist ` G )
3 mirreu.i 
 |-  I = ( Itv ` G )
4 mirreu.g 
 |-  ( ph -> G e. TarskiG )
5 mirreu.a 
 |-  ( ph -> A e. P )
6 mirreu.m 
 |-  ( ph -> M e. P )
7 5 adantr 
 |-  ( ( ph /\ A = M ) -> A e. P )
8 eqidd 
 |-  ( ( ph /\ A = M ) -> ( M .- A ) = ( M .- A ) )
9 simpr 
 |-  ( ( ph /\ A = M ) -> A = M )
10 4 adantr 
 |-  ( ( ph /\ A = M ) -> G e. TarskiG )
11 1 2 3 10 7 7 tgbtwntriv2 
 |-  ( ( ph /\ A = M ) -> A e. ( A I A ) )
12 9 11 eqeltrrd 
 |-  ( ( ph /\ A = M ) -> M e. ( A I A ) )
13 oveq2 
 |-  ( b = A -> ( M .- b ) = ( M .- A ) )
14 13 eqeq1d 
 |-  ( b = A -> ( ( M .- b ) = ( M .- A ) <-> ( M .- A ) = ( M .- A ) ) )
15 oveq1 
 |-  ( b = A -> ( b I A ) = ( A I A ) )
16 15 eleq2d 
 |-  ( b = A -> ( M e. ( b I A ) <-> M e. ( A I A ) ) )
17 14 16 anbi12d 
 |-  ( b = A -> ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) <-> ( ( M .- A ) = ( M .- A ) /\ M e. ( A I A ) ) ) )
18 17 rspcev 
 |-  ( ( A e. P /\ ( ( M .- A ) = ( M .- A ) /\ M e. ( A I A ) ) ) -> E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )
19 7 8 12 18 syl12anc 
 |-  ( ( ph /\ A = M ) -> E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )
20 4 ad3antrrr 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> G e. TarskiG )
21 6 ad3antrrr 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. P )
22 simplrl 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> b e. P )
23 simprll 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- b ) = ( M .- A ) )
24 simpllr 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> A = M )
25 24 oveq2d 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- A ) = ( M .- M ) )
26 23 25 eqtrd 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- b ) = ( M .- M ) )
27 1 2 3 20 21 22 21 26 axtgcgrid 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M = b )
28 simplrr 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> c e. P )
29 simprrl 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- c ) = ( M .- A ) )
30 29 25 eqtrd 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- c ) = ( M .- M ) )
31 1 2 3 20 21 28 21 30 axtgcgrid 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M = c )
32 27 31 eqtr3d 
 |-  ( ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> b = c )
33 32 ex 
 |-  ( ( ( ph /\ A = M ) /\ ( b e. P /\ c e. P ) ) -> ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) )
34 33 ralrimivva 
 |-  ( ( ph /\ A = M ) -> A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) )
35 19 34 jca 
 |-  ( ( ph /\ A = M ) -> ( E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) ) )
36 4 adantr 
 |-  ( ( ph /\ A =/= M ) -> G e. TarskiG )
37 5 adantr 
 |-  ( ( ph /\ A =/= M ) -> A e. P )
38 6 adantr 
 |-  ( ( ph /\ A =/= M ) -> M e. P )
39 1 2 3 36 37 38 38 37 axtgsegcon 
 |-  ( ( ph /\ A =/= M ) -> E. b e. P ( M e. ( A I b ) /\ ( M .- b ) = ( M .- A ) ) )
40 ancom 
 |-  ( ( M e. ( A I b ) /\ ( M .- b ) = ( M .- A ) ) <-> ( ( M .- b ) = ( M .- A ) /\ M e. ( A I b ) ) )
41 4 adantr 
 |-  ( ( ph /\ b e. P ) -> G e. TarskiG )
42 5 adantr 
 |-  ( ( ph /\ b e. P ) -> A e. P )
43 6 adantr 
 |-  ( ( ph /\ b e. P ) -> M e. P )
44 simpr 
 |-  ( ( ph /\ b e. P ) -> b e. P )
45 1 2 3 41 42 43 44 tgbtwncomb 
 |-  ( ( ph /\ b e. P ) -> ( M e. ( A I b ) <-> M e. ( b I A ) ) )
46 45 anbi2d 
 |-  ( ( ph /\ b e. P ) -> ( ( ( M .- b ) = ( M .- A ) /\ M e. ( A I b ) ) <-> ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) ) )
47 40 46 syl5bb 
 |-  ( ( ph /\ b e. P ) -> ( ( M e. ( A I b ) /\ ( M .- b ) = ( M .- A ) ) <-> ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) ) )
48 47 rexbidva 
 |-  ( ph -> ( E. b e. P ( M e. ( A I b ) /\ ( M .- b ) = ( M .- A ) ) <-> E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) ) )
49 48 adantr 
 |-  ( ( ph /\ A =/= M ) -> ( E. b e. P ( M e. ( A I b ) /\ ( M .- b ) = ( M .- A ) ) <-> E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) ) )
50 39 49 mpbid 
 |-  ( ( ph /\ A =/= M ) -> E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )
51 4 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> G e. TarskiG )
52 6 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. P )
53 5 ad3antrrr 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> A e. P )
54 simplrl 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> b e. P )
55 simplrr 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> c e. P )
56 simpllr 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> A =/= M )
57 simprlr 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. ( b I A ) )
58 1 2 3 51 54 52 53 57 tgbtwncom 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. ( A I b ) )
59 simprrr 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. ( c I A ) )
60 1 2 3 51 55 52 53 59 tgbtwncom 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> M e. ( A I c ) )
61 simprll 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- b ) = ( M .- A ) )
62 simprrl 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> ( M .- c ) = ( M .- A ) )
63 1 2 3 51 52 52 53 53 54 55 56 58 60 61 62 tgsegconeq 
 |-  ( ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) /\ ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) ) -> b = c )
64 63 ex 
 |-  ( ( ( ph /\ A =/= M ) /\ ( b e. P /\ c e. P ) ) -> ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) )
65 64 ralrimivva 
 |-  ( ( ph /\ A =/= M ) -> A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) )
66 50 65 jca 
 |-  ( ( ph /\ A =/= M ) -> ( E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) ) )
67 35 66 pm2.61dane 
 |-  ( ph -> ( E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) ) )
68 oveq2 
 |-  ( b = c -> ( M .- b ) = ( M .- c ) )
69 68 eqeq1d 
 |-  ( b = c -> ( ( M .- b ) = ( M .- A ) <-> ( M .- c ) = ( M .- A ) ) )
70 oveq1 
 |-  ( b = c -> ( b I A ) = ( c I A ) )
71 70 eleq2d 
 |-  ( b = c -> ( M e. ( b I A ) <-> M e. ( c I A ) ) )
72 69 71 anbi12d 
 |-  ( b = c -> ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) <-> ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) )
73 72 reu4 
 |-  ( E! b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) <-> ( E. b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ A. b e. P A. c e. P ( ( ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) /\ ( ( M .- c ) = ( M .- A ) /\ M e. ( c I A ) ) ) -> b = c ) ) )
74 67 73 sylibr 
 |-  ( ph -> E! b e. P ( ( M .- b ) = ( M .- A ) /\ M e. ( b I A ) ) )