Metamath Proof Explorer


Theorem subrgpsr

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 S = I mPwSer R
subrgpsr.h H = R 𝑠 T
subrgpsr.u U = I mPwSer H
subrgpsr.b B = Base U
Assertion subrgpsr I V T SubRing R B SubRing S

Proof

Step Hyp Ref Expression
1 subrgpsr.s S = I mPwSer R
2 subrgpsr.h H = R 𝑠 T
3 subrgpsr.u U = I mPwSer H
4 subrgpsr.b B = Base U
5 simpl I V T SubRing R I V
6 subrgrcl T SubRing R R Ring
7 6 adantl I V T SubRing R R Ring
8 1 5 7 psrring I V T SubRing R S Ring
9 2 subrgring T SubRing R H Ring
10 9 adantl I V T SubRing R H Ring
11 3 5 10 psrring I V T SubRing R U Ring
12 4 a1i I V T SubRing R B = Base U
13 eqid S 𝑠 B = S 𝑠 B
14 simpr I V T SubRing R T SubRing R
15 1 2 3 4 13 14 resspsrbas I V T SubRing R B = Base S 𝑠 B
16 1 2 3 4 13 14 resspsradd I V T SubRing R x B y B x + U y = x + S 𝑠 B y
17 1 2 3 4 13 14 resspsrmul I V T SubRing R x B y B x U y = x S 𝑠 B y
18 12 15 16 17 ringpropd I V T SubRing R U Ring S 𝑠 B Ring
19 11 18 mpbid I V T SubRing R S 𝑠 B Ring
20 eqid Base S = Base S
21 13 20 ressbasss Base S 𝑠 B Base S
22 15 21 eqsstrdi I V T SubRing R B Base S
23 eqid f 0 I | f -1 Fin = f 0 I | f -1 Fin
24 eqid 0 R = 0 R
25 eqid 1 R = 1 R
26 eqid 1 S = 1 S
27 1 5 7 23 24 25 26 psr1 I V T SubRing R 1 S = x f 0 I | f -1 Fin if x = I × 0 1 R 0 R
28 25 subrg1cl T SubRing R 1 R T
29 subrgsubg T SubRing R T SubGrp R
30 24 subg0cl T SubGrp R 0 R T
31 29 30 syl T SubRing R 0 R T
32 28 31 ifcld T SubRing R if x = I × 0 1 R 0 R T
33 32 adantl I V T SubRing R if x = I × 0 1 R 0 R T
34 2 subrgbas T SubRing R T = Base H
35 34 adantl I V T SubRing R T = Base H
36 33 35 eleqtrd I V T SubRing R if x = I × 0 1 R 0 R Base H
37 36 adantr I V T SubRing R x f 0 I | f -1 Fin if x = I × 0 1 R 0 R Base H
38 27 37 fmpt3d I V T SubRing R 1 S : f 0 I | f -1 Fin Base H
39 fvex Base H V
40 ovex 0 I V
41 40 rabex f 0 I | f -1 Fin V
42 39 41 elmap 1 S Base H f 0 I | f -1 Fin 1 S : f 0 I | f -1 Fin Base H
43 38 42 sylibr I V T SubRing R 1 S Base H f 0 I | f -1 Fin
44 eqid Base H = Base H
45 3 44 23 4 5 psrbas I V T SubRing R B = Base H f 0 I | f -1 Fin
46 43 45 eleqtrrd I V T SubRing R 1 S B
47 22 46 jca I V T SubRing R B Base S 1 S B
48 20 26 issubrg B SubRing S S Ring S 𝑠 B Ring B Base S 1 S B
49 8 19 47 48 syl21anbrc I V T SubRing R B SubRing S