This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 mulridd 
 |-  ( ( ( 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 ) )