Theorem evls1fvcl

Description: Variant of fveval1fvcl for the subring evaluation function evalSub1 (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	evls1maprhm.q	|- O = ( R evalSub1 S )
	evls1maprhm.p	|- P = ( Poly1 ` ( R |`s S ) )
	evls1maprhm.b	|- B = ( Base ` R )
	evls1maprhm.u	|- U = ( Base ` P )
	evls1maprhm.r	|- ( ph -> R e. CRing )
	evls1maprhm.s	|- ( ph -> S e. ( SubRing ` R ) )
	evls1fvcl.1	|- ( ph -> Y e. B )
	evls1fvcl.2	|- ( ph -> M e. U )
Assertion	evls1fvcl	|- ( ph -> ( ( O ` M ) ` Y ) e. B )

Proof

Step	Hyp	Ref	Expression
1		evls1maprhm.q	|- O = ( R evalSub1 S )
2		evls1maprhm.p	|- P = ( Poly1 ` ( R |`s S ) )
3		evls1maprhm.b	|- B = ( Base ` R )
4		evls1maprhm.u	|- U = ( Base ` P )
5		evls1maprhm.r	|- ( ph -> R e. CRing )
6		evls1maprhm.s	|- ( ph -> S e. ( SubRing ` R ) )
7		evls1fvcl.1	|- ( ph -> Y e. B )
8		evls1fvcl.2	|- ( ph -> M e. U )
9		eqid	|- ( R |`s S ) = ( R |`s S )
10		eqid	|- ( eval1 ` R ) = ( eval1 ` R )
11	1 3 2 9 4 10 5 6	ressply1evl	|- ( ph -> O = ( ( eval1 ` R ) |` U ) )
12	11	fveq1d	|- ( ph -> ( O ` M ) = ( ( ( eval1 ` R ) |` U ) ` M ) )
13	8	fvresd	|- ( ph -> ( ( ( eval1 ` R ) |` U ) ` M ) = ( ( eval1 ` R ) ` M ) )
14	12 13	eqtrd	|- ( ph -> ( O ` M ) = ( ( eval1 ` R ) ` M ) )
15	14	fveq1d	|- ( ph -> ( ( O ` M ) ` Y ) = ( ( ( eval1 ` R ) ` M ) ` Y ) )
16		eqid	|- ( Poly1 ` R ) = ( Poly1 ` R )
17		eqid	|- ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
18		eqid	|- ( ( Poly1 ` R ) |`s U ) = ( ( Poly1 ` R ) |`s U )
19	16 9 2 4 6 18	ressply1bas	|- ( ph -> U = ( Base ` ( ( Poly1 ` R ) |`s U ) ) )
20	18 17	ressbasss	|- ( Base ` ( ( Poly1 ` R ) |`s U ) ) C_ ( Base ` ( Poly1 ` R ) )
21	19 20	eqsstrdi	|- ( ph -> U C_ ( Base ` ( Poly1 ` R ) ) )
22	21 8	sseldd	|- ( ph -> M e. ( Base ` ( Poly1 ` R ) ) )
23	10 16 3 17 5 7 22	fveval1fvcl	|- ( ph -> ( ( ( eval1 ` R ) ` M ) ` Y ) e. B )
24	15 23	eqeltrd	|- ( ph -> ( ( O ` M ) ` Y ) e. B )