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=ImPwSerR
subrgpsr.h H=R𝑠T
subrgpsr.u U=ImPwSerH
subrgpsr.b B=BaseU
Assertion subrgpsr IVTSubRingRBSubRingS

Proof

Step Hyp Ref Expression
1 subrgpsr.s S=ImPwSerR
2 subrgpsr.h H=R𝑠T
3 subrgpsr.u U=ImPwSerH
4 subrgpsr.b B=BaseU
5 simpl IVTSubRingRIV
6 subrgrcl TSubRingRRRing
7 6 adantl IVTSubRingRRRing
8 1 5 7 psrring IVTSubRingRSRing
9 2 subrgring TSubRingRHRing
10 9 adantl IVTSubRingRHRing
11 3 5 10 psrring IVTSubRingRURing
12 4 a1i IVTSubRingRB=BaseU
13 eqid S𝑠B=S𝑠B
14 simpr IVTSubRingRTSubRingR
15 1 2 3 4 13 14 resspsrbas IVTSubRingRB=BaseS𝑠B
16 1 2 3 4 13 14 resspsradd IVTSubRingRxByBx+Uy=x+S𝑠By
17 1 2 3 4 13 14 resspsrmul IVTSubRingRxByBxUy=xS𝑠By
18 12 15 16 17 ringpropd IVTSubRingRURingS𝑠BRing
19 11 18 mpbid IVTSubRingRS𝑠BRing
20 eqid BaseS=BaseS
21 13 20 ressbasss BaseS𝑠BBaseS
22 15 21 eqsstrdi IVTSubRingRBBaseS
23 eqid f0I|f-1Fin=f0I|f-1Fin
24 eqid 0R=0R
25 eqid 1R=1R
26 eqid 1S=1S
27 1 5 7 23 24 25 26 psr1 IVTSubRingR1S=xf0I|f-1Finifx=I×01R0R
28 25 subrg1cl TSubRingR1RT
29 subrgsubg TSubRingRTSubGrpR
30 24 subg0cl TSubGrpR0RT
31 29 30 syl TSubRingR0RT
32 28 31 ifcld TSubRingRifx=I×01R0RT
33 32 adantl IVTSubRingRifx=I×01R0RT
34 2 subrgbas TSubRingRT=BaseH
35 34 adantl IVTSubRingRT=BaseH
36 33 35 eleqtrd IVTSubRingRifx=I×01R0RBaseH
37 36 adantr IVTSubRingRxf0I|f-1Finifx=I×01R0RBaseH
38 27 37 fmpt3d IVTSubRingR1S:f0I|f-1FinBaseH
39 fvex BaseHV
40 ovex 0IV
41 40 rabex f0I|f-1FinV
42 39 41 elmap 1SBaseHf0I|f-1Fin1S:f0I|f-1FinBaseH
43 38 42 sylibr IVTSubRingR1SBaseHf0I|f-1Fin
44 eqid BaseH=BaseH
45 3 44 23 4 5 psrbas IVTSubRingRB=BaseHf0I|f-1Fin
46 43 45 eleqtrrd IVTSubRingR1SB
47 22 46 jca IVTSubRingRBBaseS1SB
48 20 26 issubrg BSubRingSSRingS𝑠BRingBBaseS1SB
49 8 19 47 48 syl21anbrc IVTSubRingRBSubRingS