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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ 𝐵 )