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 ∈ Fin ⟼ i ∈ x , y ∈ ℝ ⟼ ⨉ k ∈ x if k = i −∞ y ℝ
hspval.x ⊢ φ → X ∈ Fin
hspval.i ⊢ φ → I ∈ X
hspval.y ⊢ φ → Y ∈ ℝ
Assertion hspval ⊢ φ → I H ⁡ X Y = ⨉ k ∈ X if k = I −∞ Y ℝ

Proof

Step Hyp Ref Expression
1 hspval.h ⊢ H = x ∈ Fin ⟼ i ∈ x , y ∈ ℝ ⟼ ⨉ k ∈ x if k = i −∞ y ℝ
2 hspval.x ⊢ φ → X ∈ Fin
3 hspval.i ⊢ φ → I ∈ X
4 hspval.y ⊢ φ → Y ∈ ℝ
5 id ⊢ x = X → x = X
6 eqidd ⊢ x = X → ℝ = ℝ
7 ixpeq1 ⊢ x = X → ⨉ k ∈ x if k = i −∞ y ℝ = ⨉ k ∈ X if k = i −∞ y ℝ
8 5 6 7 mpoeq123dv ⊢ x = X → i ∈ x , y ∈ ℝ ⟼ ⨉ k ∈ x if k = i −∞ y ℝ = i ∈ X , y ∈ ℝ ⟼ ⨉ k ∈ X if k = i −∞ y ℝ
9 reex ⊢ ℝ ∈ V
10 9 a1i ⊢ φ → ℝ ∈ V
11 eqid ⊢ i ∈ X , y ∈ ℝ ⟼ ⨉ k ∈ X if k = i −∞ y ℝ = i ∈ X , y ∈ ℝ ⟼ ⨉ k ∈ X if k = i −∞ y ℝ
12 11 mpoexg ⊢ X ∈ Fin ∧ ℝ ∈ V → i ∈ X , y ∈ ℝ ⟼ ⨉ k ∈ X if k = i −∞ y ℝ ∈ V
13 2 10 12 syl2anc ⊢ φ → i ∈ X , y ∈ ℝ ⟼ ⨉ k ∈ X if k = i −∞ y ℝ ∈ V
14 1 8 2 13 fvmptd3 ⊢ φ → H ⁡ X = i ∈ X , y ∈ ℝ ⟼ ⨉ k ∈ X if k = i −∞ y ℝ
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 → −∞ y = −∞ Y
19 16 18 ifbieq1d ⊢ i = I ∧ y = Y → if k = i −∞ y ℝ = if k = I −∞ Y ℝ
20 19 ixpeq2dv ⊢ i = I ∧ y = Y → ⨉ k ∈ X if k = i −∞ y ℝ = ⨉ k ∈ X if k = I −∞ Y ℝ
21 20 adantl ⊢ φ ∧ i = I ∧ y = Y → ⨉ k ∈ X if k = i −∞ y ℝ = ⨉ k ∈ X if k = I −∞ Y ℝ
22 ovex ⊢ −∞ Y ∈ V
23 22 9 ifcli ⊢ if k = I −∞ Y ℝ ∈ V
24 23 a1i ⊢ φ ∧ k ∈ X → if k = I −∞ Y ℝ ∈ V
25 24 ralrimiva ⊢ φ → ∀ k ∈ X if k = I −∞ Y ℝ ∈ V
26 ixpexg ⊢ ∀ k ∈ X if k = I −∞ Y ℝ ∈ V → ⨉ k ∈ X if k = I −∞ Y ℝ ∈ V
27 25 26 syl ⊢ φ → ⨉ k ∈ X if k = I −∞ Y ℝ ∈ V
28 14 21 3 4 27 ovmpod ⊢ φ → I H ⁡ X Y = ⨉ k ∈ X if k = I −∞ Y ℝ