Metamath Proof Explorer

Theorem plyun0

Description: The set of polynomials is unaffected by the addition of zero. (This is built into the definition because all higher powers of a polynomial are effectively zero, so we require that the coefficient field contain zero to simplify some of our closure theorems.) (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion plyun0 
|- ( Poly ` ( S u. { 0 } ) ) = ( Poly ` S )

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 snssi 
 |-  ( 0 e. CC -> { 0 } C_ CC )
3 1 2 ax-mp 
 |-  { 0 } C_ CC
4 3 biantru 
 |-  ( S C_ CC <-> ( S C_ CC /\ { 0 } C_ CC ) )
5 unss 
 |-  ( ( S C_ CC /\ { 0 } C_ CC ) <-> ( S u. { 0 } ) C_ CC )
6 4 5 bitr2i 
 |-  ( ( S u. { 0 } ) C_ CC <-> S C_ CC )
7 unass 
 |-  ( ( S u. { 0 } ) u. { 0 } ) = ( S u. ( { 0 } u. { 0 } ) )
8 unidm 
 |-  ( { 0 } u. { 0 } ) = { 0 }
9 8 uneq2i 
 |-  ( S u. ( { 0 } u. { 0 } ) ) = ( S u. { 0 } )
10 7 9 eqtri 
 |-  ( ( S u. { 0 } ) u. { 0 } ) = ( S u. { 0 } )
11 10 oveq1i 
 |-  ( ( ( S u. { 0 } ) u. { 0 } ) ^m NN0 ) = ( ( S u. { 0 } ) ^m NN0 )
12 11 rexeqi 
 |-  ( E. a e. ( ( ( S u. { 0 } ) u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) <-> E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
13 12 rexbii 
 |-  ( E. n e. NN0 E. a e. ( ( ( S u. { 0 } ) u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) <-> E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) )
14 6 13 anbi12i 
 |-  ( ( ( S u. { 0 } ) C_ CC /\ E. n e. NN0 E. a e. ( ( ( S u. { 0 } ) u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) <-> ( S C_ CC /\ E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
15 elply 
 |-  ( f e. ( Poly ` ( S u. { 0 } ) ) <-> ( ( S u. { 0 } ) C_ CC /\ E. n e. NN0 E. a e. ( ( ( S u. { 0 } ) u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
16 elply 
 |-  ( f e. ( Poly ` S ) <-> ( S C_ CC /\ E. n e. NN0 E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
17 14 15 16 3bitr4i 
 |-  ( f e. ( Poly ` ( S u. { 0 } ) ) <-> f e. ( Poly ` S ) )
18 17 eqriv 
 |-  ( Poly ` ( S u. { 0 } ) ) = ( Poly ` S )