Metamath Proof Explorer

Theorem lmimid

Description: If we have a right angle, then the mirror point is the point inversion. (Contributed by Thierry Arnoux, 15-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 )
lmimid.s 
|- S = ( ( pInvG ` G ) ` B )
lmimid.r 
|- ( ph -> <" A B C "> e. ( raG ` G ) )
lmimid.a 
|- ( ph -> A e. D )
lmimid.b 
|- ( ph -> B e. D )
lmimid.c 
|- ( ph -> C e. P )
lmimid.d 
|- ( ph -> A =/= B )
Assertion lmimid 
|- ( ph -> ( M ` C ) = ( S ` C ) )

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 lmimid.s 
 |-  S = ( ( pInvG ` G ) ` B )
11 lmimid.r 
 |-  ( ph -> <" A B C "> e. ( raG ` G ) )
12 lmimid.a 
 |-  ( ph -> A e. D )
13 lmimid.b 
 |-  ( ph -> B e. D )
14 lmimid.c 
 |-  ( ph -> C e. P )
15 lmimid.d 
 |-  ( ph -> A =/= B )
16 10 a1i 
 |-  ( ph -> S = ( ( pInvG ` G ) ` B ) )
17 16 fveq1d 
 |-  ( ph -> ( S ` C ) = ( ( ( pInvG ` G ) ` B ) ` C ) )
18 eqid 
 |-  ( pInvG ` G ) = ( pInvG ` G )
19 1 7 3 4 8 13 tglnpt 
 |-  ( ph -> B e. P )
20 1 2 3 7 18 4 19 10 14 mircl 
 |-  ( ph -> ( S ` C ) e. P )
21 1 2 3 4 5 14 20 18 19 ismidb 
 |-  ( ph -> ( ( S ` C ) = ( ( ( pInvG ` G ) ` B ) ` C ) <-> ( C ( midG ` G ) ( S ` C ) ) = B ) )
22 17 21 mpbid 
 |-  ( ph -> ( C ( midG ` G ) ( S ` C ) ) = B )
23 22 13 eqeltrd 
 |-  ( ph -> ( C ( midG ` G ) ( S ` C ) ) e. D )
24 df-ne 
 |-  ( C =/= ( S ` C ) <-> -. C = ( S ` C ) )
25 4 adantr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> G e. TarskiG )
26 8 adantr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> D e. ran L )
27 14 adantr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> C e. P )
28 20 adantr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> ( S ` C ) e. P )
29 simpr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> C =/= ( S ` C ) )
30 1 3 7 25 27 28 29 tgelrnln 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> ( C L ( S ` C ) ) e. ran L )
31 13 adantr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> B e. D )
32 19 adantr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> B e. P )
33 1 2 3 4 5 14 20 midbtwn 
 |-  ( ph -> ( C ( midG ` G ) ( S ` C ) ) e. ( C I ( S ` C ) ) )
34 22 33 eqeltrrd 
 |-  ( ph -> B e. ( C I ( S ` C ) ) )
35 34 adantr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> B e. ( C I ( S ` C ) ) )
36 1 3 7 25 27 28 32 29 35 btwnlng1 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> B e. ( C L ( S ` C ) ) )
37 31 36 elind 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> B e. ( D i^i ( C L ( S ` C ) ) ) )
38 12 adantr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> A e. D )
39 1 3 7 25 27 28 29 tglinerflx1 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> C e. ( C L ( S ` C ) ) )
40 15 adantr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> A =/= B )
41 1 2 3 7 18 4 19 10 14 mirinv 
 |-  ( ph -> ( ( S ` C ) = C <-> B = C ) )
42 eqcom 
 |-  ( B = C <-> C = B )
43 41 42 bitrdi 
 |-  ( ph -> ( ( S ` C ) = C <-> C = B ) )
44 43 biimpar 
 |-  ( ( ph /\ C = B ) -> ( S ` C ) = C )
45 44 eqcomd 
 |-  ( ( ph /\ C = B ) -> C = ( S ` C ) )
46 45 ex 
 |-  ( ph -> ( C = B -> C = ( S ` C ) ) )
47 46 necon3d 
 |-  ( ph -> ( C =/= ( S ` C ) -> C =/= B ) )
48 47 imp 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> C =/= B )
49 11 adantr 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> <" A B C "> e. ( raG ` G ) )
50 1 2 3 7 25 26 30 37 38 39 40 48 49 ragperp 
 |-  ( ( ph /\ C =/= ( S ` C ) ) -> D ( perpG ` G ) ( C L ( S ` C ) ) )
51 50 ex 
 |-  ( ph -> ( C =/= ( S ` C ) -> D ( perpG ` G ) ( C L ( S ` C ) ) ) )
52 24 51 syl5bir 
 |-  ( ph -> ( -. C = ( S ` C ) -> D ( perpG ` G ) ( C L ( S ` C ) ) ) )
53 52 orrd 
 |-  ( ph -> ( C = ( S ` C ) \/ D ( perpG ` G ) ( C L ( S ` C ) ) ) )
54 53 orcomd 
 |-  ( ph -> ( D ( perpG ` G ) ( C L ( S ` C ) ) \/ C = ( S ` C ) ) )
55 1 2 3 4 5 6 7 8 14 20 islmib 
 |-  ( ph -> ( ( S ` C ) = ( M ` C ) <-> ( ( C ( midG ` G ) ( S ` C ) ) e. D /\ ( D ( perpG ` G ) ( C L ( S ` C ) ) \/ C = ( S ` C ) ) ) ) )
56 23 54 55 mpbir2and 
 |-  ( ph -> ( S ` C ) = ( M ` C ) )
57 56 eqcomd 
 |-  ( ph -> ( M ` C ) = ( S ` C ) )