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

Metamath Proof Explorer

Theorem psrascl

Description: Value of the scalar injection into the power series algebra. (Contributed by SN, 18-May-2025)

Ref Expression
Hypotheses psrascl.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrascl.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
psrascl.z ⊢ 0 = ( 0g ‘ 𝑅 )
psrascl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
psrascl.a ⊢ 𝐴 = ( algSc ‘ 𝑆 )
psrascl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psrascl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
psrascl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
Assertion psrascl ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 psrascl.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrascl.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3 psrascl.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 psrascl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
5 psrascl.a ⊢ 𝐴 = ( algSc ‘ 𝑆 )
6 psrascl.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7 psrascl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
8 psrascl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
9 1 6 7 psrsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) )
10 9 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
11 4 10 eqtrid ⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
12 8 11 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
13 eqid ⊢ ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑆 )
14 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑆 ) )
15 eqid ⊢ ( ·𝑠 ‘ 𝑆 ) = ( ·𝑠 ‘ 𝑆 )
16 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
17 5 13 14 15 16 asclval ⊢ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑆 ) ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
18 12 17 syl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) )
19 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
20 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
21 1 6 7 psrring ⊢ ( 𝜑 → 𝑆 ∈ Ring )
22 19 16 ringidcl ⊢ ( 𝑆 ∈ Ring → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
23 21 22 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
24 1 15 4 19 20 2 8 23 psrvsca ⊢ ( 𝜑 → ( 𝑋 ( ·𝑠 ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = ( ( 𝐷 × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) ( 1r ‘ 𝑆 ) ) )
25 fnconstg ⊢ ( 𝑋 ∈ 𝐾 → ( 𝐷 × { 𝑋 } ) Fn 𝐷 )
26 8 25 syl ⊢ ( 𝜑 → ( 𝐷 × { 𝑋 } ) Fn 𝐷 )
27 1 4 2 19 23 psrelbas ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) : 𝐷 ⟶ 𝐾 )
28 27 ffnd ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) Fn 𝐷 )
29 ovexd ⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V )
30 2 29 rabexd ⊢ ( 𝜑 → 𝐷 ∈ V )
31 inidm ⊢ ( 𝐷 ∩ 𝐷 ) = 𝐷
32 fvconst2g ⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐷 × { 𝑋 } ) ‘ 𝑦 ) = 𝑋 )
33 8 32 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐷 × { 𝑋 } ) ‘ 𝑦 ) = 𝑋 )
34 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
35 1 6 7 2 3 34 16 psr1 ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 1r ‘ 𝑆 ) = ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) )
37 36 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 1r ‘ 𝑆 ) ‘ 𝑦 ) = ( ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ‘ 𝑦 ) )
38 eqeq1 ⊢ ( 𝑑 = 𝑦 → ( 𝑑 = ( 𝐼 × { 0 } ) ↔ 𝑦 = ( 𝐼 × { 0 } ) ) )
39 38 ifbid ⊢ ( 𝑑 = 𝑦 → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) )
40 eqid ⊢ ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) = ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) )
41 fvex ⊢ ( 1r ‘ 𝑅 ) ∈ V
42 3 fvexi ⊢ 0 ∈ V
43 41 42 ifex ⊢ if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ∈ V
44 39 40 43 fvmpt ⊢ ( 𝑦 ∈ 𝐷 → ( ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ‘ 𝑦 ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑑 ∈ 𝐷 ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ‘ 𝑦 ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) )
46 37 45 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( 1r ‘ 𝑆 ) ‘ 𝑦 ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) )
47 26 28 30 30 31 33 46 offval ⊢ ( 𝜑 → ( ( 𝐷 × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) ( 1r ‘ 𝑆 ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) )
48 ovif2 ⊢ ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 𝑋 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) , ( 𝑋 ( .r ‘ 𝑅 ) 0 ) )
49 4 20 34 7 8 ringridmd ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑋 )
50 4 20 3 7 8 ringrzd ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) 0 ) = 0 )
51 49 50 ifeq12d ⊢ ( 𝜑 → if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 𝑋 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) , ( 𝑋 ( .r ‘ 𝑅 ) 0 ) ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) )
52 48 51 eqtrid ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) )
53 52 mpteq2dv ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ( .r ‘ 𝑅 ) if ( 𝑦 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )
54 47 53 eqtrd ⊢ ( 𝜑 → ( ( 𝐷 × { 𝑋 } ) ∘f ( .r ‘ 𝑅 ) ( 1r ‘ 𝑆 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )
55 18 24 54 3eqtrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 𝑋 , 0 ) ) )