Metamath Proof Explorer


Theorem resspsrmul

Description: A restricted power series algebra has the same multiplication operation. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses resspsr.s S = I mPwSer R
resspsr.h H = R 𝑠 T
resspsr.u U = I mPwSer H
resspsr.b B = Base U
resspsr.p P = S 𝑠 B
resspsr.2 φ T SubRing R
Assertion resspsrmul φ X B Y B X U Y = X P Y

Proof

Step Hyp Ref Expression
1 resspsr.s S = I mPwSer R
2 resspsr.h H = R 𝑠 T
3 resspsr.u U = I mPwSer H
4 resspsr.b B = Base U
5 resspsr.p P = S 𝑠 B
6 resspsr.2 φ T SubRing R
7 eqid f 0 I | f -1 Fin = f 0 I | f -1 Fin
8 7 psrbaglefi k f 0 I | f -1 Fin y f 0 I | f -1 Fin | y f k Fin
9 8 adantl φ X B Y B k f 0 I | f -1 Fin y f 0 I | f -1 Fin | y f k Fin
10 subrgsubg T SubRing R T SubGrp R
11 6 10 syl φ T SubGrp R
12 subgsubm T SubGrp R T SubMnd R
13 11 12 syl φ T SubMnd R
14 13 ad2antrr φ X B Y B k f 0 I | f -1 Fin T SubMnd R
15 6 ad3antrrr φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k T SubRing R
16 eqid Base H = Base H
17 simprl φ X B Y B X B
18 3 16 7 4 17 psrelbas φ X B Y B X : f 0 I | f -1 Fin Base H
19 18 adantr φ X B Y B k f 0 I | f -1 Fin X : f 0 I | f -1 Fin Base H
20 elrabi x y f 0 I | f -1 Fin | y f k x f 0 I | f -1 Fin
21 ffvelrn X : f 0 I | f -1 Fin Base H x f 0 I | f -1 Fin X x Base H
22 19 20 21 syl2an φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k X x Base H
23 2 subrgbas T SubRing R T = Base H
24 15 23 syl φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k T = Base H
25 22 24 eleqtrrd φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k X x T
26 simprr φ X B Y B Y B
27 3 16 7 4 26 psrelbas φ X B Y B Y : f 0 I | f -1 Fin Base H
28 27 ad2antrr φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k Y : f 0 I | f -1 Fin Base H
29 ssrab2 y f 0 I | f -1 Fin | y f k f 0 I | f -1 Fin
30 simplr φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k k f 0 I | f -1 Fin
31 simpr φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k x y f 0 I | f -1 Fin | y f k
32 eqid y f 0 I | f -1 Fin | y f k = y f 0 I | f -1 Fin | y f k
33 7 32 psrbagconcl k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k k f x y f 0 I | f -1 Fin | y f k
34 30 31 33 syl2anc φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k k f x y f 0 I | f -1 Fin | y f k
35 29 34 sselid φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k k f x f 0 I | f -1 Fin
36 28 35 ffvelrnd φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k Y k f x Base H
37 36 24 eleqtrrd φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k Y k f x T
38 eqid R = R
39 38 subrgmcl T SubRing R X x T Y k f x T X x R Y k f x T
40 15 25 37 39 syl3anc φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k X x R Y k f x T
41 40 fmpttd φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k X x R Y k f x : y f 0 I | f -1 Fin | y f k T
42 9 14 41 2 gsumsubm φ X B Y B k f 0 I | f -1 Fin R x y f 0 I | f -1 Fin | y f k X x R Y k f x = H x y f 0 I | f -1 Fin | y f k X x R Y k f x
43 2 38 ressmulr T SubRing R R = H
44 6 43 syl φ R = H
45 44 ad3antrrr φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k R = H
46 45 oveqd φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k X x R Y k f x = X x H Y k f x
47 46 mpteq2dva φ X B Y B k f 0 I | f -1 Fin x y f 0 I | f -1 Fin | y f k X x R Y k f x = x y f 0 I | f -1 Fin | y f k X x H Y k f x
48 47 oveq2d φ X B Y B k f 0 I | f -1 Fin H x y f 0 I | f -1 Fin | y f k X x R Y k f x = H x y f 0 I | f -1 Fin | y f k X x H Y k f x
49 42 48 eqtrd φ X B Y B k f 0 I | f -1 Fin R x y f 0 I | f -1 Fin | y f k X x R Y k f x = H x y f 0 I | f -1 Fin | y f k X x H Y k f x
50 49 mpteq2dva φ X B Y B k f 0 I | f -1 Fin R x y f 0 I | f -1 Fin | y f k X x R Y k f x = k f 0 I | f -1 Fin H x y f 0 I | f -1 Fin | y f k X x H Y k f x
51 eqid Base S = Base S
52 eqid S = S
53 fvex Base R V
54 6 23 syl φ T = Base H
55 eqid Base R = Base R
56 55 subrgss T SubRing R T Base R
57 6 56 syl φ T Base R
58 54 57 eqsstrrd φ Base H Base R
59 mapss Base R V Base H Base R Base H f 0 I | f -1 Fin Base R f 0 I | f -1 Fin
60 53 58 59 sylancr φ Base H f 0 I | f -1 Fin Base R f 0 I | f -1 Fin
61 60 adantr φ X B Y B Base H f 0 I | f -1 Fin Base R f 0 I | f -1 Fin
62 reldmpsr Rel dom mPwSer
63 62 3 4 elbasov X B I V H V
64 63 ad2antrl φ X B Y B I V H V
65 64 simpld φ X B Y B I V
66 3 16 7 4 65 psrbas φ X B Y B B = Base H f 0 I | f -1 Fin
67 1 55 7 51 65 psrbas φ X B Y B Base S = Base R f 0 I | f -1 Fin
68 61 66 67 3sstr4d φ X B Y B B Base S
69 68 17 sseldd φ X B Y B X Base S
70 68 26 sseldd φ X B Y B Y Base S
71 1 51 38 52 7 69 70 psrmulfval φ X B Y B X S Y = k f 0 I | f -1 Fin R x y f 0 I | f -1 Fin | y f k X x R Y k f x
72 eqid H = H
73 eqid U = U
74 3 4 72 73 7 17 26 psrmulfval φ X B Y B X U Y = k f 0 I | f -1 Fin H x y f 0 I | f -1 Fin | y f k X x H Y k f x
75 50 71 74 3eqtr4rd φ X B Y B X U Y = X S Y
76 4 fvexi B V
77 5 52 ressmulr B V S = P
78 76 77 mp1i φ X B Y B S = P
79 78 oveqd φ X B Y B X S Y = X P Y
80 75 79 eqtrd φ X B Y B X U Y = X P Y