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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
mirlni.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
mirlni.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
mirlni.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
mirlni.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
mirlni.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
mirlni.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
mirlni.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
mirlni.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
mirlni.1 ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
mirlni.2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
Assertion mirlni ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 mirlni.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 mirlni.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 mirlni.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
4 mirlni.m ⊢ 𝑀 = ( 𝑆 ‘ 𝐴 )
5 mirlni.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 mirlni.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 mirlni.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
8 mirlni.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
9 mirlni.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
10 mirlni.1 ⊢ ( 𝜑 → 𝑍 ≠ 𝑌 )
11 mirlni.2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
12 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
13 10 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
14 1 2 12 5 8 9 13 7 tgellng ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ↔ ( 𝑋 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑍 ) ∨ 𝑌 ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) ∨ 𝑍 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) ) )
15 11 14 mpbid ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑍 ) ∨ 𝑌 ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) ∨ 𝑍 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) )
16 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
17 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝐺 ∈ TarskiG )
18 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝐴 ∈ 𝑃 )
19 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝑌 ∈ 𝑃 )
20 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝑋 ∈ 𝑃 )
21 9 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝑍 ∈ 𝑃 )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝑋 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑍 ) )
23 1 16 12 2 3 17 18 4 19 20 21 22 mirbtwni ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑍 ) ) → ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑌 ) ( Itv ‘ 𝐺 ) ( 𝑀 ‘ 𝑍 ) ) )
24 5 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝐺 ∈ TarskiG )
25 6 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝐴 ∈ 𝑃 )
26 7 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝑋 ∈ 𝑃 )
27 8 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝑌 ∈ 𝑃 )
28 9 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝑍 ∈ 𝑃 )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) ) → 𝑌 ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) )
30 1 16 12 2 3 24 25 4 26 27 28 29 mirbtwni ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑋 ( Itv ‘ 𝐺 ) 𝑍 ) ) → ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) ( Itv ‘ 𝐺 ) ( 𝑀 ‘ 𝑍 ) ) )
31 5 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝐺 ∈ TarskiG )
32 6 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝐴 ∈ 𝑃 )
33 8 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑌 ∈ 𝑃 )
34 9 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑍 ∈ 𝑃 )
35 7 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑋 ∈ 𝑃 )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → 𝑍 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) )
37 1 16 12 2 3 31 32 4 33 34 35 36 mirbtwni ⊢ ( ( 𝜑 ∧ 𝑍 ∈ ( 𝑌 ( Itv ‘ 𝐺 ) 𝑋 ) ) → ( 𝑀 ‘ 𝑍 ) ∈ ( ( 𝑀 ‘ 𝑌 ) ( Itv ‘ 𝐺 ) ( 𝑀 ‘ 𝑋 ) ) )
38 15 23 30 37 3orim123da ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑌 ) ( Itv ‘ 𝐺 ) ( 𝑀 ‘ 𝑍 ) ) ∨ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) ( Itv ‘ 𝐺 ) ( 𝑀 ‘ 𝑍 ) ) ∨ ( 𝑀 ‘ 𝑍 ) ∈ ( ( 𝑀 ‘ 𝑌 ) ( Itv ‘ 𝐺 ) ( 𝑀 ‘ 𝑋 ) ) ) )
39 1 16 12 2 3 5 6 4 8 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ∈ 𝑃 )
40 1 16 12 2 3 5 6 4 9 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑍 ) ∈ 𝑃 )
41 1 3 4 5 6 8 9 mirleqb ⊢ ( 𝜑 → ( 𝑌 = 𝑍 ↔ ( 𝑀 ‘ 𝑌 ) = ( 𝑀 ‘ 𝑍 ) ) )
42 41 necon3bid ⊢ ( 𝜑 → ( 𝑌 ≠ 𝑍 ↔ ( 𝑀 ‘ 𝑌 ) ≠ ( 𝑀 ‘ 𝑍 ) ) )
43 13 42 mpbid ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑌 ) ≠ ( 𝑀 ‘ 𝑍 ) )
44 1 16 12 2 3 5 6 4 7 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ 𝑃 )
45 1 2 12 5 39 40 43 44 tgellng ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑍 ) ) ↔ ( ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑌 ) ( Itv ‘ 𝐺 ) ( 𝑀 ‘ 𝑍 ) ) ∨ ( 𝑀 ‘ 𝑌 ) ∈ ( ( 𝑀 ‘ 𝑋 ) ( Itv ‘ 𝐺 ) ( 𝑀 ‘ 𝑍 ) ) ∨ ( 𝑀 ‘ 𝑍 ) ∈ ( ( 𝑀 ‘ 𝑌 ) ( Itv ‘ 𝐺 ) ( 𝑀 ‘ 𝑋 ) ) ) ) )
46 38 45 mpbird ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ( ( 𝑀 ‘ 𝑌 ) 𝐿 ( 𝑀 ‘ 𝑍 ) ) )