Definition df-lmi 25467

Description: Define the line mirroring function. Definition 10.3 of [Schwabhauser] p. 89. See islmib 25479. (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 25465	. 2 class lInvG
2		vg	. . 3 setvar 𝑔
3		cvv 3173	. . 3 class V
4		vm	. . . 4 setvar 𝑚
5	2	cv 1474	. . . . . 6 class 𝑔
6		clng 25136	. . . . . 6 class LineG
7	5, 6	cfv 5804	. . . . 5 class (LineG‘𝑔)
8	7	crn 5039	. . . 4 class ran (LineG‘𝑔)
9		va	. . . . 5 setvar 𝑎
10		cbs 15695	. . . . . 6 class Base
11	5, 10	cfv 5804	. . . . 5 class (Base‘𝑔)
12	9	cv 1474	. . . . . . . . 9 class 𝑎
13		vb	. . . . . . . . . 10 setvar 𝑏
14	13	cv 1474	. . . . . . . . 9 class 𝑏
15		cmid 25464	. . . . . . . . . 10 class midG
16	5, 15	cfv 5804	. . . . . . . . 9 class (midG‘𝑔)
17	12, 14, 16	co 6549	. . . . . . . 8 class (𝑎(midG‘𝑔)𝑏)
18	4	cv 1474	. . . . . . . 8 class 𝑚
19	17, 18	wcel 1977	. . . . . . 7 wff (𝑎(midG‘𝑔)𝑏) ∈ 𝑚
20	12, 14, 7	co 6549	. . . . . . . . 9 class (𝑎(LineG‘𝑔)𝑏)
21		cperpg 25390	. . . . . . . . . 10 class ⟂G
22	5, 21	cfv 5804	. . . . . . . . 9 class (⟂G‘𝑔)
23	18, 20, 22	wbr 4583	. . . . . . . 8 wff 𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏)
24	9, 13	weq 1861	. . . . . . . 8 wff 𝑎 = 𝑏
25	23, 24	wo 382	. . . . . . 7 wff (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)
26	19, 25	wa 383	. . . . . 6 wff ((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))
27	26, 13, 11	crio 6510	. . . . 5 class (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))
28	9, 11, 27	cmpt 4643	. . . 4 class (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))
29	4, 8, 28	cmpt 4643	. . 3 class (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏)))))
30	2, 3, 29	cmpt 4643	. 2 class (𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))))
31	1, 30	wceq 1475	1 wff lInvG = (𝑔 ∈ V ↦ (𝑚 ∈ ran (LineG‘𝑔) ↦ (𝑎 ∈ (Base‘𝑔) ↦ (℩𝑏 ∈ (Base‘𝑔)((𝑎(midG‘𝑔)𝑏) ∈ 𝑚 ∧ (𝑚(⟂G‘𝑔)(𝑎(LineG‘𝑔)𝑏) ∨ 𝑎 = 𝑏))))))

This definition is referenced by:  lmif  25477  islmib  25479