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	⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑖 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
	hspval.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	hspval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
	hspval.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
Assertion	hspval	⊢ ( 𝜑 → ( 𝐼 ( 𝐻 ‘ 𝑋 ) 𝑌 ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		hspval.h	⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑖 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
2		hspval.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		hspval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
4		hspval.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
5		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
6		eqidd	⊢ ( 𝑥 = 𝑋 → ℝ = ℝ )
7		ixpeq1	⊢ ( 𝑥 = 𝑋 → X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) )
8	5 6 7	mpoeq123dv	⊢ ( 𝑥 = 𝑋 → ( 𝑖 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑥 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) ) = ( 𝑖 ∈ 𝑋 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
9		reex	⊢ ℝ ∈ V
10	9	a1i	⊢ ( 𝜑 → ℝ ∈ V )
11		eqid	⊢ ( 𝑖 ∈ 𝑋 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) ) = ( 𝑖 ∈ 𝑋 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) )
12	11	mpoexg	⊢ ( ( 𝑋 ∈ Fin ∧ ℝ ∈ V ) → ( 𝑖 ∈ 𝑋 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) ) ∈ V )
13	2 10 12	syl2anc	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑋 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) ) ∈ V )
14	1 8 2 13	fvmptd3	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) = ( 𝑖 ∈ 𝑋 , 𝑦 ∈ ℝ ↦ X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
15		simpl	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑦 = 𝑌 ) → 𝑖 = 𝐼 )
16	15	eqeq2d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑦 = 𝑌 ) → ( 𝑘 = 𝑖 ↔ 𝑘 = 𝐼 ) )
17		simpr	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑦 = 𝑌 ) → 𝑦 = 𝑌 )
18	17	oveq2d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑦 = 𝑌 ) → ( -∞ (,) 𝑦 ) = ( -∞ (,) 𝑌 ) )
19	16 18	ifbieq1d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑦 = 𝑌 ) → if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) = if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) )
20	19	ixpeq2dv	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑦 = 𝑌 ) → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑦 = 𝑌 ) ) → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝑖 , ( -∞ (,) 𝑦 ) , ℝ ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) )
22		ovex	⊢ ( -∞ (,) 𝑌 ) ∈ V
23	22 9	ifcli	⊢ if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V
24	23	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V )
25	24	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V )
26		ixpexg	⊢ ( ∀ 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V )
27	25 26	syl	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) ∈ V )
28	14 21 3 4 27	ovmpod	⊢ ( 𝜑 → ( 𝐼 ( 𝐻 ‘ 𝑋 ) 𝑌 ) = X 𝑘 ∈ 𝑋 if ( 𝑘 = 𝐼 , ( -∞ (,) 𝑌 ) , ℝ ) )

Metamath Proof Explorer

Theorem hspval

Proof