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 ⊢ 𝑆 = ( 𝐼 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 ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ 𝐵 )