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

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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 1 8 7 2 5 psrelbas ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
10 1 8 7 2 6 psrelbas ⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
11 7 4 9 10 rhmpsrlem2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
12 11 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
13 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
14 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
15 7 14 rabex2 ⊢ 𝐷 ∈ V
16 13 15 elmap ⊢ ( ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
17 12 16 sylibr ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
18 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
19 1 2 18 3 7 5 6 psrmulfval ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
20 reldmpsr ⊢ Rel dom mPwSer
21 20 1 2 elbasov ⊢ ( 𝑋 ∈ 𝐵 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
22 5 21 syl ⊢ ( 𝜑 → ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) )
23 22 simpld ⊢ ( 𝜑 → 𝐼 ∈ V )
24 1 8 7 2 23 psrbas ⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
25 17 19 24 3eltr4d ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )