Definition df-mid 25666

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

Assertion

Ref	Expression
df-mid	|- midG = ( g e. _V |-> ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( (pInvG ` g ) ` m ) ` a ) ) ) )

Distinct variable group:   a, b, g, m

Detailed syntax breakdown of Definition df-mid

Step	Hyp	Ref	Expression
1		cmid 25664	. 2 class midG
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		va	. . . 4 setvar a
5		vb	. . . 4 setvar b
6	2	cv 1482	. . . . 5 class g
7		cbs 15857	. . . . 5 class Base
8	6, 7	cfv 5888	. . . 4 class ( Base ` g )
9	5	cv 1482	. . . . . 6 class b
10	4	cv 1482	. . . . . . 7 class a
11		vm	. . . . . . . . 9 setvar m
12	11	cv 1482	. . . . . . . 8 class m
13		cmir 25547	. . . . . . . . 9 class pInvG
14	6, 13	cfv 5888	. . . . . . . 8 class (pInvG ` g )
15	12, 14	cfv 5888	. . . . . . 7 class ( (pInvG ` g ) ` m )
16	10, 15	cfv 5888	. . . . . 6 class ( ( (pInvG ` g ) ` m ) ` a )
17	9, 16	wceq 1483	. . . . 5 wff b = ( ( (pInvG ` g ) ` m ) ` a )
18	17, 11, 8	crio 6610	. . . 4 class ( iota_ m e. ( Base ` g ) b = ( ( (pInvG ` g ) ` m ) ` a ) )
19	4, 5, 8, 8, 18	cmpt2 6652	. . 3 class ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( (pInvG ` g ) ` m ) ` a ) ) )
20	2, 3, 19	cmpt 4729	. 2 class ( g e. _V |-> ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( (pInvG ` g ) ` m ) ` a ) ) ) )
21	1, 20	wceq 1483	1 wff midG = ( g e. _V |-> ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( (pInvG ` g ) ` m ) ` a ) ) ) )

This definition is referenced by:  midf  25668  ismidb  25670