Metamath Proof Explorer

Theorem nhpmirhp

Description: If a point Z is on the plane defined by a line A and a point Y , but not on the same half-plane as Y , then its mirror point ( MZ ) by a point X on A is on the same half-plane as Y . (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses nhpmirhp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
nhpmirhp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
nhpmirhp.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
nhpmirhp.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
nhpmirhp.m ⊢ 𝑀 = ( 𝑆 ‘ 𝑋 )
nhpmirhp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
nhpmirhp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
nhpmirhp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
nhpmirhp.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ 𝐴 ) )
nhpmirhp.z ⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝐴 𝐸 𝑌 ) ∖ 𝐴 ) )
nhpmirhp.1 ⊢ ( 𝜑 → ¬ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑍 )
Assertion nhpmirhp ( 𝜑 → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) ( 𝑀 ‘ 𝑍 ) )

Proof

Step Hyp Ref Expression
1 nhpmirhp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 nhpmirhp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 nhpmirhp.s ⊢ 𝑆 = ( pInvG ‘ 𝐺 )
4 nhpmirhp.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
5 nhpmirhp.m ⊢ 𝑀 = ( 𝑆 ‘ 𝑋 )
6 nhpmirhp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 nhpmirhp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
8 nhpmirhp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
9 nhpmirhp.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑃 ∖ 𝐴 ) )
10 nhpmirhp.z ⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝐴 𝐸 𝑌 ) ∖ 𝐴 ) )
11 nhpmirhp.1 ⊢ ( 𝜑 → ¬ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑍 )
12 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
13 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
14 eleq1w ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ↔ 𝑧 ∈ ( 𝑃 ∖ 𝐴 ) ) )
15 eleq1w ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ↔ 𝑤 ∈ ( 𝑃 ∖ 𝐴 ) ) )
16 14 15 bi2anan9 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ↔ ( 𝑧 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑤 ∈ ( 𝑃 ∖ 𝐴 ) ) ) )
17 oveq12 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) = ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) )
18 17 eleq2d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ 𝑠 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) )
19 18 rexbidv ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) )
20 eleq1w ⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ↔ 𝑡 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) )
21 20 cbvrexvw ⊢ ( ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ↔ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) )
22 19 21 bitrdi ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ↔ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) )
23 16 22 anbi12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) ↔ ( ( 𝑧 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑤 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) ) )
24 23 cbvopabv ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑤 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑡 ∈ 𝐴 𝑡 ∈ ( 𝑧 ( Itv ‘ 𝐺 ) 𝑤 ) ) }
25 10 eldifad ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐴 𝐸 𝑌 ) )
26 1 13 2 4 6 7 9 25 plngssp ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
27 1 2 13 6 7 8 tglnpt ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
28 1 12 13 2 3 6 27 5 26 mircl ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑍 ) ∈ 𝑃 )
29 10 eldifbd ⊢ ( 𝜑 → ¬ 𝑍 ∈ 𝐴 )
30 26 29 eldifd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑃 ∖ 𝐴 ) )
31 1 13 3 5 24 6 7 8 30 2 oppmir ⊢ ( 𝜑 → 𝑍 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) } ( 𝑀 ‘ 𝑍 ) )
32 1 12 13 24 2 7 6 26 28 31 oppcom ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑍 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) } 𝑍 )
33 9 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
34 6 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ) → 𝐺 ∈ TarskiG )
35 7 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ) → 𝐴 ∈ ran 𝐿 )
36 26 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ) → 𝑍 ∈ 𝑃 )
37 33 adantr ⊢ ( ( 𝜑 ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ) → 𝑌 ∈ 𝑃 )
38 simpr ⊢ ( ( 𝜑 ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ) → 𝑍 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 )
39 1 13 2 34 35 36 24 37 38 hpgcom ⊢ ( ( 𝜑 ∧ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ) → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑍 )
40 11 39 mtand ⊢ ( 𝜑 → ¬ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 )
41 1 13 2 4 6 7 9 24 26 elplng ⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝐴 𝐸 𝑌 ) ↔ ( 𝑍 ∈ 𝐴 ∨ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ∨ 𝑍 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) } 𝑌 ) ) )
42 25 41 mpbid ⊢ ( 𝜑 → ( 𝑍 ∈ 𝐴 ∨ 𝑍 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑌 ∨ 𝑍 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) } 𝑌 ) )
43 29 40 42 ecase33d ⊢ ( 𝜑 → 𝑍 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) } 𝑌 )
44 1 12 13 24 2 7 6 26 33 43 oppcom ⊢ ( 𝜑 → 𝑌 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) } 𝑍 )
45 1 13 2 24 6 7 33 28 26 44 lnopp2hpgb ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑍 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) } 𝑍 ↔ 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) ( 𝑀 ‘ 𝑍 ) ) )
46 32 45 mpbid ⊢ ( 𝜑 → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) ( 𝑀 ‘ 𝑍 ) )