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 ⊢ pInv 𝒢 = g ∈ V ⟼ m ∈ Base g ⟼ a ∈ Base g ⟼ ι b ∈ Base g | m dist ⁡ g b = m dist ⁡ g a ∧ m ∈ b Itv ⁡ g a

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmir class pInv 𝒢
1 vg setvar g
2 cvv class V
3 vm setvar m
4 cbs class Base
5 1 cv setvar g
6 5 4 cfv class Base g
7 va setvar a
8 vb setvar b
9 3 cv setvar m
10 cds class dist
11 5 10 cfv class dist ⁡ g
12 8 cv setvar b
13 9 12 11 co class m dist ⁡ g b
14 7 cv setvar a
15 9 14 11 co class m dist ⁡ g a
16 13 15 wceq wff m dist ⁡ g b = m dist ⁡ g a
17 citv class Itv
18 5 17 cfv class Itv ⁡ g
19 12 14 18 co class b Itv ⁡ g a
20 9 19 wcel wff m ∈ b Itv ⁡ g a
21 16 20 wa wff m dist ⁡ g b = m dist ⁡ g a ∧ m ∈ b Itv ⁡ g a
22 21 8 6 crio class ι b ∈ Base g | m dist ⁡ g b = m dist ⁡ g a ∧ m ∈ b Itv ⁡ g a
23 7 6 22 cmpt class a ∈ Base g ⟼ ι b ∈ Base g | m dist ⁡ g b = m dist ⁡ g a ∧ m ∈ b Itv ⁡ g a
24 3 6 23 cmpt class m ∈ Base g ⟼ a ∈ Base g ⟼ ι b ∈ Base g | m dist ⁡ g b = m dist ⁡ g a ∧ m ∈ b Itv ⁡ g a
25 1 2 24 cmpt class g ∈ V ⟼ m ∈ Base g ⟼ a ∈ Base g ⟼ ι b ∈ Base g | m dist ⁡ g b = m dist ⁡ g a ∧ m ∈ b Itv ⁡ g a
26 0 25 wceq wff pInv 𝒢 = g ∈ V ⟼ m ∈ Base g ⟼ a ∈ Base g ⟼ ι b ∈ Base g | m dist ⁡ g b = m dist ⁡ g a ∧ m ∈ b Itv ⁡ g a