Definition df-lmi 27136

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

Assertion

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

Distinct variable group:   𝑎,𝑏,𝑔,𝑚

Detailed syntax breakdown of Definition df-lmi

Step	Hyp	Ref	Expression
1		clmi 27134	. 2 class lInvG
2		vg	. . 3 setvar 𝑔
3		cvv 3432	. . 3 class V
4		vm	. . . 4 setvar 𝑚
5	2	cv 1538	. . . . . 6 class 𝑔
6		clng 26795	. . . . . 6 class LineG
7	5, 6	cfv 6433	. . . . 5 class (LineG‘𝑔)
8	7	crn 5590	. . . 4 class ran (LineG‘𝑔)
9		va	. . . . 5 setvar 𝑎
10		cbs 16912	. . . . . 6 class Base
11	5, 10	cfv 6433	. . . . 5 class (Base‘𝑔)
12	9	cv 1538	. . . . . . . . 9 class 𝑎
13		vb	. . . . . . . . . 10 setvar 𝑏
14	13	cv 1538	. . . . . . . . 9 class 𝑏
15		cmid 27133	. . . . . . . . . 10 class midG
16	5, 15	cfv 6433	. . . . . . . . 9 class (midG‘𝑔)
17	12, 14, 16	co 7275	. . . . . . . 8 class (𝑎(midG‘𝑔)𝑏)
18	4	cv 1538	. . . . . . . 8 class 𝑚
19	17, 18	wcel 2106	. . . . . . 7 wff (𝑎(midG‘𝑔)𝑏) ∈ 𝑚
20	12, 14, 7	co 7275	. . . . . . . . 9 class (𝑎(LineG‘𝑔)𝑏)
21		cperpg 27056	. . . . . . . . . 10 class ⟂G
22	5, 21	cfv 6433	. . . . . . . . 9 class (⟂G‘𝑔)
23	18, 20, 22	wbr 5074	. . . . . . . 8 wff 𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏)
24	9, 13	weq 1966	. . . . . . . 8 wff 𝑎 = 𝑏
25	23, 24	wo 844	. . . . . . 7 wff (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)
26	19, 25	wa 396	. . . . . 6 wff ((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))
27	26, 13, 11	crio 7231	. . . . 5 class (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))
28	9, 11, 27	cmpt 5157	. . . 4 class (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))
29	4, 8, 28	cmpt 5157	. . 3 class (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))))
30	2, 3, 29	cmpt 5157	. 2 class (𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))))
31	1, 30	wceq 1539	1 wff lInvG = (𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))))

This definition is referenced by:  lmif  27146  islmib  27148