Definition df-mir

Description: Define the point inversion ("mirror") function. Definition 7.5 of Schwabhauser p. 49. See mirval and ismir . (Contributed by Thierry Arnoux, 30-May-2019)

	Ref	Expression
Assertion	df-mir	⊢ pInvG = ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmir	⊢ pInvG
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vm	⊢ 𝑚
4		cbs	⊢ Base
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Base ‘ 𝑔 )
7		va	⊢ 𝑎
8		vb	⊢ 𝑏
9	3	cv	⊢ 𝑚
10		cds	⊢ dist
11	5 10	cfv	⊢ ( dist ‘ 𝑔 )
12	8	cv	⊢ 𝑏
13	9 12 11	co	⊢ ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 )
14	7	cv	⊢ 𝑎
15	9 14 11	co	⊢ ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 )
16	13 15	wceq	⊢ ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 )
17		citv	⊢ Itv
18	5 17	cfv	⊢ ( Itv ‘ 𝑔 )
19	12 14 18	co	⊢ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 )
20	9 19	wcel	⊢ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 )
21	16 20	wa	⊢ ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) )
22	21 8 6	crio	⊢ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) )
23	7 6 22	cmpt	⊢ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) )
24	3 6 23	cmpt	⊢ ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) )
25	1 2 24	cmpt	⊢ ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ) )
26	0 25	wceq	⊢ pInvG = ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑚 ( dist ‘ 𝑔 ) 𝑏 ) = ( 𝑚 ( dist ‘ 𝑔 ) 𝑎 ) ∧ 𝑚 ∈ ( 𝑏 ( Itv ‘ 𝑔 ) 𝑎 ) ) ) ) ) )