Metamath Proof Explorer


Theorem eldioph3

Description: Inference version of eldioph3b with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion eldioph3 N 0 P mzPoly t | u 0 t = u 1 N P u = 0 Dioph N

Proof

Step Hyp Ref Expression
1 simpl N 0 P mzPoly N 0
2 simpr N 0 P mzPoly P mzPoly
3 eqidd N 0 P mzPoly t | u 0 t = u 1 N P u = 0 = t | u 0 t = u 1 N P u = 0
4 fveq1 p = P p b = P b
5 4 eqeq1d p = P p b = 0 P b = 0
6 5 anbi2d p = P a = b 1 N p b = 0 a = b 1 N P b = 0
7 6 rexbidv p = P b 0 a = b 1 N p b = 0 b 0 a = b 1 N P b = 0
8 7 abbidv p = P a | b 0 a = b 1 N p b = 0 = a | b 0 a = b 1 N P b = 0
9 eqeq1 a = t a = b 1 N t = b 1 N
10 9 anbi1d a = t a = b 1 N P b = 0 t = b 1 N P b = 0
11 10 rexbidv a = t b 0 a = b 1 N P b = 0 b 0 t = b 1 N P b = 0
12 reseq1 b = u b 1 N = u 1 N
13 12 eqeq2d b = u t = b 1 N t = u 1 N
14 fveqeq2 b = u P b = 0 P u = 0
15 13 14 anbi12d b = u t = b 1 N P b = 0 t = u 1 N P u = 0
16 15 cbvrexvw b 0 t = b 1 N P b = 0 u 0 t = u 1 N P u = 0
17 11 16 bitrdi a = t b 0 a = b 1 N P b = 0 u 0 t = u 1 N P u = 0
18 17 cbvabv a | b 0 a = b 1 N P b = 0 = t | u 0 t = u 1 N P u = 0
19 8 18 eqtrdi p = P a | b 0 a = b 1 N p b = 0 = t | u 0 t = u 1 N P u = 0
20 19 rspceeqv P mzPoly t | u 0 t = u 1 N P u = 0 = t | u 0 t = u 1 N P u = 0 p mzPoly t | u 0 t = u 1 N P u = 0 = a | b 0 a = b 1 N p b = 0
21 2 3 20 syl2anc N 0 P mzPoly p mzPoly t | u 0 t = u 1 N P u = 0 = a | b 0 a = b 1 N p b = 0
22 eldioph3b t | u 0 t = u 1 N P u = 0 Dioph N N 0 p mzPoly t | u 0 t = u 1 N P u = 0 = a | b 0 a = b 1 N p b = 0
23 1 21 22 sylanbrc N 0 P mzPoly t | u 0 t = u 1 N P u = 0 Dioph N