Metamath Proof Explorer


Definition df-mir

Description: Define the point inversion ("mirror") function. Definition 7.5 of Schwabhauser p. 49. See mirval and ismir . (Contributed by Thierry Arnoux, 30-May-2019)

Ref Expression
Assertion df-mir pInvG = ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmir pInvG
1 vg 𝑔
2 cvv V
3 vm 𝑚
4 cbs Base
5 1 cv 𝑔
6 5 4 cfv ( Base ‘ 𝑔 )
7 va 𝑎
8 vb 𝑏
9 3 cv 𝑚
10 cds dist
11 5 10 cfv ( dist ‘ 𝑔 )
12 8 cv 𝑏
13 9 12 11 co ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 )
14 7 cv 𝑎
15 9 14 11 co ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 )
16 13 15 wceq ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 )
17 citv Itv
18 5 17 cfv ( Itv ‘ 𝑔 )
19 12 14 18 co ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 )
20 9 19 wcel 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 )
21 16 20 wa ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) )
22 21 8 6 crio ( 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) )
23 7 6 22 cmpt ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) )
24 3 6 23 cmpt ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) )
25 1 2 24 cmpt ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ) )
26 0 25 wceq pInvG = ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ) )