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 S = I mPwSer R
psrplusg.b B = Base S
psrplusg.a + ˙ = + R
psrplusg.p ˙ = + S
Assertion psrplusg ˙ = f + ˙ B × B

Proof

Step Hyp Ref Expression
1 psrplusg.s S = I mPwSer R
2 psrplusg.b B = Base S
3 psrplusg.a + ˙ = + R
4 psrplusg.p ˙ = + S
5 eqid Base R = Base R
6 eqid R = R
7 eqid TopOpen R = TopOpen R
8 eqid h 0 I | h -1 Fin = h 0 I | h -1 Fin
9 simpl I V R V I V
10 1 5 8 2 9 psrbas I V R V B = Base R h 0 I | h -1 Fin
11 eqid f + ˙ B × B = f + ˙ B × B
12 eqid f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x = f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x
13 eqid x Base R , f B h 0 I | h -1 Fin × x R f f = x Base R , f B h 0 I | h -1 Fin × x R f f
14 eqidd I V R V 𝑡 h 0 I | h -1 Fin × TopOpen R = 𝑡 h 0 I | h -1 Fin × TopOpen R
15 simpr I V R V R V
16 1 5 3 6 7 8 10 11 12 13 14 9 15 psrval I V R V S = Base ndx B + ndx f + ˙ B × B ndx f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x Scalar ndx R ndx x Base R , f B h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
17 16 fveq2d I V R V + S = + Base ndx B + ndx f + ˙ B × B ndx f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x Scalar ndx R ndx x Base R , f B h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
18 2 fvexi B V
19 18 18 xpex B × B V
20 ofexg B × B V f + ˙ B × B V
21 psrvalstr Base ndx B + ndx f + ˙ B × B ndx f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x Scalar ndx R ndx x Base R , f B h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R Struct 1 9
22 plusgid + 𝑔 = Slot + ndx
23 snsstp2 + ndx f + ˙ B × B Base ndx B + ndx f + ˙ B × B ndx f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x
24 ssun1 Base ndx B + ndx f + ˙ B × B ndx f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x Base ndx B + ndx f + ˙ B × B ndx f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x Scalar ndx R ndx x Base R , f B h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
25 23 24 sstri + ndx f + ˙ B × B Base ndx B + ndx f + ˙ B × B ndx f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x Scalar ndx R ndx x Base R , f B h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
26 21 22 25 strfv f + ˙ B × B V f + ˙ B × B = + Base ndx B + ndx f + ˙ B × B ndx f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x Scalar ndx R ndx x Base R , f B h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
27 19 20 26 mp2b f + ˙ B × B = + Base ndx B + ndx f + ˙ B × B ndx f B , g B k h 0 I | h -1 Fin R x y h 0 I | h -1 Fin | y f k f x R g k f x Scalar ndx R ndx x Base R , f B h 0 I | h -1 Fin × x R f f TopSet ndx 𝑡 h 0 I | h -1 Fin × TopOpen R
28 17 4 27 3eqtr4g I V R V ˙ = f + ˙ B × B
29 reldmpsr Rel dom mPwSer
30 29 ovprc ¬ I V R V I mPwSer R =
31 1 30 syl5eq ¬ I V R V S =
32 31 fveq2d ¬ I V R V + S = +
33 22 str0 = +
34 32 4 33 3eqtr4g ¬ I V R V ˙ =
35 31 fveq2d ¬ I V R V Base S = Base
36 base0 = Base
37 35 2 36 3eqtr4g ¬ I V R V B =
38 37 xpeq2d ¬ I V R V B × B = B ×
39 xp0 B × =
40 38 39 syl6eq ¬ I V R V B × B =
41 40 reseq2d ¬ I V R V f + ˙ B × B = f + ˙
42 res0 f + ˙ =
43 41 42 syl6eq ¬ I V R V f + ˙ B × B =
44 34 43 eqtr4d ¬ I V R V ˙ = f + ˙ B × B
45 28 44 pm2.61i ˙ = f + ˙ B × B