Metamath Proof Explorer


Theorem psrmulcllem

Description: Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrmulcl.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrmulcl.b 𝐵 = ( Base ‘ 𝑆 )
psrmulcl.t · = ( .r𝑆 )
psrmulcl.r ( 𝜑𝑅 ∈ Ring )
psrmulcl.x ( 𝜑𝑋𝐵 )
psrmulcl.y ( 𝜑𝑌𝐵 )
psrmulcl.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
Assertion psrmulcllem ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 psrmulcl.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrmulcl.b 𝐵 = ( Base ‘ 𝑆 )
3 psrmulcl.t · = ( .r𝑆 )
4 psrmulcl.r ( 𝜑𝑅 ∈ Ring )
5 psrmulcl.x ( 𝜑𝑋𝐵 )
6 psrmulcl.y ( 𝜑𝑌𝐵 )
7 psrmulcl.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
8 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ( 0g𝑅 ) = ( 0g𝑅 )
10 4 adantr ( ( 𝜑𝑘𝐷 ) → 𝑅 ∈ Ring )
11 ringcmn ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
12 10 11 syl ( ( 𝜑𝑘𝐷 ) → 𝑅 ∈ CMnd )
13 7 psrbaglefi ( 𝑘𝐷 → { 𝑦𝐷𝑦r𝑘 } ∈ Fin )
14 13 adantl ( ( 𝜑𝑘𝐷 ) → { 𝑦𝐷𝑦r𝑘 } ∈ Fin )
15 4 ad2antrr ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → 𝑅 ∈ Ring )
16 1 8 7 2 5 psrelbas ( 𝜑𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
17 16 ad2antrr ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
18 simpr ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } )
19 breq1 ( 𝑦 = 𝑥 → ( 𝑦r𝑘𝑥r𝑘 ) )
20 19 elrab ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↔ ( 𝑥𝐷𝑥r𝑘 ) )
21 18 20 sylib ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → ( 𝑥𝐷𝑥r𝑘 ) )
22 21 simpld ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → 𝑥𝐷 )
23 17 22 ffvelrnd ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → ( 𝑋𝑥 ) ∈ ( Base ‘ 𝑅 ) )
24 1 8 7 2 6 psrelbas ( 𝜑𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
25 24 ad2antrr ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
26 simplr ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → 𝑘𝐷 )
27 7 psrbagf ( 𝑥𝐷𝑥 : 𝐼 ⟶ ℕ0 )
28 22 27 syl ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
29 21 simprd ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → 𝑥r𝑘 )
30 7 psrbagcon ( ( 𝑘𝐷𝑥 : 𝐼 ⟶ ℕ0𝑥r𝑘 ) → ( ( 𝑘f𝑥 ) ∈ 𝐷 ∧ ( 𝑘f𝑥 ) ∘r𝑘 ) )
31 26 28 29 30 syl3anc ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → ( ( 𝑘f𝑥 ) ∈ 𝐷 ∧ ( 𝑘f𝑥 ) ∘r𝑘 ) )
32 31 simpld ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → ( 𝑘f𝑥 ) ∈ 𝐷 )
33 25 32 ffvelrnd ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
34 eqid ( .r𝑅 ) = ( .r𝑅 )
35 8 34 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑋𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
36 15 23 33 35 syl3anc ( ( ( 𝜑𝑘𝐷 ) ∧ 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ) → ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
37 36 fmpttd ( ( 𝜑𝑘𝐷 ) → ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) : { 𝑦𝐷𝑦r𝑘 } ⟶ ( Base ‘ 𝑅 ) )
38 fvexd ( ( 𝜑𝑘𝐷 ) → ( 0g𝑅 ) ∈ V )
39 37 14 38 fdmfifsupp ( ( 𝜑𝑘𝐷 ) → ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) finSupp ( 0g𝑅 ) )
40 8 9 12 14 37 39 gsumcl ( ( 𝜑𝑘𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
41 40 fmpttd ( 𝜑 → ( 𝑘𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
42 fvex ( Base ‘ 𝑅 ) ∈ V
43 ovex ( ℕ0m 𝐼 ) ∈ V
44 7 43 rabex2 𝐷 ∈ V
45 42 44 elmap ( ( 𝑘𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ ( 𝑘𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
46 41 45 sylibr ( 𝜑 → ( 𝑘𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
47 1 2 34 3 7 5 6 psrmulfval ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑘𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦𝐷𝑦r𝑘 } ↦ ( ( 𝑋𝑥 ) ( .r𝑅 ) ( 𝑌 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) )
48 reldmpsr Rel dom mPwSer
49 48 1 2 elbasov ( 𝑋𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
50 5 49 syl ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
51 50 simpld ( 𝜑𝐼 ∈ V )
52 1 8 7 2 51 psrbas ( 𝜑𝐵 = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
53 46 47 52 3eltr4d ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )