Metamath Proof Explorer


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 lInv𝒢=gVmranLine𝒢gaBasegιbBaseg|amid𝒢gbmm𝒢gaLine𝒢gba=b

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmi classlInv𝒢
1 vg setvarg
2 cvv classV
3 vm setvarm
4 clng classLine𝒢
5 1 cv setvarg
6 5 4 cfv classLine𝒢g
7 6 crn classranLine𝒢g
8 va setvara
9 cbs classBase
10 5 9 cfv classBaseg
11 vb setvarb
12 8 cv setvara
13 cmid classmid𝒢
14 5 13 cfv classmid𝒢g
15 11 cv setvarb
16 12 15 14 co classamid𝒢gb
17 3 cv setvarm
18 16 17 wcel wffamid𝒢gbm
19 cperpg class𝒢
20 5 19 cfv class𝒢g
21 12 15 6 co classaLine𝒢gb
22 17 21 20 wbr wffm𝒢gaLine𝒢gb
23 12 15 wceq wffa=b
24 22 23 wo wffm𝒢gaLine𝒢gba=b
25 18 24 wa wffamid𝒢gbmm𝒢gaLine𝒢gba=b
26 25 11 10 crio classιbBaseg|amid𝒢gbmm𝒢gaLine𝒢gba=b
27 8 10 26 cmpt classaBasegιbBaseg|amid𝒢gbmm𝒢gaLine𝒢gba=b
28 3 7 27 cmpt classmranLine𝒢gaBasegιbBaseg|amid𝒢gbmm𝒢gaLine𝒢gba=b
29 1 2 28 cmpt classgVmranLine𝒢gaBasegιbBaseg|amid𝒢gbmm𝒢gaLine𝒢gba=b
30 0 29 wceq wfflInv𝒢=gVmranLine𝒢gaBasegιbBaseg|amid𝒢gbmm𝒢gaLine𝒢gba=b