Metamath Proof Explorer

Theorem lmireu

Description: Any point has a unique antecedent through line mirroring. Theorem 10.6 of Schwabhauser p. 89. (Contributed by Thierry Arnoux, 11-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 )
lmif.m 
|- M = ( ( lInvG ` G ) ` D )
lmif.l 
|- L = ( LineG ` G )
lmif.d 
|- ( ph -> D e. ran L )
lmicl.1 
|- ( ph -> A e. P )
Assertion lmireu 
|- ( ph -> E! b e. P ( M ` b ) = A )

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 lmif.m 
 |-  M = ( ( lInvG ` G ) ` D )
7 lmif.l 
 |-  L = ( LineG ` G )
8 lmif.d 
 |-  ( ph -> D e. ran L )
9 lmicl.1 
 |-  ( ph -> A e. P )
10 1 2 3 4 5 6 7 8 9 lmicl 
 |-  ( ph -> ( M ` A ) e. P )
11 1 2 3 4 5 6 7 8 9 lmilmi 
 |-  ( ph -> ( M ` ( M ` A ) ) = A )
12 4 ad2antrr 
 |-  ( ( ( ph /\ b e. P ) /\ ( M ` b ) = A ) -> G e. TarskiG )
13 5 ad2antrr 
 |-  ( ( ( ph /\ b e. P ) /\ ( M ` b ) = A ) -> G TarskiGDim>= 2 )
14 8 ad2antrr 
 |-  ( ( ( ph /\ b e. P ) /\ ( M ` b ) = A ) -> D e. ran L )
15 simplr 
 |-  ( ( ( ph /\ b e. P ) /\ ( M ` b ) = A ) -> b e. P )
16 1 2 3 12 13 6 7 14 15 lmilmi 
 |-  ( ( ( ph /\ b e. P ) /\ ( M ` b ) = A ) -> ( M ` ( M ` b ) ) = b )
17 simpr 
 |-  ( ( ( ph /\ b e. P ) /\ ( M ` b ) = A ) -> ( M ` b ) = A )
18 17 fveq2d 
 |-  ( ( ( ph /\ b e. P ) /\ ( M ` b ) = A ) -> ( M ` ( M ` b ) ) = ( M ` A ) )
19 16 18 eqtr3d 
 |-  ( ( ( ph /\ b e. P ) /\ ( M ` b ) = A ) -> b = ( M ` A ) )
20 19 ex 
 |-  ( ( ph /\ b e. P ) -> ( ( M ` b ) = A -> b = ( M ` A ) ) )
21 20 ralrimiva 
 |-  ( ph -> A. b e. P ( ( M ` b ) = A -> b = ( M ` A ) ) )
22 fveqeq2 
 |-  ( b = ( M ` A ) -> ( ( M ` b ) = A <-> ( M ` ( M ` A ) ) = A ) )
23 22 eqreu 
 |-  ( ( ( M ` A ) e. P /\ ( M ` ( M ` A ) ) = A /\ A. b e. P ( ( M ` b ) = A -> b = ( M ` A ) ) ) -> E! b e. P ( M ` b ) = A )
24 10 11 21 23 syl3anc 
 |-  ( ph -> E! b e. P ( M ` b ) = A )