Metamath Proof Explorer

Theorem mirlni

Description: The mirror of a point X on a line ( Y L Z ) is on the mirrored line ( ( MY ) L ( MZ ) ) . (Contributed by Thierry Arnoux, 13-Jul-2026)

Ref Expression
Hypotheses mirlni.p 
|- P = ( Base ` G )
mirlni.l 
|- L = ( LineG ` G )
mirlni.s 
|- S = ( pInvG ` G )
mirlni.m 
|- M = ( S ` A )
mirlni.g 
|- ( ph -> G e. TarskiG )
mirlni.a 
|- ( ph -> A e. P )
mirlni.x 
|- ( ph -> X e. P )
mirlni.y 
|- ( ph -> Y e. P )
mirlni.z 
|- ( ph -> Z e. P )
mirlni.1 
|- ( ph -> Z =/= Y )
mirlni.2 
|- ( ph -> X e. ( Y L Z ) )
Assertion mirlni 
|- ( ph -> ( M ` X ) e. ( ( M ` Y ) L ( M ` Z ) ) )

Proof

Step Hyp Ref Expression
1 mirlni.p 
 |-  P = ( Base ` G )
2 mirlni.l 
 |-  L = ( LineG ` G )
3 mirlni.s 
 |-  S = ( pInvG ` G )
4 mirlni.m 
 |-  M = ( S ` A )
5 mirlni.g 
 |-  ( ph -> G e. TarskiG )
6 mirlni.a 
 |-  ( ph -> A e. P )
7 mirlni.x 
 |-  ( ph -> X e. P )
8 mirlni.y 
 |-  ( ph -> Y e. P )
9 mirlni.z 
 |-  ( ph -> Z e. P )
10 mirlni.1 
 |-  ( ph -> Z =/= Y )
11 mirlni.2 
 |-  ( ph -> X e. ( Y L Z ) )
12 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
13 10 necomd 
 |-  ( ph -> Y =/= Z )
14 1 2 12 5 8 9 13 7 tgellng 
 |-  ( ph -> ( X e. ( Y L Z ) <-> ( X e. ( Y ( Itv ` G ) Z ) \/ Y e. ( X ( Itv ` G ) Z ) \/ Z e. ( Y ( Itv ` G ) X ) ) ) )
15 11 14 mpbid 
 |-  ( ph -> ( X e. ( Y ( Itv ` G ) Z ) \/ Y e. ( X ( Itv ` G ) Z ) \/ Z e. ( Y ( Itv ` G ) X ) ) )
16 eqid 
 |-  ( dist ` G ) = ( dist ` G )
17 5 adantr 
 |-  ( ( ph /\ X e. ( Y ( Itv ` G ) Z ) ) -> G e. TarskiG )
18 6 adantr 
 |-  ( ( ph /\ X e. ( Y ( Itv ` G ) Z ) ) -> A e. P )
19 8 adantr 
 |-  ( ( ph /\ X e. ( Y ( Itv ` G ) Z ) ) -> Y e. P )
20 7 adantr 
 |-  ( ( ph /\ X e. ( Y ( Itv ` G ) Z ) ) -> X e. P )
21 9 adantr 
 |-  ( ( ph /\ X e. ( Y ( Itv ` G ) Z ) ) -> Z e. P )
