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

Metamath Proof Explorer

Theorem mplasclf

Description: The scalar injection is a function into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Hypotheses mplasclf.p ⊢ P = I mPoly R
mplasclf.b ⊢ B = Base P
mplasclf.k ⊢ K = Base R
mplasclf.a ⊢ A = algSc ⁡ P
mplasclf.i ⊢ φ → I ∈ W
mplasclf.r ⊢ φ → R ∈ Ring
Assertion mplasclf ⊢ φ → A : K ⟶ B

Proof

Step Hyp Ref Expression
1 mplasclf.p ⊢ P = I mPoly R
2 mplasclf.b ⊢ B = Base P
3 mplasclf.k ⊢ K = Base R
4 mplasclf.a ⊢ A = algSc ⁡ P
5 mplasclf.i ⊢ φ → I ∈ W
6 mplasclf.r ⊢ φ → R ∈ Ring
7 eqid ⊢ Scalar ⁡ P = Scalar ⁡ P
8 1 mplring ⊢ I ∈ W ∧ R ∈ Ring → P ∈ Ring
9 1 mpllmod ⊢ I ∈ W ∧ R ∈ Ring → P ∈ LMod
10 eqid ⊢ Base Scalar ⁡ P = Base Scalar ⁡ P
11 4 7 8 9 10 2 asclf ⊢ I ∈ W ∧ R ∈ Ring → A : Base Scalar ⁡ P ⟶ B
12 5 6 11 syl2anc ⊢ φ → A : Base Scalar ⁡ P ⟶ B
13 1 5 6 mplsca ⊢ φ → R = Scalar ⁡ P
14 13 fveq2d ⊢ φ → Base R = Base Scalar ⁡ P
15 3 14 eqtrid ⊢ φ → K = Base Scalar ⁡ P
16 15 feq2d ⊢ φ → A : K ⟶ B ↔ A : Base Scalar ⁡ P ⟶ B
17 12 16 mpbird ⊢ φ → A : K ⟶ B