Metamath Proof Explorer

Theorem pf1subrg

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

Ref Expression
Hypotheses pf1const.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
pf1const.q ⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
Assertion pf1subrg ( 𝑅 ∈ CRing → 𝑄 ∈ ( SubRing ‘ ( 𝑅 ↑s 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 pf1const.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 pf1const.q ⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
3 eqid ⊢ ( eval1 ‘ 𝑅 ) = ( eval1 ‘ 𝑅 )
4 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
5 eqid ⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
6 3 4 5 1 evl1rhm ⊢ ( 𝑅 ∈ CRing → ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) )
7 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
8 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
9 7 8 rhmf ⊢ ( ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) → ( eval1 ‘ 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
10 ffn ⊢ ( ( eval1 ‘ 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) → ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
11 fnima ⊢ ( ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) → ( ( eval1 ‘ 𝑅 ) “ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) = ran ( eval1 ‘ 𝑅 ) )
12 6 9 10 11 4syl ⊢ ( 𝑅 ∈ CRing → ( ( eval1 ‘ 𝑅 ) “ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) = ran ( eval1 ‘ 𝑅 ) )
13 12 2 eqtr4di ⊢ ( 𝑅 ∈ CRing → ( ( eval1 ‘ 𝑅 ) “ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) = 𝑄 )
14 4 ply1assa ⊢ ( 𝑅 ∈ CRing → ( Poly1 ‘ 𝑅 ) ∈ AssAlg )
15 assaring ⊢ ( ( Poly1 ‘ 𝑅 ) ∈ AssAlg → ( Poly1 ‘ 𝑅 ) ∈ Ring )
16 7 subrgid ⊢ ( ( Poly1 ‘ 𝑅 ) ∈ Ring → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∈ ( SubRing ‘ ( Poly1 ‘ 𝑅 ) ) )
17 14 15 16 3syl ⊢ ( 𝑅 ∈ CRing → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∈ ( SubRing ‘ ( Poly1 ‘ 𝑅 ) ) )
18 rhmima ⊢ ( ( ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) ∧ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∈ ( SubRing ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) “ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) ∈ ( SubRing ‘ ( 𝑅 ↑s 𝐵 ) ) )
19 6 17 18 syl2anc ⊢ ( 𝑅 ∈ CRing → ( ( eval1 ‘ 𝑅 ) “ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) ∈ ( SubRing ‘ ( 𝑅 ↑s 𝐵 ) ) )
20 13 19 eqeltrrd ⊢ ( 𝑅 ∈ CRing → 𝑄 ∈ ( SubRing ‘ ( 𝑅 ↑s 𝐵 ) ) )