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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | clmi | |
|
1 | vg | |
|
2 | cvv | |
|
3 | vm | |
|
4 | clng | |
|
5 | 1 | cv | |
6 | 5 4 | cfv | |
7 | 6 | crn | |
8 | va | |
|
9 | cbs | |
|
10 | 5 9 | cfv | |
11 | vb | |
|
12 | 8 | cv | |
13 | cmid | |
|
14 | 5 13 | cfv | |
15 | 11 | cv | |
16 | 12 15 14 | co | |
17 | 3 | cv | |
18 | 16 17 | wcel | |
19 | cperpg | |
|
20 | 5 19 | cfv | |
21 | 12 15 6 | co | |
22 | 17 21 20 | wbr | |
23 | 12 15 | wceq | |
24 | 22 23 | wo | |
25 | 18 24 | wa | |
26 | 25 11 10 | crio | |
27 | 8 10 26 | cmpt | |
28 | 3 7 27 | cmpt | |
29 | 1 2 28 | cmpt | |
30 | 0 29 | wceq | |