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 = ( x e. Fin |-> ( i e. x , y e. RR |-> X_ k e. x if ( k = i , ( -oo (,) y ) , RR ) ) )
hspval.x 
|- ( ph -> X e. Fin )
hspval.i 
|- ( ph -> I e. X )
hspval.y 
|- ( ph -> Y e. RR )
Assertion hspval 
|- ( ph -> ( I ( H ` X ) Y ) = X_ k e. X if ( k = I , ( -oo (,) Y ) , RR ) )

Proof

Step Hyp Ref Expression
1 hspval.h 
 |-  H = ( x e. Fin |-> ( i e. x , y e. RR |-> X_ k e. x if ( k = i , ( -oo (,) y ) , RR ) ) )
2 hspval.x 
 |-  ( ph -> X e. Fin )
3 hspval.i 
 |-  ( ph -> I e. X )
4 hspval.y 
 |-  ( ph -> Y e. RR )
5 id 
 |-  ( x = X -> x = X )
6 eqidd 
 |-  ( x = X -> RR = RR )
7 ixpeq1 
 |-  ( x = X -> X_ k e. x if ( k = i , ( -oo (,) y ) , RR ) = X_ k e. X if ( k = i , ( -oo (,) y ) , RR ) )
8 5 6 7 mpoeq123dv 
 |-  ( x = X -> ( i e. x , y e. RR |-> X_ k e. x if ( k = i , ( -oo (,) y ) , RR ) ) = ( i e. X , y e. RR |-> X_ k e. X if ( k = i , ( -oo (,) y ) , RR ) ) )
9 reex 
 |-  RR e. _V
10 9 a1i 
 |-  ( ph -> RR e. _V )
11 eqid 
 |-  ( i e. X , y e. RR |-> X_ k e. X if ( k = i , ( -oo (,) y ) , RR ) ) = ( i e. X , y e. RR |-> X_ k e. X if ( k = i , ( -oo (,) y ) , RR ) )
12 11 mpoexg 
 |-  ( ( X e. Fin /\ RR e. _V ) -> ( i e. X , y e. RR |-> X_ k e. X if ( k = i , ( -oo (,) y ) , RR ) ) e. _V )
13 2 10 12 syl2anc 
 |-  ( ph -> ( i e. X , y e. RR |-> X_ k e. X if ( k = i , ( -oo (,) y ) , RR ) ) e. _V )
14 1 8 2 13 fvmptd3 
 |-  ( ph -> ( H ` X ) = ( i e. X , y e. RR |-> X_ k e. X if ( k = i , ( -oo (,) y ) , RR ) ) )
15 simpl 
 |-  ( ( i = I /\ y = Y ) -> i = I )
16 15 eqeq2d 
 |-  ( ( i = I /\ y = Y ) -> ( k = i <-> k = I ) )
17 simpr 
 |-  ( ( i = I /\ y = Y ) -> y = Y )
18 17 oveq2d 
 |-  ( ( i = I /\ y = Y ) -> ( -oo (,) y ) = ( -oo (,) Y ) )
19 16 18 ifbieq1d 
 |-  ( ( i = I /\ y = Y ) -> if ( k = i , ( -oo (,) y ) , RR ) = if ( k = I , ( -oo (,) Y ) , RR ) )
20 19 ixpeq2dv 
 |-  ( ( i = I /\ y = Y ) -> X_ k e. X if ( k = i , ( -oo (,) y ) , RR ) = X_ k e. X if ( k = I , ( -oo (,) Y ) , RR ) )
21 20 adantl 
 |-  ( ( ph /\ ( i = I /\ y = Y ) ) -> X_ k e. X if ( k = i , ( -oo (,) y ) , RR ) = X_ k e. X if ( k = I , ( -oo (,) Y ) , RR ) )
22 ovex 
 |-  ( -oo (,) Y ) e. _V
23 22 9 ifcli 
 |-  if ( k = I , ( -oo (,) Y ) , RR ) e. _V
24 23 a1i 
 |-  ( ( ph /\ k e. X ) -> if ( k = I , ( -oo (,) Y ) , RR ) e. _V )
25 24 ralrimiva 
 |-  ( ph -> A. k e. X if ( k = I , ( -oo (,) Y ) , RR ) e. _V )
26 ixpexg 
 |-  ( A. k e. X if ( k = I , ( -oo (,) Y ) , RR ) e. _V -> X_ k e. X if ( k = I , ( -oo (,) Y ) , RR ) e. _V )
27 25 26 syl 
 |-  ( ph -> X_ k e. X if ( k = I , ( -oo (,) Y ) , RR ) e. _V )
28 14 21 3 4 27 ovmpod 
 |-  ( ph -> ( I ( H ` X ) Y ) = X_ k e. X if ( k = I , ( -oo (,) Y ) , RR ) )