Metamath Proof Explorer


Theorem q1peqb

Description: Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses q1pval.q Q = quot 1p R
q1pval.p P = Poly 1 R
q1pval.b B = Base P
q1pval.d D = deg 1 R
q1pval.m - ˙ = - P
q1pval.t · ˙ = P
q1peqb.c C = Unic 1p R
Assertion q1peqb R Ring F B G C X B D F - ˙ X · ˙ G < D G F Q G = X

Proof

Step Hyp Ref Expression
1 q1pval.q Q = quot 1p R
2 q1pval.p P = Poly 1 R
3 q1pval.b B = Base P
4 q1pval.d D = deg 1 R
5 q1pval.m - ˙ = - P
6 q1pval.t · ˙ = P
7 q1peqb.c C = Unic 1p R
8 elex X B X V
9 8 adantr X B D F - ˙ X · ˙ G < D G X V
10 9 a1i R Ring F B G C X B D F - ˙ X · ˙ G < D G X V
11 ovex F Q G V
12 eleq1 F Q G = X F Q G V X V
13 11 12 mpbii F Q G = X X V
14 13 a1i R Ring F B G C F Q G = X X V
15 simpr R Ring F B G C X V X V
16 eqid 0 P = 0 P
17 simp1 R Ring F B G C R Ring
18 simp2 R Ring F B G C F B
19 2 3 7 uc1pcl G C G B
20 19 3ad2ant3 R Ring F B G C G B
21 2 16 7 uc1pn0 G C G 0 P
22 21 3ad2ant3 R Ring F B G C G 0 P
23 eqid Unit R = Unit R
24 4 23 7 uc1pldg G C coe 1 G D G Unit R
25 24 3ad2ant3 R Ring F B G C coe 1 G D G Unit R
26 2 4 3 5 16 6 17 18 20 22 25 23 ply1divalg2 R Ring F B G C ∃! q B D F - ˙ q · ˙ G < D G
27 df-reu ∃! q B D F - ˙ q · ˙ G < D G ∃! q q B D F - ˙ q · ˙ G < D G
28 26 27 sylib R Ring F B G C ∃! q q B D F - ˙ q · ˙ G < D G
29 28 adantr R Ring F B G C X V ∃! q q B D F - ˙ q · ˙ G < D G
30 eleq1 q = X q B X B
31 oveq1 q = X q · ˙ G = X · ˙ G
32 31 oveq2d q = X F - ˙ q · ˙ G = F - ˙ X · ˙ G
33 32 fveq2d q = X D F - ˙ q · ˙ G = D F - ˙ X · ˙ G
34 33 breq1d q = X D F - ˙ q · ˙ G < D G D F - ˙ X · ˙ G < D G
35 30 34 anbi12d q = X q B D F - ˙ q · ˙ G < D G X B D F - ˙ X · ˙ G < D G
36 35 adantl R Ring F B G C X V q = X q B D F - ˙ q · ˙ G < D G X B D F - ˙ X · ˙ G < D G
37 15 29 36 iota2d R Ring F B G C X V X B D F - ˙ X · ˙ G < D G ι q | q B D F - ˙ q · ˙ G < D G = X
38 1 2 3 4 5 6 q1pval F B G B F Q G = ι q B | D F - ˙ q · ˙ G < D G
39 18 20 38 syl2anc R Ring F B G C F Q G = ι q B | D F - ˙ q · ˙ G < D G
40 df-riota ι q B | D F - ˙ q · ˙ G < D G = ι q | q B D F - ˙ q · ˙ G < D G
41 39 40 eqtrdi R Ring F B G C F Q G = ι q | q B D F - ˙ q · ˙ G < D G
42 41 adantr R Ring F B G C X V F Q G = ι q | q B D F - ˙ q · ˙ G < D G
43 42 eqeq1d R Ring F B G C X V F Q G = X ι q | q B D F - ˙ q · ˙ G < D G = X
44 37 43 bitr4d R Ring F B G C X V X B D F - ˙ X · ˙ G < D G F Q G = X
45 44 ex R Ring F B G C X V X B D F - ˙ X · ˙ G < D G F Q G = X
46 10 14 45 pm5.21ndd R Ring F B G C X B D F - ˙ X · ˙ G < D G F Q G = X