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 𝑆 = ( 𝐼 mPoly 𝑅 )
subrgmpl.h 𝐻 = ( 𝑅s 𝑇 )
subrgmpl.u 𝑈 = ( 𝐼 mPoly 𝐻 )
subrgmpl.b 𝐵 = ( Base ‘ 𝑈 )
Assertion subrgmpl ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 subrgmpl.s 𝑆 = ( 𝐼 mPoly 𝑅 )
2 subrgmpl.h 𝐻 = ( 𝑅s 𝑇 )
3 subrgmpl.u 𝑈 = ( 𝐼 mPoly 𝐻 )
4 subrgmpl.b 𝐵 = ( Base ‘ 𝑈 )
5 simpl ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐼𝑉 )
6 simpr ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
7 eqid ( 𝐼 mPwSer 𝐻 ) = ( 𝐼 mPwSer 𝐻 )
8 eqid ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝐻 ) )
9 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10 1 2 3 4 5 6 7 8 9 ressmplbas2 ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 = ( ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∩ ( Base ‘ 𝑆 ) ) )
11 eqid ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
12 11 2 7 8 subrgpsr ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
13 subrgrcl ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
14 13 adantl ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
15 11 1 9 5 14 mplsubrg ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( Base ‘ 𝑆 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
16 subrgin ( ( ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( Base ‘ 𝑆 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∩ ( Base ‘ 𝑆 ) ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
17 12 15 16 syl2anc ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∩ ( Base ‘ 𝑆 ) ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
18 10 17 eqeltrd ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
19 inss2 ( ( Base ‘ ( 𝐼 mPwSer 𝐻 ) ) ∩ ( Base ‘ 𝑆 ) ) ⊆ ( Base ‘ 𝑆 )
20 10 19 eqsstrdi ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 ⊆ ( Base ‘ 𝑆 ) )
21 1 11 9 mplval2 𝑆 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑆 ) )
22 21 subsubrg ( ( Base ‘ 𝑆 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) → ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) ↔ ( 𝐵 ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝐵 ⊆ ( Base ‘ 𝑆 ) ) ) )
23 15 22 syl ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) ↔ ( 𝐵 ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝐵 ⊆ ( Base ‘ 𝑆 ) ) ) )
24 18 20 23 mpbir2and ( ( 𝐼𝑉𝑇 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )