Metamath Proof Explorer


Theorem ressmplbas2

Description: The base set of a restricted polynomial algebra consists of power series in the subring which are also polynomials (in the parent ring). (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses ressmpl.s S = I mPoly R
ressmpl.h H = R 𝑠 T
ressmpl.u U = I mPoly H
ressmpl.b B = Base U
ressmpl.1 φ I V
ressmpl.2 φ T SubRing R
ressmplbas2.w W = I mPwSer H
ressmplbas2.c C = Base W
ressmplbas2.k K = Base S
Assertion ressmplbas2 φ B = C K

Proof

Step Hyp Ref Expression
1 ressmpl.s S = I mPoly R
2 ressmpl.h H = R 𝑠 T
3 ressmpl.u U = I mPoly H
4 ressmpl.b B = Base U
5 ressmpl.1 φ I V
6 ressmpl.2 φ T SubRing R
7 ressmplbas2.w W = I mPwSer H
8 ressmplbas2.c C = Base W
9 ressmplbas2.k K = Base S
10 eqid I mPwSer R = I mPwSer R
11 10 2 7 8 subrgpsr I V T SubRing R C SubRing I mPwSer R
12 5 6 11 syl2anc φ C SubRing I mPwSer R
13 eqid Base I mPwSer R = Base I mPwSer R
14 13 subrgss C SubRing I mPwSer R C Base I mPwSer R
15 12 14 syl φ C Base I mPwSer R
16 df-ss C Base I mPwSer R C Base I mPwSer R = C
17 15 16 sylib φ C Base I mPwSer R = C
18 eqid 0 R = 0 R
19 2 18 subrg0 T SubRing R 0 R = 0 H
20 6 19 syl φ 0 R = 0 H
21 20 breq2d φ finSupp 0 R f finSupp 0 H f
22 21 abbidv φ f | finSupp 0 R f = f | finSupp 0 H f
23 17 22 ineq12d φ C Base I mPwSer R f | finSupp 0 R f = C f | finSupp 0 H f
24 23 eqcomd φ C f | finSupp 0 H f = C Base I mPwSer R f | finSupp 0 R f
25 eqid 0 H = 0 H
26 3 7 8 25 4 mplbas B = f C | finSupp 0 H f
27 dfrab3 f C | finSupp 0 H f = C f | finSupp 0 H f
28 26 27 eqtri B = C f | finSupp 0 H f
29 1 10 13 18 9 mplbas K = f Base I mPwSer R | finSupp 0 R f
30 dfrab3 f Base I mPwSer R | finSupp 0 R f = Base I mPwSer R f | finSupp 0 R f
31 29 30 eqtri K = Base I mPwSer R f | finSupp 0 R f
32 31 ineq2i C K = C Base I mPwSer R f | finSupp 0 R f
33 inass C Base I mPwSer R f | finSupp 0 R f = C Base I mPwSer R f | finSupp 0 R f
34 32 33 eqtr4i C K = C Base I mPwSer R f | finSupp 0 R f
35 24 28 34 3eqtr4g φ B = C K