evlsscaval

Description: Polynomial evaluation builder for a scalar. Compare evl1scad . Note that scalar multiplication by X is the same as vector multiplication by ( AX ) by asclmul1 . (Contributed by SN, 27-Jul-2024)

	Ref	Expression
Hypotheses	evlsscaval.q	$⊢ Q = (I evalSub S) (R)$
	evlsscaval.p	$⊢ P = I mPoly U$
	evlsscaval.u	$⊢ U = S ↾_{𝑠} R$
	evlsscaval.k	$⊢ K = {Base}_{S}$
	evlsscaval.b	$⊢ B = {Base}_{P}$
	evlsscaval.a	$⊢ A = algSc (P)$
	evlsscaval.i	$⊢ φ \to I \in V$
	evlsscaval.s	$⊢ φ \to S \in CRing$
	evlsscaval.r	$⊢ φ \to R \in SubRing (S)$
	evlsscaval.x	$⊢ φ \to X \in R$
	evlsscaval.l	$⊢ φ \to L \in (K^{I})$
Assertion	evlsscaval	$⊢ φ \to (A (X) \in B \land Q (A (X)) (L) = X)$

Proof

Step	Hyp	Ref	Expression
1		evlsscaval.q	$⊢ Q = (I evalSub S) (R)$
2		evlsscaval.p	$⊢ P = I mPoly U$
3		evlsscaval.u	$⊢ U = S ↾_{𝑠} R$
4		evlsscaval.k	$⊢ K = {Base}_{S}$
5		evlsscaval.b	$⊢ B = {Base}_{P}$
6		evlsscaval.a	$⊢ A = algSc (P)$
7		evlsscaval.i	$⊢ φ \to I \in V$
8		evlsscaval.s	$⊢ φ \to S \in CRing$
9		evlsscaval.r	$⊢ φ \to R \in SubRing (S)$
10		evlsscaval.x	$⊢ φ \to X \in R$
11		evlsscaval.l	$⊢ φ \to L \in (K^{I})$
12		eqid	$⊢ {Base}_{U} = {Base}_{U}$
13	3	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
14	9 13	syl	$⊢ φ \to U \in Ring$
15	2 5 12 6 7 14	mplasclf	$⊢ φ \to A : {Base}_{U} ⟶ B$
16	3	subrgbas	$⊢ R \in SubRing (S) \to R = {Base}_{U}$
17	9 16	syl	$⊢ φ \to R = {Base}_{U}$
18	10 17	eleqtrd	$⊢ φ \to X \in {Base}_{U}$
19	15 18	ffvelcdmd	$⊢ φ \to A (X) \in B$
20	1 2 3 4 6 7 8 9 10	evlssca	$⊢ φ \to Q (A (X)) = (K^{I}) \times \{X\}$
21	20	fveq1d	$⊢ φ \to Q (A (X)) (L) = ((K^{I}) \times \{X\}) (L)$
22		fvconst2g	$⊢ (X \in R \land L \in (K^{I})) \to ((K^{I}) \times \{X\}) (L) = X$
23	10 11 22	syl2anc	$⊢ φ \to ((K^{I}) \times \{X\}) (L) = X$
24	21 23	eqtrd	$⊢ φ \to Q (A (X)) (L) = X$
25	19 24	jca	$⊢ φ \to (A (X) \in B \land Q (A (X)) (L) = X)$

Metamath Proof Explorer

Theorem evlsscaval

Proof