Metamath Proof Explorer


Theorem hspval

Description: The value of the half-space of n-dimensional Real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspval.h H=xFinix,ykxifk=i−∞y
hspval.x φXFin
hspval.i φIX
hspval.y φY
Assertion hspval φIHXY=kXifk=I−∞Y

Proof

Step Hyp Ref Expression
1 hspval.h H=xFinix,ykxifk=i−∞y
2 hspval.x φXFin
3 hspval.i φIX
4 hspval.y φY
5 id x=Xx=X
6 eqidd x=X=
7 ixpeq1 x=Xkxifk=i−∞y=kXifk=i−∞y
8 5 6 7 mpoeq123dv x=Xix,ykxifk=i−∞y=iX,ykXifk=i−∞y
9 reex V
10 9 a1i φV
11 eqid iX,ykXifk=i−∞y=iX,ykXifk=i−∞y
12 11 mpoexg XFinViX,ykXifk=i−∞yV
13 2 10 12 syl2anc φiX,ykXifk=i−∞yV
14 1 8 2 13 fvmptd3 φHX=iX,ykXifk=i−∞y
15 simpl i=Iy=Yi=I
16 15 eqeq2d i=Iy=Yk=ik=I
17 simpr i=Iy=Yy=Y
18 17 oveq2d i=Iy=Y−∞y=−∞Y
19 16 18 ifbieq1d i=Iy=Yifk=i−∞y=ifk=I−∞Y
20 19 ixpeq2dv i=Iy=YkXifk=i−∞y=kXifk=I−∞Y
21 20 adantl φi=Iy=YkXifk=i−∞y=kXifk=I−∞Y
22 ovex −∞YV
23 22 9 ifcli ifk=I−∞YV
24 23 a1i φkXifk=I−∞YV
25 24 ralrimiva φkXifk=I−∞YV
26 ixpexg kXifk=I−∞YVkXifk=I−∞YV
27 25 26 syl φkXifk=I−∞YV
28 14 21 3 4 27 ovmpod φIHXY=kXifk=I−∞Y