Metamath Proof Explorer


Theorem plyconst

Description: A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion plyconst
|- ( ( S C_ CC /\ A e. S ) -> ( CC X. { A } ) e. ( Poly ` S ) )

Proof

Step Hyp Ref Expression
1 exp0
 |-  ( z e. CC -> ( z ^ 0 ) = 1 )
2 1 adantl
 |-  ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( z ^ 0 ) = 1 )
3 2 oveq2d
 |-  ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( A x. ( z ^ 0 ) ) = ( A x. 1 ) )
4 ssel2
 |-  ( ( S C_ CC /\ A e. S ) -> A e. CC )
5 4 adantr
 |-  ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> A e. CC )
6 5 mulid1d
 |-  ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( A x. 1 ) = A )
7 3 6 eqtrd
 |-  ( ( ( S C_ CC /\ A e. S ) /\ z e. CC ) -> ( A x. ( z ^ 0 ) ) = A )
8 7 mpteq2dva
 |-  ( ( S C_ CC /\ A e. S ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) = ( z e. CC |-> A ) )
9 fconstmpt
 |-  ( CC X. { A } ) = ( z e. CC |-> A )
10 8 9 eqtr4di
 |-  ( ( S C_ CC /\ A e. S ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) = ( CC X. { A } ) )
11 0nn0
 |-  0 e. NN0
12 eqid
 |-  ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) = ( z e. CC |-> ( A x. ( z ^ 0 ) ) )
13 12 ply1term
 |-  ( ( S C_ CC /\ A e. S /\ 0 e. NN0 ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) e. ( Poly ` S ) )
14 11 13 mp3an3
 |-  ( ( S C_ CC /\ A e. S ) -> ( z e. CC |-> ( A x. ( z ^ 0 ) ) ) e. ( Poly ` S ) )
15 10 14 eqeltrrd
 |-  ( ( S C_ CC /\ A e. S ) -> ( CC X. { A } ) e. ( Poly ` S ) )