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 = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) , 𝑏 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmid	⊢ midG
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		va	⊢ 𝑎
4		cbs	⊢ Base
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Base ‘ 𝑔 )
7		vb	⊢ 𝑏
8		vm	⊢ 𝑚
9	7	cv	⊢ 𝑏
10		cmir	⊢ pInvG
11	5 10	cfv	⊢ ( pInvG ‘ 𝑔 )
12	8	cv	⊢ 𝑚
13	12 11	cfv	⊢ ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 )
14	3	cv	⊢ 𝑎
15	14 13	cfv	⊢ ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 )
16	9 15	wceq	⊢ 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 )
17	16 8 6	crio	⊢ ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) )
18	3 7 6 6 17	cmpo	⊢ ( 𝑎 ∈ ( Base ‘ 𝑔 ) , 𝑏 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ) )
19	1 2 18	cmpt	⊢ ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) , 𝑏 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) )
20	0 19	wceq	⊢ midG = ( 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) , 𝑏 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑚 ∈ ( Base ‘ 𝑔 ) 𝑏 = ( ( ( pInvG ‘ 𝑔 ) ‘ 𝑚 ) ‘ 𝑎 ) ) ) )