Metamath Proof Explorer

Theorem lmiopp

Description: Line mirroring produces points on the opposite side of the mirroring line. Theorem 10.14 of Schwabhauser p. 92. (Contributed by Thierry Arnoux, 2-Aug-2020)

Ref Expression
Hypotheses lmiopp.p 
|- P = ( Base ` G )
lmiopp.m 
|- .- = ( dist ` G )
lmiopp.i 
|- I = ( Itv ` G )
lmiopp.l 
|- L = ( LineG ` G )
lmiopp.g 
|- ( ph -> G e. TarskiG )
lmiopp.h 
|- ( ph -> G TarskiGDim>= 2 )
lmiopp.d 
|- ( ph -> D e. ran L )
lmiopp.o 
|- O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
lmiopp.n 
|- M = ( ( lInvG ` G ) ` D )
lmiopp.a 
|- ( ph -> A e. P )
lmiopp.1 
|- ( ph -> -. A e. D )
Assertion lmiopp 
|- ( ph -> A O ( M ` A ) )

Proof

Step Hyp Ref Expression
1 lmiopp.p 
 |-  P = ( Base ` G )
2 lmiopp.m 
 |-  .- = ( dist ` G )
3 lmiopp.i 
 |-  I = ( Itv ` G )
4 lmiopp.l 
 |-  L = ( LineG ` G )
5 lmiopp.g 
 |-  ( ph -> G e. TarskiG )
6 lmiopp.h 
 |-  ( ph -> G TarskiGDim>= 2 )
7 lmiopp.d 
 |-  ( ph -> D e. ran L )
8 lmiopp.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ D ) /\ b e. ( P \ D ) ) /\ E. t e. D t e. ( a I b ) ) }
9 lmiopp.n 
 |-  M = ( ( lInvG ` G ) ` D )
10 lmiopp.a 
 |-  ( ph -> A e. P )
11 lmiopp.1 
 |-  ( ph -> -. A e. D )
12 1 2 3 5 6 9 4 7 10 lmicl 
 |-  ( ph -> ( M ` A ) e. P )
13 eqidd 
 |-  ( ph -> ( M ` A ) = ( M ` A ) )
14 1 2 3 5 6 9 4 7 10 12 islmib 
 |-  ( ph -> ( ( M ` A ) = ( M ` A ) <-> ( ( A ( midG ` G ) ( M ` A ) ) e. D /\ ( D ( perpG ` G ) ( A L ( M ` A ) ) \/ A = ( M ` A ) ) ) ) )
15 13 14 mpbid 
 |-  ( ph -> ( ( A ( midG ` G ) ( M ` A ) ) e. D /\ ( D ( perpG ` G ) ( A L ( M ` A ) ) \/ A = ( M ` A ) ) ) )
16 15 simpld 
 |-  ( ph -> ( A ( midG ` G ) ( M ` A ) ) e. D )
17 1 2 3 5 6 9 4 7 10 lmilmi 
 |-  ( ph -> ( M ` ( M ` A ) ) = A )
18 17 eqeq1d 
 |-  ( ph -> ( ( M ` ( M ` A ) ) = ( M ` A ) <-> A = ( M ` A ) ) )
19 1 2 3 5 6 9 4 7 12 lmiinv 
 |-  ( ph -> ( ( M ` ( M ` A ) ) = ( M ` A ) <-> ( M ` A ) e. D ) )
20 eqcom 
 |-  ( A = ( M ` A ) <-> ( M ` A ) = A )
21 20 a1i 
 |-  ( ph -> ( A = ( M ` A ) <-> ( M ` A ) = A ) )
22 18 19 21 3bitr3d 
 |-  ( ph -> ( ( M ` A ) e. D <-> ( M ` A ) = A ) )
23 1 2 3 5 6 9 4 7 10 lmiinv 
 |-  ( ph -> ( ( M ` A ) = A <-> A e. D ) )
24 22 23 bitrd 
 |-  ( ph -> ( ( M ` A ) e. D <-> A e. D ) )
25 11 24 mtbird 
 |-  ( ph -> -. ( M ` A ) e. D )
26 1 2 3 5 6 10 12 midbtwn 
 |-  ( ph -> ( A ( midG ` G ) ( M ` A ) ) e. ( A I ( M ` A ) ) )
27 1 2 3 8 10 12 16 11 25 26 islnoppd 
 |-  ( ph -> A O ( M ` A ) )