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 ‘ 𝑆 ) )