Description: The value of the half-space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hspval.h | |
|
hspval.x | |
||
hspval.i | |
||
hspval.y | |
||
Assertion | hspval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hspval.h | |
|
2 | hspval.x | |
|
3 | hspval.i | |
|
4 | hspval.y | |
|
5 | id | |
|
6 | eqidd | |
|
7 | ixpeq1 | |
|
8 | 5 6 7 | mpoeq123dv | |
9 | reex | |
|
10 | 9 | a1i | |
11 | eqid | |
|
12 | 11 | mpoexg | |
13 | 2 10 12 | syl2anc | |
14 | 1 8 2 13 | fvmptd3 | |
15 | simpl | |
|
16 | 15 | eqeq2d | |
17 | simpr | |
|
18 | 17 | oveq2d | |
19 | 16 18 | ifbieq1d | |
20 | 19 | ixpeq2dv | |
21 | 20 | adantl | |
22 | ovex | |
|
23 | 22 9 | ifcli | |
24 | 23 | a1i | |
25 | 24 | ralrimiva | |
26 | ixpexg | |
|
27 | 25 26 | syl | |
28 | 14 21 3 4 27 | ovmpod | |