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