Theorem psrasclcl

Description: A scalar is lifted into a member of the power series. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	psrasclcl.s	|- S = ( I mPwSer R )
	psrasclcl.b	|- B = ( Base ` S )
	psrasclcl.k	|- K = ( Base ` R )
	psrasclcl.a	|- A = ( algSc ` S )
	psrasclcl.i	|- ( ph -> I e. W )
	psrasclcl.r	|- ( ph -> R e. Ring )
	psrasclcl.c	|- ( ph -> C e. K )
Assertion	psrasclcl	|- ( ph -> ( A ` C ) e. B )

Proof

Step	Hyp	Ref	Expression
1		psrasclcl.s	|- S = ( I mPwSer R )
2		psrasclcl.b	|- B = ( Base ` S )
3		psrasclcl.k	|- K = ( Base ` R )
4		psrasclcl.a	|- A = ( algSc ` S )
5		psrasclcl.i	|- ( ph -> I e. W )
6		psrasclcl.r	|- ( ph -> R e. Ring )
7		psrasclcl.c	|- ( ph -> C e. K )
8		eqid	|- ( Scalar ` S ) = ( Scalar ` S )
9	1 5 6	psrring	|- ( ph -> S e. Ring )
10	1 5 6	psrlmod	|- ( ph -> S e. LMod )
11		eqid	|- ( Base ` ( Scalar ` S ) ) = ( Base ` ( Scalar ` S ) )
12	4 8 9 10 11 2	asclf	|- ( ph -> A : ( Base ` ( Scalar ` S ) ) --> B )
13	1 5 6	psrsca	|- ( ph -> R = ( Scalar ` S ) )
14	13	fveq2d	|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` S ) ) )
15	3 14	eqtrid	|- ( ph -> K = ( Base ` ( Scalar ` S ) ) )
16	15	feq2d	|- ( ph -> ( A : K --> B <-> A : ( Base ` ( Scalar ` S ) ) --> B ) )
17	12 16	mpbird	|- ( ph -> A : K --> B )
18	17 7	ffvelcdmd	|- ( ph -> ( A ` C ) e. B )