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 T T Poly S Poly T

Proof

Step Hyp Ref Expression
1 simpr S T T T
2 cnex V
3 ssexg T V T V
4 1 2 3 sylancl S T T T V
5 snex 0 V
6 unexg T V 0 V T 0 V
7 4 5 6 sylancl S T T T 0 V
8 unss1 S T S 0 T 0
9 8 adantr S T T S 0 T 0
10 mapss T 0 V S 0 T 0 S 0 0 T 0 0
11 7 9 10 syl2anc S T T S 0 0 T 0 0
12 ssrexv S 0 0 T 0 0 a S 0 0 f = z k = 0 n a k z k a T 0 0 f = z k = 0 n a k z k
13 11 12 syl S T T a S 0 0 f = z k = 0 n a k z k a T 0 0 f = z k = 0 n a k z k
14 13 reximdv S T T n 0 a S 0 0 f = z k = 0 n a k z k n 0 a T 0 0 f = z k = 0 n a k z k
15 14 ss2abdv S T T f | n 0 a S 0 0 f = z k = 0 n a k z k f | n 0 a T 0 0 f = z k = 0 n a k z k
16 sstr S T T S
17 plyval S Poly S = f | n 0 a S 0 0 f = z k = 0 n a k z k
18 16 17 syl S T T Poly S = f | n 0 a S 0 0 f = z k = 0 n a k z k
19 plyval T Poly T = f | n 0 a T 0 0 f = z k = 0 n a k z k
20 19 adantl S T T Poly T = f | n 0 a T 0 0 f = z k = 0 n a k z k
21 15 18 20 3sstr4d S T T Poly S Poly T