22 simpr 
 |-  ( ( ph /\ X e. ( Y ( Itv ` G ) Z ) ) -> X e. ( Y ( Itv ` G ) Z ) )
23 1 16 12 2 3 17 18 4 19 20 21 22 mirbtwni 
 |-  ( ( ph /\ X e. ( Y ( Itv ` G ) Z ) ) -> ( M ` X ) e. ( ( M ` Y ) ( Itv ` G ) ( M ` Z ) ) )
24 5 adantr 
 |-  ( ( ph /\ Y e. ( X ( Itv ` G ) Z ) ) -> G e. TarskiG )
25 6 adantr 
 |-  ( ( ph /\ Y e. ( X ( Itv ` G ) Z ) ) -> A e. P )
26 7 adantr 
 |-  ( ( ph /\ Y e. ( X ( Itv ` G ) Z ) ) -> X e. P )
27 8 adantr 
 |-  ( ( ph /\ Y e. ( X ( Itv ` G ) Z ) ) -> Y e. P )
28 9 adantr 
 |-  ( ( ph /\ Y e. ( X ( Itv ` G ) Z ) ) -> Z e. P )
29 simpr 
 |-  ( ( ph /\ Y e. ( X ( Itv ` G ) Z ) ) -> Y e. ( X ( Itv ` G ) Z ) )
30 1 16 12 2 3 24 25 4 26 27 28 29 mirbtwni 
 |-  ( ( ph /\ Y e. ( X ( Itv ` G ) Z ) ) -> ( M ` Y ) e. ( ( M ` X ) ( Itv ` G ) ( M ` Z ) ) )
31 5 adantr 
 |-  ( ( ph /\ Z e. ( Y ( Itv ` G ) X ) ) -> G e. TarskiG )
32 6 adantr 
 |-  ( ( ph /\ Z e. ( Y ( Itv ` G ) X ) ) -> A e. P )
33 8 adantr 
 |-  ( ( ph /\ Z e. ( Y ( Itv ` G ) X ) ) -> Y e. P )
34 9 adantr 
 |-  ( ( ph /\ Z e. ( Y ( Itv ` G ) X ) ) -> Z e. P )
35 7 adantr 
 |-  ( ( ph /\ Z e. ( Y ( Itv ` G ) X ) ) -> X e. P )
36 simpr 
 |-  ( ( ph /\ Z e. ( Y ( Itv ` G ) X ) ) -> Z e. ( Y ( Itv ` G ) X ) )
37 1 16 12 2 3 31 32 4 33 34 35 36 mirbtwni 
 |-  ( ( ph /\ Z e. ( Y ( Itv ` G ) X ) ) -> ( M ` Z ) e. ( ( M ` Y ) ( Itv ` G ) ( M ` X ) ) )
38 15 23 30 37 3orim123da 
 |-  ( ph -> ( ( M ` X ) e. ( ( M ` Y ) ( Itv ` G ) ( M ` Z ) ) \/ ( M ` Y ) e. ( ( M ` X ) ( Itv ` G ) ( M ` Z ) ) \/ ( M ` Z ) e. ( ( M ` Y ) ( Itv ` G ) ( M ` X ) ) ) )
39 1 16 12 2 3 5 6 4 8 mircl 
 |-  ( ph -> ( M ` Y ) e. P )
40 1 16 12 2 3 5 6 4 9 mircl 
 |-  ( ph -> ( M ` Z ) e. P )
41 1 3 4 5 6 8 9 mirleqb 
 |-  ( ph -> ( Y = Z <-> ( M ` Y ) = ( M ` Z ) ) )
42 41 necon3bid 
 |-  ( ph -> ( Y =/= Z <-> ( M ` Y ) =/= ( M ` Z ) ) )
43 13 42 mpbid 
 |-  ( ph -> ( M ` Y ) =/= ( M ` Z ) )
44 1 16 12 2 3 5 6 4 7 mircl 
 |-  ( ph -> ( M ` X ) e. P )
45 1 2 12 5 39 40 43 44 tgellng 
 |-  ( ph -> ( ( M ` X ) e. ( ( M ` Y ) L ( M ` Z ) ) <-> ( ( M ` X ) e. ( ( M ` Y ) ( Itv ` G ) ( M ` Z ) ) \/ ( M ` Y ) e. ( ( M ` X ) ( Itv ` G ) ( M ` Z ) ) \/ ( M ` Z ) e. ( ( M ` Y ) ( Itv ` G ) ( M ` X ) ) ) ) )
46 38 45 mpbird 
 |-  ( ph -> ( M ` X ) e. ( ( M ` Y ) L ( M ` Z ) ) )