Metamath Proof Explorer


Theorem elply

Description: Definition of a polynomial with coefficients in S . (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion elply F Poly S S n 0 a S 0 0 F = z k = 0 n a k z k

Proof

Step Hyp Ref Expression
1 plybss F Poly S S
2 plyval S Poly S = f | n 0 a S 0 0 f = z k = 0 n a k z k
3 2 eleq2d S F Poly S F f | n 0 a S 0 0 f = z k = 0 n a k z k
4 id F = z k = 0 n a k z k F = z k = 0 n a k z k
5 cnex V
6 5 mptex z k = 0 n a k z k V
7 4 6 eqeltrdi F = z k = 0 n a k z k F V
8 7 a1i n 0 a S 0 0 F = z k = 0 n a k z k F V
9 8 rexlimivv n 0 a S 0 0 F = z k = 0 n a k z k F V
10 eqeq1 f = F f = z k = 0 n a k z k F = z k = 0 n a k z k
11 10 2rexbidv f = F n 0 a S 0 0 f = z k = 0 n a k z k n 0 a S 0 0 F = z k = 0 n a k z k
12 9 11 elab3 F f | n 0 a S 0 0 f = z k = 0 n a k z k n 0 a S 0 0 F = z k = 0 n a k z k
13 3 12 bitrdi S F Poly S n 0 a S 0 0 F = z k = 0 n a k z k
14 1 13 biadanii F Poly S S n 0 a S 0 0 F = z k = 0 n a k z k