Metamath Proof Explorer

Theorem pf1const

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

Ref Expression
Hypotheses pf1const.b 
|- B = ( Base ` R )
pf1const.q 
|- Q = ran ( eval1 ` R )
Assertion pf1const 
|- ( ( R e. CRing /\ X e. B ) -> ( B X. { X } ) e. Q )

Proof

Step Hyp Ref Expression
1 pf1const.b 
 |-  B = ( Base ` R )
2 pf1const.q 
 |-  Q = ran ( eval1 ` R )
3 eqid 
 |-  ( eval1 ` R ) = ( eval1 ` R )
4 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
5 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
6 3 4 1 5 evl1sca 
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( eval1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) = ( B X. { X } ) )
7 eqid 
 |-  ( R ^s B ) = ( R ^s B )
8 3 4 7 1 evl1rhm 
 |-  ( R e. CRing -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) )
9 8 adantr 
 |-  ( ( R e. CRing /\ X e. B ) -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) )
10 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
11 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
12 10 11 rhmf 
 |-  ( ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
13 ffn 
 |-  ( ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) -> ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) )
14 9 12 13 3syl 
 |-  ( ( R e. CRing /\ X e. B ) -> ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) )
15 crngring 
 |-  ( R e. CRing -> R e. Ring )
16 15 adantr 
 |-  ( ( R e. CRing /\ X e. B ) -> R e. Ring )
17 4 5 1 10 ply1sclf 
 |-  ( R e. Ring -> ( algSc ` ( Poly1 ` R ) ) : B --> ( Base ` ( Poly1 ` R ) ) )
18 16 17 syl 
 |-  ( ( R e. CRing /\ X e. B ) -> ( algSc ` ( Poly1 ` R ) ) : B --> ( Base ` ( Poly1 ` R ) ) )
19 ffvelrn 
 |-  ( ( ( algSc ` ( Poly1 ` R ) ) : B --> ( Base ` ( Poly1 ` R ) ) /\ X e. B ) -> ( ( algSc ` ( Poly1 ` R ) ) ` X ) e. ( Base ` ( Poly1 ` R ) ) )
20 18 19 sylancom 
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( algSc ` ( Poly1 ` R ) ) ` X ) e. ( Base ` ( Poly1 ` R ) ) )
21 fnfvelrn 
 |-  ( ( ( eval1 ` R ) Fn ( Base ` ( Poly1 ` R ) ) /\ ( ( algSc ` ( Poly1 ` R ) ) ` X ) e. ( Base ` ( Poly1 ` R ) ) ) -> ( ( eval1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) e. ran ( eval1 ` R ) )
22 14 20 21 syl2anc 
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( eval1 ` R ) ` ( ( algSc ` ( Poly1 ` R ) ) ` X ) ) e. ran ( eval1 ` R ) )
23 6 22 eqeltrrd 
 |-  ( ( R e. CRing /\ X e. B ) -> ( B X. { X } ) e. ran ( eval1 ` R ) )
24 23 2 eleqtrrdi 
 |-  ( ( R e. CRing /\ X e. B ) -> ( B X. { X } ) e. Q )