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	|- midG = ( g e. _V |-> ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( ( pInvG ` g ) ` m ) ` a ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmid	|- midG
1		vg	|- g
2		cvv	|- _V
3		va	|- a
4		cbs	|- Base
5	1	cv	|- g
6	5 4	cfv	|- ( Base ` g )
7		vb	|- b
8		vm	|- m
9	7	cv	|- b
10		cmir	|- pInvG
11	5 10	cfv	|- ( pInvG ` g )
12	8	cv	|- m
13	12 11	cfv	|- ( ( pInvG ` g ) ` m )
14	3	cv	|- a
15	14 13	cfv	|- ( ( ( pInvG ` g ) ` m ) ` a )
16	9 15	wceq	|- b = ( ( ( pInvG ` g ) ` m ) ` a )
17	16 8 6	crio	|- ( iota_ m e. ( Base ` g ) b = ( ( ( pInvG ` g ) ` m ) ` a ) )
18	3 7 6 6 17	cmpo	|- ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( ( pInvG ` g ) ` m ) ` a ) ) )
19	1 2 18	cmpt	|- ( g e. _V |-> ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( ( pInvG ` g ) ` m ) ` a ) ) ) )
20	0 19	wceq	|- midG = ( g e. _V |-> ( a e. ( Base ` g ) , b e. ( Base ` g ) |-> ( iota_ m e. ( Base ` g ) b = ( ( ( pInvG ` g ) ` m ) ` a ) ) ) )