Metamath Proof Explorer

Theorem lmicom

Description: The line mirroring function is an involution. Theorem 10.4 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 )
islmib.b 
|- ( ph -> B e. P )
lmicom.1 
|- ( ph -> ( M ` A ) = B )
Assertion lmicom 
|- ( ph -> ( 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 islmib.b 
 |-  ( ph -> B e. P )
11 lmicom.1 
 |-  ( ph -> ( M ` A ) = B )
12 1 2 3 4 5 9 10 midcom 
 |-  ( ph -> ( A ( midG ` G ) B ) = ( B ( midG ` G ) A ) )
13 11 eqcomd 
 |-  ( ph -> B = ( M ` A ) )
14 1 2 3 4 5 6 7 8 9 10 islmib 
 |-  ( ph -> ( B = ( M ` A ) <-> ( ( A ( midG ` G ) B ) e. D /\ ( D ( perpG ` G ) ( A L B ) \/ A = B ) ) ) )
15 13 14 mpbid 
 |-  ( ph -> ( ( A ( midG ` G ) B ) e. D /\ ( D ( perpG ` G ) ( A L B ) \/ A = B ) ) )
16 15 simpld 
 |-  ( ph -> ( A ( midG ` G ) B ) e. D )
17 12 16 eqeltrrd 
 |-  ( ph -> ( B ( midG ` G ) A ) e. D )
18 15 simprd 
 |-  ( ph -> ( D ( perpG ` G ) ( A L B ) \/ A = B ) )
19 18 orcomd 
 |-  ( ph -> ( A = B \/ D ( perpG ` G ) ( A L B ) ) )
20 19 ord 
 |-  ( ph -> ( -. A = B -> D ( perpG ` G ) ( A L B ) ) )
21 4 adantr 
 |-  ( ( ph /\ -. A = B ) -> G e. TarskiG )
22 9 adantr 
 |-  ( ( ph /\ -. A = B ) -> A e. P )
23 10 adantr 
 |-  ( ( ph /\ -. A = B ) -> B e. P )
24 simpr 
 |-  ( ( ph /\ -. A = B ) -> -. A = B )
25 24 neqned 
 |-  ( ( ph /\ -. A = B ) -> A =/= B )
26 1 3 7 21 22 23 25 tglinecom 
 |-  ( ( ph /\ -. A = B ) -> ( A L B ) = ( B L A ) )
27 26 breq2d 
 |-  ( ( ph /\ -. A = B ) -> ( D ( perpG ` G ) ( A L B ) <-> D ( perpG ` G ) ( B L A ) ) )
28 27 pm5.74da 
 |-  ( ph -> ( ( -. A = B -> D ( perpG ` G ) ( A L B ) ) <-> ( -. A = B -> D ( perpG ` G ) ( B L A ) ) ) )
29 20 28 mpbid 
 |-  ( ph -> ( -. A = B -> D ( perpG ` G ) ( B L A ) ) )
30 29 orrd 
 |-  ( ph -> ( A = B \/ D ( perpG ` G ) ( B L A ) ) )
31 30 orcomd 
 |-  ( ph -> ( D ( perpG ` G ) ( B L A ) \/ A = B ) )
32 eqcom 
 |-  ( A = B <-> B = A )
33 32 orbi2i 
 |-  ( ( D ( perpG ` G ) ( B L A ) \/ A = B ) <-> ( D ( perpG ` G ) ( B L A ) \/ B = A ) )
34 31 33 sylib 
 |-  ( ph -> ( D ( perpG ` G ) ( B L A ) \/ B = A ) )
35 1 2 3 4 5 6 7 8 10 9 islmib 
 |-  ( ph -> ( A = ( M ` B ) <-> ( ( B ( midG ` G ) A ) e. D /\ ( D ( perpG ` G ) ( B L A ) \/ B = A ) ) ) )
36 17 34 35 mpbir2and 
 |-  ( ph -> A = ( M ` B ) )
37 36 eqcomd 
 |-  ( ph -> ( M ` B ) = A )