Description: A subring of the base ring induces a subring of power series. (Contributed by Mario Carneiro, 3-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subrgpsr.s | |
|
subrgpsr.h | |
||
subrgpsr.u | |
||
subrgpsr.b | |
||
Assertion | subrgpsr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subrgpsr.s | |
|
2 | subrgpsr.h | |
|
3 | subrgpsr.u | |
|
4 | subrgpsr.b | |
|
5 | simpl | |
|
6 | subrgrcl | |
|
7 | 6 | adantl | |
8 | 1 5 7 | psrring | |
9 | 2 | subrgring | |
10 | 9 | adantl | |
11 | 3 5 10 | psrring | |
12 | 4 | a1i | |
13 | eqid | |
|
14 | simpr | |
|
15 | 1 2 3 4 13 14 | resspsrbas | |
16 | 1 2 3 4 13 14 | resspsradd | |
17 | 1 2 3 4 13 14 | resspsrmul | |
18 | 12 15 16 17 | ringpropd | |
19 | 11 18 | mpbid | |
20 | eqid | |
|
21 | 13 20 | ressbasss | |
22 | 15 21 | eqsstrdi | |
23 | eqid | |
|
24 | eqid | |
|
25 | eqid | |
|
26 | eqid | |
|
27 | 1 5 7 23 24 25 26 | psr1 | |
28 | 25 | subrg1cl | |
29 | subrgsubg | |
|
30 | 24 | subg0cl | |
31 | 29 30 | syl | |
32 | 28 31 | ifcld | |
33 | 32 | adantl | |
34 | 2 | subrgbas | |
35 | 34 | adantl | |
36 | 33 35 | eleqtrd | |
37 | 36 | adantr | |
38 | 27 37 | fmpt3d | |
39 | fvex | |
|
40 | ovex | |
|
41 | 40 | rabex | |
42 | 39 41 | elmap | |
43 | 38 42 | sylibr | |
44 | eqid | |
|
45 | 3 44 23 4 5 | psrbas | |
46 | 43 45 | eleqtrrd | |
47 | 22 46 | jca | |
48 | 20 26 | issubrg | |
49 | 8 19 47 48 | syl21anbrc | |