Metamath Proof Explorer

Theorem plyss

Description: The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion plyss 
|- ( ( S C_ T /\ T C_ CC ) -> ( Poly ` S ) C_ ( Poly ` T ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( S C_ T /\ T C_ CC ) -> T C_ CC )
2 cnex 
 |-  CC e. _V
3 ssexg 
 |-  ( ( T C_ CC /\ CC e. _V ) -> T e. _V )
4 1 2 3 sylancl 
 |-  ( ( S C_ T /\ T C_ CC ) -> T e. _V )
5 snex 
 |-  { 0 } e. _V
6 unexg 
 |-  ( ( T e. _V /\ { 0 } e. _V ) -> ( T u. { 0 } ) e. _V )
7 4 5 6 sylancl 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( T u. { 0 } ) e. _V )
8 unss1 
 |-  ( S C_ T -> ( S u. { 0 } ) C_ ( T u. { 0 } ) )
9 8 adantr 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( S u. { 0 } ) C_ ( T u. { 0 } ) )
10 mapss 
 |-  ( ( ( T u. { 0 } ) e. _V /\ ( S u. { 0 } ) C_ ( T u. { 0 } ) ) -> ( ( S u. { 0 } ) ^m NN0 ) C_ ( ( T u. { 0 } ) ^m NN0 ) )
11 7 9 10 syl2anc 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( ( S u. { 0 } ) ^m NN0 ) C_ ( ( T u. { 0 } ) ^m NN0 ) )
12 ssrexv 
 |-  ( ( ( S u. { 0 } ) ^m NN0 ) C_ ( ( T u. { 0 } ) ^m NN0 ) -> ( E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> E. a e. ( ( T u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
13 11 12 syl 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( E. a e. ( ( S u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) -> E. a e. ( ( T u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
14 13 reximdv 
 |-  ( ( S C_ T /\ T 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 ) ) ) -> E. n e. NN0 E. a e. ( ( T u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) ) )
15 14 ss2abdv 
 |-  ( ( S C_ T /\ T C_ CC ) -> { f | 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 ) ) ) } C_ { f | E. n e. NN0 E. a e. ( ( T u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )
16 sstr 
 |-  ( ( S C_ T /\ T C_ CC ) -> S C_ CC )
17 plyval 
 |-  ( S C_ CC -> ( Poly ` S ) = { f | 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 ) ) ) } )
18 16 17 syl 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( Poly ` S ) = { f | 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 ) ) ) } )
19 plyval 
 |-  ( T C_ CC -> ( Poly ` T ) = { f | E. n e. NN0 E. a e. ( ( T u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )
20 19 adantl 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( Poly ` T ) = { f | E. n e. NN0 E. a e. ( ( T u. { 0 } ) ^m NN0 ) f = ( z e. CC |-> sum_ k e. ( 0 ... n ) ( ( a ` k ) x. ( z ^ k ) ) ) } )
21 15 18 20 3sstr4d 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( Poly ` S ) C_ ( Poly ` T ) )