mvrvalind

Description: Value of the generating elements of the power series structure, expressed using the indicator function. (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Hypotheses	mvrvalind.1	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
	mvrvalind.2	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
	mvrvalind.3	⊢ 0 = ( 0_g ‘ 𝑅 )
	mvrvalind.4	⊢ 1 = ( 1_r ‘ 𝑅 )
	mvrvalind.5	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mvrvalind.6	⊢ ( 𝜑 → 𝑅 ∈ 𝑌 )
	mvrvalind.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	mvrvalind.8	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
	mvrvalind.9	⊢ 𝐴 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑋 } )
Assertion	mvrvalind	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ‘ 𝐹 ) = if ( 𝐹 = 𝐴 , 1 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		mvrvalind.1	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
2		mvrvalind.2	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
3		mvrvalind.3	⊢ 0 = ( 0_g ‘ 𝑅 )
4		mvrvalind.4	⊢ 1 = ( 1_r ‘ 𝑅 )
5		mvrvalind.5	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6		mvrvalind.6	⊢ ( 𝜑 → 𝑅 ∈ 𝑌 )
7		mvrvalind.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
8		mvrvalind.8	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
9		mvrvalind.9	⊢ 𝐴 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑋 } )
10	1 2 3 4 5 6 7 8	mvrval2	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ‘ 𝐹 ) = if ( 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) )
11	9	a1i	⊢ ( 𝜑 → 𝐴 = ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑋 } ) )
12	7	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
13		indval	⊢ ( ( 𝐼 ∈ 𝑊 ∧ { 𝑋 } ⊆ 𝐼 ) → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑋 } ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 ∈ { 𝑋 } , 1 , 0 ) ) )
14	5 12 13	syl2anc	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝐼 ) ‘ { 𝑋 } ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 ∈ { 𝑋 } , 1 , 0 ) ) )
15		velsn	⊢ ( 𝑦 ∈ { 𝑋 } ↔ 𝑦 = 𝑋 )
16	15	a1i	⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑋 } ↔ 𝑦 = 𝑋 ) )
17	16	ifbid	⊢ ( 𝜑 → if ( 𝑦 ∈ { 𝑋 } , 1 , 0 ) = if ( 𝑦 = 𝑋 , 1 , 0 ) )
18	17	mpteq2dv	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 ∈ { 𝑋 } , 1 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) )
19	11 14 18	3eqtrd	⊢ ( 𝜑 → 𝐴 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) )
20	19	eqeq2d	⊢ ( 𝜑 → ( 𝐹 = 𝐴 ↔ 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
21	20	ifbid	⊢ ( 𝜑 → if ( 𝐹 = 𝐴 , 1 , 0 ) = if ( 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) )
22	10 21	eqtr4d	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ‘ 𝐹 ) = if ( 𝐹 = 𝐴 , 1 , 0 ) )

Metamath Proof Explorer

Theorem mvrvalind

Proof