Theorem mvrf2

Description: The power series/polynomial variable function maps indices to polynomials. (Contributed by Stefan O'Rear, 8-Mar-2015)

	Ref	Expression
Hypotheses	mvrf2.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mvrf2.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
	mvrf2.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mvrf2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mvrf2.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	mvrf2	⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mvrf2.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mvrf2.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
3		mvrf2.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		mvrf2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		mvrf2.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
7		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
8	6 2 7 4 5	mvrf	⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
9	8	ffnd	⊢ ( 𝜑 → 𝑉 Fn 𝐼 )
10	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
11	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ Ring )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
13	1 2 3 10 11 12	mvrcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑉 ‘ 𝑥 ) ∈ 𝐵 )
14	13	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝑉 ‘ 𝑥 ) ∈ 𝐵 )
15		ffnfv	⊢ ( 𝑉 : 𝐼 ⟶ 𝐵 ↔ ( 𝑉 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑉 ‘ 𝑥 ) ∈ 𝐵 ) )
16	9 14 15	sylanbrc	⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ 𝐵 )