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	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrasclcl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	psrasclcl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	psrasclcl.a	⊢ 𝐴 = ( algSc ‘ 𝑆 )
	psrasclcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	psrasclcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	psrasclcl.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion	psrasclcl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		psrasclcl.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrasclcl.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
3		psrasclcl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		psrasclcl.a	⊢ 𝐴 = ( algSc ‘ 𝑆 )
5		psrasclcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6		psrasclcl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		psrasclcl.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
8		eqid	⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
9	1 5 6	psrring	⊢ ( 𝜑 → 𝑆 ∈ Ring )
10	1 5 6	psrlmod	⊢ ( 𝜑 → 𝑆 ∈ LMod )
11		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
12	4 8 9 10 11 2	asclf	⊢ ( 𝜑 → 𝐴 : ( Base ‘ ( Scalar ‘ 𝑆 ) ) ⟶ 𝐵 )
13	1 5 6	psrsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) )
14	13	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
15	3 14	eqtrid	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
16	15	feq2d	⊢ ( 𝜑 → ( 𝐴 : 𝐾 ⟶ 𝐵 ↔ 𝐴 : ( Base ‘ ( Scalar ‘ 𝑆 ) ) ⟶ 𝐵 ) )
17	12 16	mpbird	⊢ ( 𝜑 → 𝐴 : 𝐾 ⟶ 𝐵 )
18	17 7	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ 𝐵 )