This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mvrid

Description: The X i -th coefficient of the term X i is 1 . (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 mvrid ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ‘ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) = 1 )

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 1nn0 ⊢ 1 ∈ ℕ0
9 2 snifpsrbag ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 1 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐷 )
10 5 8 9 sylancl ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐷 )
11 1 2 3 4 5 6 7 10 mvrval2 ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ‘ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) = if ( ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) )
12 eqid ⊢ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) )
13 12 iftruei ⊢ if ( ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) , 1 , 0 ) = 1
14 11 13 eqtrdi ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝑋 ) ‘ ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ) = 1 )