Metamath Proof Explorer


Theorem psrplusg

Description: The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses psrplusg.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrplusg.b 𝐵 = ( Base ‘ 𝑆 )
psrplusg.a + = ( +g𝑅 )
psrplusg.p = ( +g𝑆 )
Assertion psrplusg = ( ∘f + ↾ ( 𝐵 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 psrplusg.s 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrplusg.b 𝐵 = ( Base ‘ 𝑆 )
3 psrplusg.a + = ( +g𝑅 )
4 psrplusg.p = ( +g𝑆 )
5 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ( .r𝑅 ) = ( .r𝑅 )
7 eqid ( TopOpen ‘ 𝑅 ) = ( TopOpen ‘ 𝑅 )
8 eqid { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
9 simpl ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝐼 ∈ V )
10 1 5 8 2 9 psrbas ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ( ( Base ‘ 𝑅 ) ↑m { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ) )
11 eqid ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) = ( ∘f + ↾ ( 𝐵 × 𝐵 ) )
12 eqid ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ) = ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) )
13 eqid ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓𝐵 ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓𝐵 ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) )
14 eqidd ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) = ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) )
15 simpr ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
16 1 5 3 6 7 8 10 11 12 13 14 9 15 psrval ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑆 = ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓𝐵 ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) )
17 16 fveq2d ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( +g𝑆 ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓𝐵 ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
18 2 fvexi 𝐵 ∈ V
19 18 18 xpex ( 𝐵 × 𝐵 ) ∈ V
20 ofexg ( ( 𝐵 × 𝐵 ) ∈ V → ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ∈ V )
21 psrvalstr ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓𝐵 ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) Struct ⟨ 1 , 9 ⟩
22 plusgid +g = Slot ( +g ‘ ndx )
23 snsstp2 { ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ) ⟩ }
24 ssun1 { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓𝐵 ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } )
25 23 24 sstri { ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓𝐵 ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } )
26 21 22 25 strfv ( ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ∈ V → ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓𝐵 ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) ) )
27 19 20 26 mp2b ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) = ( +g ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑓𝐵 , 𝑔𝐵 ↦ ( 𝑘 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ↦ ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ 𝑦r𝑘 } ↦ ( ( 𝑓𝑥 ) ( .r𝑅 ) ( 𝑔 ‘ ( 𝑘f𝑥 ) ) ) ) ) ) ) ⟩ } ∪ { ⟨ ( Scalar ‘ ndx ) , 𝑅 ⟩ , ⟨ ( ·𝑠 ‘ ndx ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑓𝐵 ↦ ( ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { 𝑥 } ) ∘f ( .r𝑅 ) 𝑓 ) ) ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ∏t ‘ ( { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } × { ( TopOpen ‘ 𝑅 ) } ) ) ⟩ } ) )
28 17 4 27 3eqtr4g ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → = ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) )
29 reldmpsr Rel dom mPwSer
30 29 ovprc ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mPwSer 𝑅 ) = ∅ )
31 1 30 syl5eq ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝑆 = ∅ )
32 31 fveq2d ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( +g𝑆 ) = ( +g ‘ ∅ ) )
33 22 str0 ∅ = ( +g ‘ ∅ )
34 32 4 33 3eqtr4g ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → = ∅ )
35 31 fveq2d ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ 𝑆 ) = ( Base ‘ ∅ ) )
36 base0 ∅ = ( Base ‘ ∅ )
37 35 2 36 3eqtr4g ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ∅ )
38 37 xpeq2d ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐵 × 𝐵 ) = ( 𝐵 × ∅ ) )
39 xp0 ( 𝐵 × ∅ ) = ∅
40 38 39 eqtrdi ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐵 × 𝐵 ) = ∅ )
41 40 reseq2d ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) = ( ∘f + ↾ ∅ ) )
42 res0 ( ∘f + ↾ ∅ ) = ∅
43 41 42 eqtrdi ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) = ∅ )
44 34 43 eqtr4d ( ¬ ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → = ( ∘f + ↾ ( 𝐵 × 𝐵 ) ) )
45 28 44 pm2.61i = ( ∘f + ↾ ( 𝐵 × 𝐵 ) )