Metamath Proof Explorer

Theorem mpfsubrg

Description: Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 6-May-2015) (Revised by AV, 19-Sep-2021)

Ref Expression
Hypothesis mpfsubrg.q ⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
Assertion mpfsubrg ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )

Proof

Step Hyp Ref Expression
1 mpfsubrg.q ⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 eqid ⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
3 eqid ⊢ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) )
4 eqid ⊢ ( 𝑆 ↾s 𝑅 ) = ( 𝑆 ↾s 𝑅 )
5 eqid ⊢ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) = ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) )
6 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7 2 3 4 5 6 evlsrhm ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
8 eqid ⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) )
9 eqid ⊢ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) )
10 8 9 rhmf ⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
11 ffn ⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
12 fnima ⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
13 11 12 syl ⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
14 7 10 13 3syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) )
15 1 14 eqtr4id ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) )
16 4 subrgring ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑆 ↾s 𝑅 ) ∈ Ring )
17 3 mplring ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑆 ↾s 𝑅 ) ∈ Ring ) → ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ∈ Ring )
18 16 17 sylan2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ∈ Ring )
19 18 3adant2 ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ∈ Ring )
20 8 subrgid ⊢ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ∈ Ring → ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ∈ ( SubRing ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
21 19 20 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ∈ ( SubRing ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
22 rhmima ⊢ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ∧ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ∈ ( SubRing ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
23 7 21 22 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) “ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
24 15 23 eqeltrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( SubRing ‘ ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )