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