Metamath Proof Explorer

Definition df-mid

Description: Define the midpoint operation. Definition 10.1 of Schwabhauser p. 88. See ismidb , midbtwn , and midcgr . (Contributed by Thierry Arnoux, 9-Jun-2019)

Ref Expression
Assertion df-mid ⊢ mid 𝒢 = g ∈ V ⟼ a ∈ Base g , b ∈ Base g ⟼ ι m ∈ Base g | b = pInv 𝒢 ⁡ g ⁡ m ⁡ a

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmid class mid 𝒢
1 vg setvar g
2 cvv class V
3 va setvar a
4 cbs class Base
5 1 cv setvar g
6 5 4 cfv class Base g
7 vb setvar b
8 vm setvar m
9 7 cv setvar b
10 cmir class pInv 𝒢
11 5 10 cfv class pInv 𝒢 ⁡ g
12 8 cv setvar m
13 12 11 cfv class pInv 𝒢 ⁡ g ⁡ m
14 3 cv setvar a
15 14 13 cfv class pInv 𝒢 ⁡ g ⁡ m ⁡ a
16 9 15 wceq wff b = pInv 𝒢 ⁡ g ⁡ m ⁡ a
17 16 8 6 crio class ι m ∈ Base g | b = pInv 𝒢 ⁡ g ⁡ m ⁡ a
18 3 7 6 6 17 cmpo class a ∈ Base g , b ∈ Base g ⟼ ι m ∈ Base g | b = pInv 𝒢 ⁡ g ⁡ m ⁡ a
19 1 2 18 cmpt class g ∈ V ⟼ a ∈ Base g , b ∈ Base g ⟼ ι m ∈ Base g | b = pInv 𝒢 ⁡ g ⁡ m ⁡ a
20 0 19 wceq wff mid 𝒢 = g ∈ V ⟼ a ∈ Base g , b ∈ Base g ⟼ ι m ∈ Base g | b = pInv 𝒢 ⁡ g ⁡ m ⁡ a