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 \|`s R )
	evlsscaval.k	\|- K = ( Base ` S )
	evlsscaval.b	\|- B = ( Base ` P )
	evlsscaval.a	\|- A = ( algSc ` P )
	evlsscaval.i	\|- ( ph -> I e. V )
	evlsscaval.s	\|- ( ph -> S e. CRing )
	evlsscaval.r	\|- ( ph -> R e. ( SubRing ` S ) )
	evlsscaval.x	\|- ( ph -> X e. R )
	evlsscaval.l	\|- ( ph -> L e. ( K ^m I ) )
Assertion	evlsscaval	\|- ( ph -> ( ( A ` X ) e. B /\ ( ( 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 \|`s R )
4		evlsscaval.k	\|- K = ( Base ` S )
5		evlsscaval.b	\|- B = ( Base ` P )
6		evlsscaval.a	\|- A = ( algSc ` P )
7		evlsscaval.i	\|- ( ph -> I e. V )
8		evlsscaval.s	\|- ( ph -> S e. CRing )
9		evlsscaval.r	\|- ( ph -> R e. ( SubRing ` S ) )
10		evlsscaval.x	\|- ( ph -> X e. R )
11		evlsscaval.l	\|- ( ph -> L e. ( K ^m I ) )
12		eqid	\|- ( Base ` U ) = ( Base ` U )
13	3	subrgring	\|- ( R e. ( SubRing ` S ) -> U e. Ring )
14	9 13	syl	\|- ( ph -> U e. Ring )
15	2 5 12 6 7 14	mplasclf	\|- ( ph -> A : ( Base ` U ) --> B )
16	3	subrgbas	\|- ( R e. ( SubRing ` S ) -> R = ( Base ` U ) )
17	9 16	syl	\|- ( ph -> R = ( Base ` U ) )
18	10 17	eleqtrd	\|- ( ph -> X e. ( Base ` U ) )
19	15 18	ffvelcdmd	\|- ( ph -> ( A ` X ) e. B )
20	1 2 3 4 6 7 8 9 10	evlssca	\|- ( ph -> ( Q ` ( A ` X ) ) = ( ( K ^m I ) X. { X } ) )
21	20	fveq1d	\|- ( ph -> ( ( Q ` ( A ` X ) ) ` L ) = ( ( ( K ^m I ) X. { X } ) ` L ) )
22		fvconst2g	\|- ( ( X e. R /\ L e. ( K ^m I ) ) -> ( ( ( K ^m I ) X. { X } ) ` L ) = X )
23	10 11 22	syl2anc	\|- ( ph -> ( ( ( K ^m I ) X. { X } ) ` L ) = X )
24	21 23	eqtrd	\|- ( ph -> ( ( Q ` ( A ` X ) ) ` L ) = X )
25	19 24	jca	\|- ( ph -> ( ( A ` X ) e. B /\ ( ( Q ` ( A ` X ) ) ` L ) = X ) )

Metamath Proof Explorer

Theorem evlsscaval

Proof