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\mathrm{mPwSer}R$$
	psrasclcl.b	$$⊢B={\mathrm{Base}}_S$$
	psrasclcl.k	$$⊢K={\mathrm{Base}}_R$$
	psrasclcl.a	$$⊢A=\mathrm{algSc}\left(S\right)$$
	psrasclcl.i	$$⊢\phi \to I\in W$$
	psrasclcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	psrasclcl.c	$$⊢\phi \to C\in K$$
Assertion	psrasclcl	$$⊢\phi \to A\left(C\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		psrasclcl.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrasclcl.b	$$⊢B={\mathrm{Base}}_S$$
3		psrasclcl.k	$$⊢K={\mathrm{Base}}_R$$
4		psrasclcl.a	$$⊢A=\mathrm{algSc}\left(S\right)$$
5		psrasclcl.i	$$⊢\phi \to I\in W$$
6		psrasclcl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		psrasclcl.c	$$⊢\phi \to C\in K$$
8		eqid	$$⊢\mathrm{Scalar}\left(S\right)=\mathrm{Scalar}\left(S\right)$$
9	1 5 6	psrring	$$⊢\phi \to S\in \mathrm{Ring}$$
10	1 5 6	psrlmod	$$⊢\phi \to S\in \mathrm{LMod}$$
11		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
12	4 8 9 10 11 2	asclf	$$⊢\phi \to A:{\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}⟶B$$
13	1 5 6	psrsca	$$⊢\phi \to R=\mathrm{Scalar}\left(S\right)$$
14	13	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
15	3 14	eqtrid	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
16	15	feq2d	$$⊢\phi \to \left(A:K⟶B\leftrightarrow A:{\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}⟶B\right)$$
17	12 16	mpbird	$$⊢\phi \to A:K⟶B$$
18	17 7	ffvelcdmd	$$⊢\phi \to A\left(C\right)\in B$$