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 S = I mPwSer R
psrmulr.b B = Base S
psrmulr.m · ˙ = R
psrmulr.t ˙ = S
psrmulr.d D = h 0 I | h -1 Fin
Assertion psrmulr ˙ = f B , g B k D R x y D | y f k f x · ˙ g k f x

Proof

Step Hyp Ref Expression
1 psrmulr.s S = I mPwSer R
2 psrmulr.b B = Base S
3 psrmulr.m · ˙ = R
4 psrmulr.t ˙ = S
5 psrmulr.d D = h 0 I | h -1 Fin
6 eqid Base R = Base R
7 eqid + R = + R
8 eqid TopOpen R = TopOpen R
9 simpl I V R V I V
10 1 6 5 2 9 psrbas I V R V B = Base R D
11 eqid + S = + S
12 1 2 7 11 psrplusg + S = f + R B × B
13 eqid f B , g B k D R x y D | y f k f x · ˙ g k f x = f B , g B k D R x y D | y f k f x · ˙ g k f x
14 eqid x Base R , f B D × x · ˙ f f = x Base R , f B D × x · ˙ f f
15 eqidd I V R V 𝑡 D × TopOpen R = 𝑡 D × TopOpen R
16 simpr I V R V R V
17 1 6 7 3 8 5 10 12 13 14 15 9 16 psrval I V R V S = Base ndx B + ndx + S ndx f B , g B k D R x y D | y f k f x · ˙ g k f x Scalar ndx R ndx x Base R , f B D × x · ˙ f f TopSet ndx 𝑡 D × TopOpen R
18 17 fveq2d I V R V S = Base ndx B + ndx + S ndx f B , g B k D R x y D | y f k f x · ˙ g k f x Scalar ndx R ndx x Base R , f B D × x · ˙ f f TopSet ndx 𝑡 D × TopOpen R
19 2 fvexi B V
20 19 19 mpoex f B , g B k D R x y D | y f k f x · ˙ g k f x V
21 psrvalstr Base ndx B + ndx + S ndx f B , g B k D R x y D | y f k f x · ˙ g k f x Scalar ndx R ndx x Base R , f B D × x · ˙ f f TopSet ndx 𝑡 D × TopOpen R Struct 1 9
22 mulrid 𝑟 = Slot ndx
23 snsstp3 ndx f B , g B k D R x y D | y f k f x · ˙ g k f x Base ndx B + ndx + S ndx f B , g B k D R x y D | y f k f x · ˙ g k f x
24 ssun1 Base ndx B + ndx + S ndx f B , g B k D R x y D | y f k f x · ˙ g k f x Base ndx B + ndx + S ndx f B , g B k D R x y D | y f k f x · ˙ g k f x Scalar ndx R ndx x Base R , f B D × x · ˙ f f TopSet ndx 𝑡 D × TopOpen R
25 23 24 sstri ndx f B , g B k D R x y D | y f k f x · ˙ g k f x Base ndx B + ndx + S ndx f B , g B k D R x y D | y f k f x · ˙ g k f x Scalar ndx R ndx x Base R , f B D × x · ˙ f f TopSet ndx 𝑡 D × TopOpen R
26 21 22 25 strfv f B , g B k D R x y D | y f k f x · ˙ g k f x V f B , g B k D R x y D | y f k f x · ˙ g k f x = Base ndx B + ndx + S ndx f B , g B k D R x y D | y f k f x · ˙ g k f x Scalar ndx R ndx x Base R , f B D × x · ˙ f f TopSet ndx 𝑡 D × TopOpen R
27 20 26 ax-mp f B , g B k D R x y D | y f k f x · ˙ g k f x = Base ndx B + ndx + S ndx f B , g B k D R x y D | y f k f x · ˙ g k f x Scalar ndx R ndx x Base R , f B D × x · ˙ f f TopSet ndx 𝑡 D × TopOpen R
28 18 4 27 3eqtr4g I V R V ˙ = f B , g B k D R x y D | y f k f x · ˙ g k f x
29 22 str0 =
30 29 eqcomi =
31 reldmpsr Rel dom mPwSer
32 31 ovprc ¬ I V R V I mPwSer R =
33 1 32 syl5eq ¬ I V R V S =
34 33 fveq2d ¬ I V R V S =
35 4 34 syl5eq ¬ I V R V ˙ =
36 33 fveq2d ¬ I V R V Base S = Base
37 base0 = Base
38 36 2 37 3eqtr4g ¬ I V R V B =
39 38 olcd ¬ I V R V B = B =
40 0mpo0 B = B = f B , g B k D R x y D | y f k f x · ˙ g k f x =
41 39 40 syl ¬ I V R V f B , g B k D R x y D | y f k f x · ˙ g k f x =
42 30 35 41 3eqtr4a ¬ I V R V ˙ = f B , g B k D R x y D | y f k f x · ˙ g k f x
43 28 42 pm2.61i ˙ = f B , g B k D R x y D | y f k f x · ˙ g k f x