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

Metamath Proof Explorer

Theorem 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	$⊢ P = {Poly}_{1} (R)$
	ply1scl.a	$⊢ A = algSc (P)$
	coe1scl.k	$⊢ K = {Base}_{R}$
	ply1sclf.b	$⊢ B = {Base}_{P}$
Assertion	ply1sclcl	$⊢ (R \in Ring \land S \in K) \to A (S) \in B$

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	$⊢ P = {Poly}_{1} (R)$
2		ply1scl.a	$⊢ A = algSc (P)$
3		coe1scl.k	$⊢ K = {Base}_{R}$
4		ply1sclf.b	$⊢ B = {Base}_{P}$
5	1 2 3 4	ply1sclf	$⊢ R \in Ring \to A : K ⟶ B$
6	5	ffvelcdmda	$⊢ (R \in Ring \land S \in K) \to A (S) \in B$