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 ⊢ P = I mPoly R
mvrf2.v ⊢ V = I mVar R
mvrf2.b ⊢ B = Base P
mvrf2.i ⊢ φ → I ∈ W
mvrf2.r ⊢ φ → R ∈ Ring
Assertion mvrf2 ⊢ φ → V : I ⟶ B

Proof

Step Hyp Ref Expression
1 mvrf2.p ⊢ P = I mPoly R
2 mvrf2.v ⊢ V = I mVar R
3 mvrf2.b ⊢ B = Base P
4 mvrf2.i ⊢ φ → I ∈ W
5 mvrf2.r ⊢ φ → R ∈ Ring
6 eqid ⊢ I mPwSer R = I mPwSer R
7 eqid ⊢ Base I mPwSer R = Base I mPwSer R
8 6 2 7 4 5 mvrf ⊢ φ → V : I ⟶ Base I mPwSer R
9 8 ffnd ⊢ φ → V Fn I
10 4 adantr ⊢ φ ∧ x ∈ I → I ∈ W
11 5 adantr ⊢ φ ∧ x ∈ I → R ∈ Ring
12 simpr ⊢ φ ∧ x ∈ I → x ∈ I
13 1 2 3 10 11 12 mvrcl ⊢ φ ∧ x ∈ I → V ⁡ x ∈ B
14 13 ralrimiva ⊢ φ → ∀ x ∈ I V ⁡ x ∈ B
15 ffnfv ⊢ V : I ⟶ B ↔ V Fn I ∧ ∀ x ∈ I V ⁡ x ∈ B
16 9 14 15 sylanbrc ⊢ φ → V : I ⟶ B