Metamath Proof Explorer

Theorem subrgmpl

Description: A subring of the base ring induces a subring of polynomials. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses subrgmpl.s ⊢ S = I mPoly R
subrgmpl.h ⊢ H = R ↾ 𝑠 T
subrgmpl.u ⊢ U = I mPoly H
subrgmpl.b ⊢ B = Base U
Assertion subrgmpl ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → B ∈ SubRing ⁡ S

Proof

Step Hyp Ref Expression
1 subrgmpl.s ⊢ S = I mPoly R
2 subrgmpl.h ⊢ H = R ↾ 𝑠 T
3 subrgmpl.u ⊢ U = I mPoly H
4 subrgmpl.b ⊢ B = Base U
5 simpl ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → I ∈ V
6 simpr ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → T ∈ SubRing ⁡ R
7 eqid ⊢ I mPwSer H = I mPwSer H
8 eqid ⊢ Base I mPwSer H = Base I mPwSer H
9 eqid ⊢ Base S = Base S
10 1 2 3 4 5 6 7 8 9 ressmplbas2 ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → B = Base I mPwSer H ∩ Base S
11 eqid ⊢ I mPwSer R = I mPwSer R
12 11 2 7 8 subrgpsr ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → Base I mPwSer H ∈ SubRing ⁡ I mPwSer R
13 subrgrcl ⊢ T ∈ SubRing ⁡ R → R ∈ Ring
14 13 adantl ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → R ∈ Ring
15 11 1 9 5 14 mplsubrg ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → Base S ∈ SubRing ⁡ I mPwSer R
16 subrgin ⊢ Base I mPwSer H ∈ SubRing ⁡ I mPwSer R ∧ Base S ∈ SubRing ⁡ I mPwSer R → Base I mPwSer H ∩ Base S ∈ SubRing ⁡ I mPwSer R
17 12 15 16 syl2anc ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → Base I mPwSer H ∩ Base S ∈ SubRing ⁡ I mPwSer R
18 10 17 eqeltrd ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → B ∈ SubRing ⁡ I mPwSer R
19 inss2 ⊢ Base I mPwSer H ∩ Base S ⊆ Base S
20 10 19 eqsstrdi ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → B ⊆ Base S
21 1 11 9 mplval2 ⊢ S = I mPwSer R ↾ 𝑠 Base S
22 21 subsubrg ⊢ Base S ∈ SubRing ⁡ I mPwSer R → B ∈ SubRing ⁡ S ↔ B ∈ SubRing ⁡ I mPwSer R ∧ B ⊆ Base S
23 15 22 syl ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → B ∈ SubRing ⁡ S ↔ B ∈ SubRing ⁡ I mPwSer R ∧ B ⊆ Base S
24 18 20 23 mpbir2and ⊢ I ∈ V ∧ T ∈ SubRing ⁡ R → B ∈ SubRing ⁡ S