This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → I ∈ W
psrasclcl.r ⊢ φ → R ∈ Ring
psrasclcl.c ⊢ φ → C ∈ K
Assertion psrasclcl ⊢ φ → A ⁡ C ∈ 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 ⊢ φ → I ∈ W
6 psrasclcl.r ⊢ φ → R ∈ Ring
7 psrasclcl.c ⊢ φ → C ∈ K
8 eqid ⊢ Scalar ⁡ S = Scalar ⁡ S
9 1 5 6 psrring ⊢ φ → S ∈ Ring
10 1 5 6 psrlmod ⊢ φ → S ∈ LMod
11 eqid ⊢ Base Scalar ⁡ S = Base Scalar ⁡ S
12 4 8 9 10 11 2 asclf ⊢ φ → A : Base Scalar ⁡ S ⟶ B
13 1 5 6 psrsca ⊢ φ → R = Scalar ⁡ S
14 13 fveq2d ⊢ φ → Base R = Base Scalar ⁡ S
15 3 14 eqtrid ⊢ φ → K = Base Scalar ⁡ S
16 15 feq2d ⊢ φ → A : K ⟶ B ↔ A : Base Scalar ⁡ S ⟶ B
17 12 16 mpbird ⊢ φ → A : K ⟶ B
18 17 7 ffvelcdmd ⊢ φ → A ⁡ C ∈ B