This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC LINEAR ALGEBRA Abstract multivariate polynomials Univariate polynomials ply1sclcl
Description: The value of the algebra scalar lifting function for (univariate)
polynomials applied to a scalar results in a constant polynomial.
(Contributed by AV , 27-Nov-2019)
Ref
Expression
Hypotheses
ply1scl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1scl.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
coe1scl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
ply1sclf.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion
ply1sclcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑆 ) ∈ 𝐵 )
Proof
Step
Hyp
Ref
Expression
1
ply1scl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2
ply1scl.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
3
coe1scl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4
ply1sclf.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
5
1 2 3 4
ply1sclf ⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐾 ⟶ 𝐵 )
6
5
ffvelcdmda ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑆 ) ∈ 𝐵 )