Metamath Proof Explorer

Theorem pf1const

Description: Constants are polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pf1const.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
pf1const.q ⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
Assertion pf1const ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝐵 × { 𝑋 } ) ∈ 𝑄 )

Proof

Step Hyp Ref Expression
1 pf1const.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 pf1const.q ⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
3 eqid ⊢ ( eval1 ‘ 𝑅 ) = ( eval1 ‘ 𝑅 )
4 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
5 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
6 3 4 1 5 evl1sca ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( eval1 ‘ 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )
7 eqid ⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
8 3 4 7 1 evl1rhm ⊢ ( 𝑅 ∈ CRing → ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) )
9 8 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) )
10 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
11 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
12 10 11 rhmf ⊢ ( ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) → ( eval1 ‘ 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
13 ffn ⊢ ( ( eval1 ‘ 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) → ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
14 9 12 13 3syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
15 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
16 15 adantr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ Ring )
17 4 5 1 10 ply1sclf ⊢ ( 𝑅 ∈ Ring → ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) : 𝐵 ⟶ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
18 16 17 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) : 𝐵 ⟶ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
19 ffvelrn ⊢ ( ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) : 𝐵 ⟶ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑋 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
20 18 19 sylancom ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑋 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
21 fnfvelrn ⊢ ( ( ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑋 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑋 ) ) ∈ ran ( eval1 ‘ 𝑅 ) )
22 14 20 21 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( ( eval1 ‘ 𝑅 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑋 ) ) ∈ ran ( eval1 ‘ 𝑅 ) )
23 6 22 eqeltrrd ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝐵 × { 𝑋 } ) ∈ ran ( eval1 ‘ 𝑅 ) )
24 23 2 eleqtrrdi ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝐵 × { 𝑋 } ) ∈ 𝑄 )