Metamath Proof Explorer


Theorem resspsradd

Description: A restricted power series algebra has the same addition 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 resspsradd φ 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 + H = + H
8 eqid + U = + U
9 simprl φ X B Y B X B
10 simprr φ X B Y B Y B
11 3 4 7 8 9 10 psradd φ X B Y B X + U Y = X + H f Y
12 eqid Base S = Base S
13 eqid + R = + R
14 eqid + S = + S
15 fvex Base R V
16 2 subrgbas T SubRing R T = Base H
17 6 16 syl φ T = Base H
18 eqid Base R = Base R
19 18 subrgss T SubRing R T Base R
20 6 19 syl φ T Base R
21 17 20 eqsstrrd φ Base H Base R
22 mapss Base R V Base H Base R Base H f 0 I | f -1 Fin Base R f 0 I | f -1 Fin
23 15 21 22 sylancr φ Base H f 0 I | f -1 Fin Base R f 0 I | f -1 Fin
24 23 adantr φ X B Y B Base H f 0 I | f -1 Fin Base R f 0 I | f -1 Fin
25 eqid Base H = Base H
26 eqid f 0 I | f -1 Fin = f 0 I | f -1 Fin
27 reldmpsr Rel dom mPwSer
28 27 3 4 elbasov X B I V H V
29 28 ad2antrl φ X B Y B I V H V
30 29 simpld φ X B Y B I V
31 3 25 26 4 30 psrbas φ X B Y B B = Base H f 0 I | f -1 Fin
32 1 18 26 12 30 psrbas φ X B Y B Base S = Base R f 0 I | f -1 Fin
33 24 31 32 3sstr4d φ X B Y B B Base S
34 33 9 sseldd φ X B Y B X Base S
35 33 10 sseldd φ X B Y B Y Base S
36 1 12 13 14 34 35 psradd φ X B Y B X + S Y = X + R f Y
37 2 13 ressplusg T SubRing R + R = + H
38 6 37 syl φ + R = + H
39 38 adantr φ X B Y B + R = + H
40 39 ofeqd φ X B Y B f + R = f + H
41 40 oveqd φ X B Y B X + R f Y = X + H f Y
42 36 41 eqtrd φ X B Y B X + S Y = X + H f Y
43 4 fvexi B V
44 5 14 ressplusg B V + S = + P
45 43 44 mp1i φ X B Y B + S = + P
46 45 oveqd φ X B Y B X + S Y = X + P Y
47 11 42 46 3eqtr2d φ X B Y B X + U Y = X + P Y