Definition df-mid 27039

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

Assertion

Ref	Expression
df-mid	⊢ midG = (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))))

Distinct variable group:   𝑎,𝑏,𝑔,𝑚

Detailed syntax breakdown of Definition df-mid

Step	Hyp	Ref	Expression
1		cmid 27037	. 2 class midG
2		vg	. . 3 setvar 𝑔
3		cvv 3422	. . 3 class V
4		va	. . . 4 setvar 𝑎
5		vb	. . . 4 setvar 𝑏
6	2	cv 1538	. . . . 5 class 𝑔
7		cbs 16840	. . . . 5 class Base
8	6, 7	cfv 6418	. . . 4 class (Base‘𝑔)
9	5	cv 1538	. . . . . 6 class 𝑏
10	4	cv 1538	. . . . . . 7 class 𝑎
11		vm	. . . . . . . . 9 setvar 𝑚
12	11	cv 1538	. . . . . . . 8 class 𝑚
13		cmir 26917	. . . . . . . . 9 class pInvG
14	6, 13	cfv 6418	. . . . . . . 8 class (pInvG‘𝑔)
15	12, 14	cfv 6418	. . . . . . 7 class ((pInvG‘𝑔)‘𝑚)
16	10, 15	cfv 6418	. . . . . 6 class (((pInvG‘𝑔)‘𝑚)‘𝑎)
17	9, 16	wceq 1539	. . . . 5 wff 𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎)
18	17, 11, 8	crio 7211	. . . 4 class (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))
19	4, 5, 8, 8, 18	cmpo 7257	. . 3 class (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎)))
20	2, 3, 19	cmpt 5153	. 2 class (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))))
21	1, 20	wceq 1539	1 wff midG = (𝑔 ∈ V ↦ (𝑎 ∈ (Base‘𝑔), 𝑏 ∈ (Base‘𝑔) ↦ (℩𝑚 ∈ (Base‘𝑔)𝑏 = (((pInvG‘𝑔)‘𝑚)‘𝑎))))

This definition is referenced by:  midf  27041  ismidb  27043