Definition df-lmi

Description: Define the line mirroring function. Definition 10.3 of Schwabhauser p. 89. See islmib . (Contributed by Thierry Arnoux, 1-Dec-2019)

	Ref	Expression
Assertion	df-lmi	⊢ lInvG = ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ran ( LineG ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑚 ∧ ( 𝑚 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmi	⊢ lInvG
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vm	⊢ 𝑚
4		clng	⊢ LineG
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( LineG ‘ 𝑔 )
7	6	crn	⊢ ran ( LineG ‘ 𝑔 )
8		va	⊢ 𝑎
9		cbs	⊢ Base
10	5 9	cfv	⊢ ( Base ‘ 𝑔 )
11		vb	⊢ 𝑏
12	8	cv	⊢ 𝑎
13		cmid	⊢ midG
14	5 13	cfv	⊢ ( midG ‘ 𝑔 )
15	11	cv	⊢ 𝑏
16	12 15 14	co	⊢ ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 )
17	3	cv	⊢ 𝑚
18	16 17	wcel	⊢ ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑚
19		cperpg	⊢ ⟂G
20	5 19	cfv	⊢ ( ⟂G ‘ 𝑔 )
21	12 15 6	co	⊢ ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 )
22	17 21 20	wbr	⊢ 𝑚 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 )
23	12 15	wceq	⊢ 𝑎 = 𝑏
24	22 23	wo	⊢ ( 𝑚 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 )
25	18 24	wa	⊢ ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑚 ∧ ( 𝑚 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) )
26	25 11 10	crio	⊢ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑚 ∧ ( 𝑚 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) )
27	8 10 26	cmpt	⊢ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑚 ∧ ( 𝑚 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) )
28	3 7 27	cmpt	⊢ ( 𝑚 ∈ ran ( LineG ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑚 ∧ ( 𝑚 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) )
29	1 2 28	cmpt	⊢ ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ran ( LineG ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑚 ∧ ( 𝑚 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) )
30	0 29	wceq	⊢ lInvG = ( 𝑔 ∈ V ↦ ( 𝑚 ∈ ran ( LineG ‘ 𝑔 ) ↦ ( 𝑎 ∈ ( Base ‘ 𝑔 ) ↦ ( ℩ 𝑏 ∈ ( Base ‘ 𝑔 ) ( ( 𝑎 ( midG ‘ 𝑔 ) 𝑏 ) ∈ 𝑚 ∧ ( 𝑚 ( ⟂G ‘ 𝑔 ) ( 𝑎 ( LineG ‘ 𝑔 ) 𝑏 ) ∨ 𝑎 = 𝑏 ) ) ) ) ) )