Description: Point inversion as function. (Contributed by Thierry Arnoux, 30-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mirval.p | |
|
mirval.d | |
||
mirval.i | |
||
mirval.l | |
||
mirval.s | |
||
mirval.g | |
||
mirval.a | |
||
mirfv.m | |
||
Assertion | mirf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mirval.p | |
|
2 | mirval.d | |
|
3 | mirval.i | |
|
4 | mirval.l | |
|
5 | mirval.s | |
|
6 | mirval.g | |
|
7 | mirval.a | |
|
8 | mirfv.m | |
|
9 | riotaex | |
|
10 | 9 | a1i | |
11 | 1 2 3 4 5 6 7 | mirval | |
12 | 8 11 | eqtrid | |
13 | 6 | adantr | |
14 | 7 | adantr | |
15 | simpr | |
|
16 | 1 2 3 4 5 13 14 8 15 | mirfv | |
17 | 1 2 3 13 15 14 | mirreu3 | |
18 | riotacl | |
|
19 | 17 18 | syl | |
20 | 16 19 | eqeltrd | |
21 | 10 12 20 | fmpt2d | |