Theorem mvrval2

Description: Value of the generating elements of the power series structure. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypotheses	mvrfval.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
	mvrfval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	mvrfval.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mvrfval.o	⊢ 1 = ( 1r ‘ 𝑅 )
	mvrfval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mvrfval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑌 )
	mvrval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	mvrval2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
Assertion	mvrval2	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ‘ 𝐹 ) = if ( 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		mvrfval.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
2		mvrfval.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
3		mvrfval.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		mvrfval.o	⊢ 1 = ( 1r ‘ 𝑅 )
5		mvrfval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6		mvrfval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑌 )
7		mvrval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
8		mvrval2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
9	1 2 3 4 5 6 7	mvrval	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) = ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) )
10	9	fveq1d	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ‘ 𝐹 ) = ( ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) ‘ 𝐹 ) )
11		eqeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ↔ 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
12	11	ifbid	⊢ ( 𝑓 = 𝐹 → if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) = if ( 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) )
13		eqid	⊢ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) )
14	4	fvexi	⊢ 1 ∈ V
15	3	fvexi	⊢ 0 ∈ V
16	14 15	ifex	⊢ if ( 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ∈ V
17	12 13 16	fvmpt	⊢ ( 𝐹 ∈ 𝐷 → ( ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) ‘ 𝐹 ) = if ( 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) )
18	8 17	syl	⊢ ( 𝜑 → ( ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) ‘ 𝐹 ) = if ( 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) )
19	10 18	eqtrd	⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ‘ 𝐹 ) = if ( 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) )