Definition df-0p 23187

Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.)

Assertion

Ref	Expression
df-0p	⊢ 0𝑝 = (ℂ × {0})

Detailed syntax breakdown of Definition df-0p

Step	Hyp	Ref	Expression
1		c0p 23186	. 2 class 0𝑝
2		cc 9790	. . 3 class ℂ
3		cc0 9792	. . . 4 class 0
4	3	csn 4124	. . 3 class {0}
5	2, 4	cxp 5025	. 2 class (ℂ × {0})
6	1, 5	wceq 1474	1 wff 0𝑝 = (ℂ × {0})

This definition is referenced by:  0pval  23188  0plef  23189  0pledm  23190  itg1ge0  23203  mbfi1fseqlem5  23236  itg2addlem  23275  ply0  23712  coeeulem  23728  dgrnznn  23751  coe0  23760  dgr0  23766  dgreq0  23769  dgrmulc  23775  plymul0or  23784  plydiveu  23801  fta1lem  23810  fta1  23811  quotcan  23812  plyexmo  23816  elqaalem3  23824  aaliou2  23843  plymul02  29742  mpaaeu  36522