Metamath Proof Explorer

Theorem mvrval

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 ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion mvrval ( 𝜑 → ( 𝑉 ‘ 𝑋 ) = ( 𝑓 ∈ 𝐷 ↦ 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 1 2 3 4 5 6 mvrfval ⊢ ( 𝜑 → 𝑉 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) )
9 8 fveq1d ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) ‘ 𝑋 ) )
10 eqeq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑦 = 𝑥 ↔ 𝑦 = 𝑋 ) )
11 10 ifbid ⊢ ( 𝑥 = 𝑋 → if ( 𝑦 = 𝑥 , 1 , 0 ) = if ( 𝑦 = 𝑋 , 1 , 0 ) )
12 11 mpteq2dv ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) )
13 12 eqeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) ↔ 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) )
14 13 ifbid ⊢ ( 𝑥 = 𝑋 → if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) = if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) )
15 14 mpteq2dv ⊢ ( 𝑥 = 𝑋 → ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) = ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) )
16 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) )
17 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
18 2 17 rabex2 ⊢ 𝐷 ∈ V
19 18 mptex ⊢ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) ∈ V
20 15 16 19 fvmpt ⊢ ( 𝑋 ∈ 𝐼 → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) ‘ 𝑋 ) = ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) )
21 7 20 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , 1 , 0 ) ) ) ‘ 𝑋 ) = ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) )
22 9 21 eqtrd ⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) = ( 𝑓 ∈ 𝐷 ↦ if ( 𝑓 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) ) )