# 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}_{𝒢}=\left({g}\in \mathrm{V}⟼\left({a}\in {\mathrm{Base}}_{{g}},{b}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {m}\in {\mathrm{Base}}_{{g}}|{b}={pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cmid ${class}{mid}_{𝒢}$
1 vg ${setvar}{g}$
2 cvv ${class}\mathrm{V}$
3 va ${setvar}{a}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{g}$
6 5 4 cfv ${class}{\mathrm{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}_{𝒢}\left({g}\right)$
12 8 cv ${setvar}{m}$
13 12 11 cfv ${class}{pInv}_{𝒢}\left({g}\right)\left({m}\right)$
14 3 cv ${setvar}{a}$
15 14 13 cfv ${class}{pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)$
16 9 15 wceq ${wff}{b}={pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)$
17 16 8 6 crio ${class}\left(\iota {m}\in {\mathrm{Base}}_{{g}}|{b}={pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)\right)$
18 3 7 6 6 17 cmpo ${class}\left({a}\in {\mathrm{Base}}_{{g}},{b}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {m}\in {\mathrm{Base}}_{{g}}|{b}={pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)\right)\right)$
19 1 2 18 cmpt ${class}\left({g}\in \mathrm{V}⟼\left({a}\in {\mathrm{Base}}_{{g}},{b}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {m}\in {\mathrm{Base}}_{{g}}|{b}={pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)\right)\right)\right)$
20 0 19 wceq ${wff}{mid}_{𝒢}=\left({g}\in \mathrm{V}⟼\left({a}\in {\mathrm{Base}}_{{g}},{b}\in {\mathrm{Base}}_{{g}}⟼\left(\iota {m}\in {\mathrm{Base}}_{{g}}|{b}={pInv}_{𝒢}\left({g}\right)\left({m}\right)\left({a}\right)\right)\right)\right)$