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 )