Metamath Proof Explorer

Theorem psrmulr

Description: The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses psrmulr.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrmulr.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psrmulr.m ⊢ · = ( .r ‘ 𝑅 )
psrmulr.t ⊢ ∙ = ( .r ‘ 𝑆 )
psrmulr.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
Assertion psrmulr ∙ = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psrmulr.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrmulr.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psrmulr.m ⊢ · = ( .r ‘ 𝑅 )
4 psrmulr.t ⊢ ∙ = ( .r ‘ 𝑆 )
5 psrmulr.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
8 eqid ⊢ ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
9 simpl ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝐼 ∈ V )
10 1 6 5 2 9 psrbas ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
11 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
12 1 2 7 11 psrplusg ⊢ ( +g ‘ 𝑆 ) = ( ∘f ( +g ‘ 𝑅 ) ↾ ( 𝐵 × 𝐵 ) )
13 eqid ⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )
14 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) )
15 eqidd ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) = ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) )
16 simpr ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
17 1 6 7 3 8 5 10 12 13 14 15 9 16 psrval ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑆 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) )
18 17 fveq2d ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( .r ‘ 𝑆 ) = ( .r ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
19 2 fvexi ⊢ 𝐵 ∈ V
20 19 19 mpoex ⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ∈ V
21 psrvalstr ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) Struct ⟨ 1 , 9 ⟩
22 mulrid ⊢ .r = Slot ( .r ‘ ndx )
23 snsstp3 ⊢ { ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ }
24 ssun1 ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } )
25 23 24 sstri ⊢ { ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } )
26 21 22 25 strfv ⊢ ( ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ∈ V → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = ( .r ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
27 20 26 ax-mp ⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = ( .r ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑆 ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓 ∈ 𝐵 ↦ ( ( 𝐷 × { 𝑥 } ) ∘f · 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( 𝐷 × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) )
28 18 4 27 3eqtr4g ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ∙ = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
29 22 str0 ⊢ ∅ = ( .r ‘ ∅ )
30 29 eqcomi ⊢ ( .r ‘ ∅ ) = ∅
31 reldmpsr ⊢ Rel dom mPwSer
32 31 ovprc ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPwSer 𝑅 ) = ∅ )
33 1 32 eqtrid ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑆 = ∅ )
34 33 fveq2d ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( .r ‘ 𝑆 ) = ( .r ‘ ∅ ) )
35 4 34 eqtrid ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ∙ = ( .r ‘ ∅ ) )
36 33 fveq2d ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ 𝑆 ) = ( Base ‘ ∅ ) )
37 base0 ⊢ ∅ = ( Base ‘ ∅ )
38 36 2 37 3eqtr4g ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ∅ )
39 38 olcd ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) )
40 0mpo0 ⊢ ( ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = ∅ )
41 39 40 syl ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) = ∅ )
42 30 35 41 3eqtr4a ⊢ ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ∙ = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) ) )
43 28 42 pm2.61i ⊢ ∙ = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑓 ‘ 𝑥 ) · ( 𝑔 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) ) )