Definition df-lmi 25667

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

Assertion

Ref	Expression
df-lmi	|- lInvG = ( g e. _V |-> ( m e. ran (LineG ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a (midG ` g ) b ) e. m /\ ( m (⟂G ` g ) ( a (LineG ` g ) b ) \/ a = b ) ) ) ) ) )

Distinct variable group:   a, b, g, m

Detailed syntax breakdown of Definition df-lmi

Step	Hyp	Ref	Expression
1		clmi 25665	. 2 class lInvG
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vm	. . . 4 setvar m
5	2	cv 1482	. . . . . 6 class g
6		clng 25336	. . . . . 6 class LineG
7	5, 6	cfv 5888	. . . . 5 class (LineG ` g )
8	7	crn 5115	. . . 4 class ran (LineG ` g )
9		va	. . . . 5 setvar a
10		cbs 15857	. . . . . 6 class Base
11	5, 10	cfv 5888	. . . . 5 class ( Base ` g )
12	9	cv 1482	. . . . . . . . 9 class a
13		vb	. . . . . . . . . 10 setvar b
14	13	cv 1482	. . . . . . . . 9 class b
15		cmid 25664	. . . . . . . . . 10 class midG
16	5, 15	cfv 5888	. . . . . . . . 9 class (midG ` g )
17	12, 14, 16	co 6650	. . . . . . . 8 class ( a (midG ` g ) b )
18	4	cv 1482	. . . . . . . 8 class m
19	17, 18	wcel 1990	. . . . . . 7 wff ( a (midG ` g ) b ) e. m
20	12, 14, 7	co 6650	. . . . . . . . 9 class ( a (LineG ` g ) b )
21		cperpg 25590	. . . . . . . . . 10 class ⟂G
22	5, 21	cfv 5888	. . . . . . . . 9 class (⟂G ` g )
23	18, 20, 22	wbr 4653	. . . . . . . 8 wff m (⟂G ` g ) ( a (LineG ` g ) b )
24	9, 13	weq 1874	. . . . . . . 8 wff a = b
25	23, 24	wo 383	. . . . . . 7 wff ( m (⟂G ` g ) ( a (LineG ` g ) b ) \/ a = b )
26	19, 25	wa 384	. . . . . 6 wff ( ( a (midG ` g ) b ) e. m /\ ( m (⟂G ` g ) ( a (LineG ` g ) b ) \/ a = b ) )
27	26, 13, 11	crio 6610	. . . . 5 class ( iota_ b e. ( Base ` g ) ( ( a (midG ` g ) b ) e. m /\ ( m (⟂G ` g ) ( a (LineG ` g ) b ) \/ a = b ) ) )
28	9, 11, 27	cmpt 4729	. . . 4 class ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a (midG ` g ) b ) e. m /\ ( m (⟂G ` g ) ( a (LineG ` g ) b ) \/ a = b ) ) ) )
29	4, 8, 28	cmpt 4729	. . 3 class ( m e. ran (LineG ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a (midG ` g ) b ) e. m /\ ( m (⟂G ` g ) ( a (LineG ` g ) b ) \/ a = b ) ) ) ) )
30	2, 3, 29	cmpt 4729	. 2 class ( g e. _V |-> ( m e. ran (LineG ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a (midG ` g ) b ) e. m /\ ( m (⟂G ` g ) ( a (LineG ` g ) b ) \/ a = b ) ) ) ) ) )
31	1, 30	wceq 1483	1 wff lInvG = ( g e. _V |-> ( m e. ran (LineG ` g ) |-> ( a e. ( Base ` g ) |-> ( iota_ b e. ( Base ` g ) ( ( a (midG ` g ) b ) e. m /\ ( m (⟂G ` g ) ( a (LineG ` g ) b ) \/ a = b ) ) ) ) ) )

This definition is referenced by:  lmif  25677  islmib  25679