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 ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplasclf.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
mplasclf.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mplasclf.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
mplasclf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mplasclf.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion mplasclf ( 𝜑 → 𝐴 : 𝐾 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 mplasclf.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplasclf.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 mplasclf.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 mplasclf.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
5 mplasclf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 mplasclf.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
8 1 mplring ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
9 1 mpllmod ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
10 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
11 4 7 8 9 10 2 asclf ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝐴 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ 𝐵 )
12 5 6 11 syl2anc ⊢ ( 𝜑 → 𝐴 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ 𝐵 )
13 1 5 6 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
14 13 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
15 3 14 eqtrid ⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
16 15 feq2d ⊢ ( 𝜑 → ( 𝐴 : 𝐾 ⟶ 𝐵 ↔ 𝐴 : ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⟶ 𝐵 ) )
17 12 16 mpbird ⊢ ( 𝜑 → 𝐴 : 𝐾 ⟶ 𝐵 )