Metamath Proof Explorer


Theorem quotcan

Description: Exact division with a multiple. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis quotcan.1 H = F × f G
Assertion quotcan F Poly S G Poly S G 0 𝑝 H quot G = F

Proof

Step Hyp Ref Expression
1 quotcan.1 H = F × f G
2 plyssc Poly S Poly
3 simp2 F Poly S G Poly S G 0 𝑝 G Poly S
4 2 3 sseldi F Poly S G Poly S G 0 𝑝 G Poly
5 simp1 F Poly S G Poly S G 0 𝑝 F Poly S
6 2 5 sseldi F Poly S G Poly S G 0 𝑝 F Poly
7 plymulcl F Poly S G Poly S F × f G Poly
8 1 7 eqeltrid F Poly S G Poly S H Poly
9 8 3adant3 F Poly S G Poly S G 0 𝑝 H Poly
10 simp3 F Poly S G Poly S G 0 𝑝 G 0 𝑝
11 quotcl2 H Poly G Poly G 0 𝑝 H quot G Poly
12 9 4 10 11 syl3anc F Poly S G Poly S G 0 𝑝 H quot G Poly
13 plysubcl F Poly H quot G Poly F f H quot G Poly
14 6 12 13 syl2anc F Poly S G Poly S G 0 𝑝 F f H quot G Poly
15 plymul0or G Poly F f H quot G Poly G × f F f H quot G = 0 𝑝 G = 0 𝑝 F f H quot G = 0 𝑝
16 4 14 15 syl2anc F Poly S G Poly S G 0 𝑝 G × f F f H quot G = 0 𝑝 G = 0 𝑝 F f H quot G = 0 𝑝
17 cnex V
18 17 a1i F Poly S G Poly S G 0 𝑝 V
19 plyf F Poly S F :
20 5 19 syl F Poly S G Poly S G 0 𝑝 F :
21 plyf G Poly S G :
22 3 21 syl F Poly S G Poly S G 0 𝑝 G :
23 mulcom x y x y = y x
24 23 adantl F Poly S G Poly S G 0 𝑝 x y x y = y x
25 18 20 22 24 caofcom F Poly S G Poly S G 0 𝑝 F × f G = G × f F
26 1 25 syl5eq F Poly S G Poly S G 0 𝑝 H = G × f F
27 26 oveq1d F Poly S G Poly S G 0 𝑝 H f G × f H quot G = G × f F f G × f H quot G
28 plyf H quot G Poly H quot G :
29 12 28 syl F Poly S G Poly S G 0 𝑝 H quot G :
30 subdi x y z x y z = x y x z
31 30 adantl F Poly S G Poly S G 0 𝑝 x y z x y z = x y x z
32 18 22 20 29 31 caofdi F Poly S G Poly S G 0 𝑝 G × f F f H quot G = G × f F f G × f H quot G
33 27 32 eqtr4d F Poly S G Poly S G 0 𝑝 H f G × f H quot G = G × f F f H quot G
34 33 eqeq1d F Poly S G Poly S G 0 𝑝 H f G × f H quot G = 0 𝑝 G × f F f H quot G = 0 𝑝
35 10 neneqd F Poly S G Poly S G 0 𝑝 ¬ G = 0 𝑝
36 biorf ¬ G = 0 𝑝 F f H quot G = 0 𝑝 G = 0 𝑝 F f H quot G = 0 𝑝
37 35 36 syl F Poly S G Poly S G 0 𝑝 F f H quot G = 0 𝑝 G = 0 𝑝 F f H quot G = 0 𝑝
38 16 34 37 3bitr4d F Poly S G Poly S G 0 𝑝 H f G × f H quot G = 0 𝑝 F f H quot G = 0 𝑝
39 38 biimpd F Poly S G Poly S G 0 𝑝 H f G × f H quot G = 0 𝑝 F f H quot G = 0 𝑝
40 eqid deg G = deg G
41 eqid deg F f H quot G = deg F f H quot G
42 40 41 dgrmul G Poly G 0 𝑝 F f H quot G Poly F f H quot G 0 𝑝 deg G × f F f H quot G = deg G + deg F f H quot G
43 42 expr G Poly G 0 𝑝 F f H quot G Poly F f H quot G 0 𝑝 deg G × f F f H quot G = deg G + deg F f H quot G
44 4 10 14 43 syl21anc F Poly S G Poly S G 0 𝑝 F f H quot G 0 𝑝 deg G × f F f H quot G = deg G + deg F f H quot G
45 dgrcl G Poly S deg G 0
46 3 45 syl F Poly S G Poly S G 0 𝑝 deg G 0
47 46 nn0red F Poly S G Poly S G 0 𝑝 deg G
48 dgrcl F f H quot G Poly deg F f H quot G 0
49 14 48 syl F Poly S G Poly S G 0 𝑝 deg F f H quot G 0
50 nn0addge1 deg G deg F f H quot G 0 deg G deg G + deg F f H quot G
51 47 49 50 syl2anc F Poly S G Poly S G 0 𝑝 deg G deg G + deg F f H quot G
52 breq2 deg G × f F f H quot G = deg G + deg F f H quot G deg G deg G × f F f H quot G deg G deg G + deg F f H quot G
53 51 52 syl5ibrcom F Poly S G Poly S G 0 𝑝 deg G × f F f H quot G = deg G + deg F f H quot G deg G deg G × f F f H quot G
54 44 53 syld F Poly S G Poly S G 0 𝑝 F f H quot G 0 𝑝 deg G deg G × f F f H quot G
55 33 fveq2d F Poly S G Poly S G 0 𝑝 deg H f G × f H quot G = deg G × f F f H quot G
56 55 breq2d F Poly S G Poly S G 0 𝑝 deg G deg H f G × f H quot G deg G deg G × f F f H quot G
57 plymulcl G Poly H quot G Poly G × f H quot G Poly
58 4 12 57 syl2anc F Poly S G Poly S G 0 𝑝 G × f H quot G Poly
59 plysubcl H Poly G × f H quot G Poly H f G × f H quot G Poly
60 9 58 59 syl2anc F Poly S G Poly S G 0 𝑝 H f G × f H quot G Poly
61 dgrcl H f G × f H quot G Poly deg H f G × f H quot G 0
62 60 61 syl F Poly S G Poly S G 0 𝑝 deg H f G × f H quot G 0
63 62 nn0red F Poly S G Poly S G 0 𝑝 deg H f G × f H quot G
64 47 63 lenltd F Poly S G Poly S G 0 𝑝 deg G deg H f G × f H quot G ¬ deg H f G × f H quot G < deg G
65 56 64 bitr3d F Poly S G Poly S G 0 𝑝 deg G deg G × f F f H quot G ¬ deg H f G × f H quot G < deg G
66 54 65 sylibd F Poly S G Poly S G 0 𝑝 F f H quot G 0 𝑝 ¬ deg H f G × f H quot G < deg G
67 66 necon4ad F Poly S G Poly S G 0 𝑝 deg H f G × f H quot G < deg G F f H quot G = 0 𝑝
68 eqid H f G × f H quot G = H f G × f H quot G
69 68 quotdgr H Poly G Poly G 0 𝑝 H f G × f H quot G = 0 𝑝 deg H f G × f H quot G < deg G
70 9 4 10 69 syl3anc F Poly S G Poly S G 0 𝑝 H f G × f H quot G = 0 𝑝 deg H f G × f H quot G < deg G
71 39 67 70 mpjaod F Poly S G Poly S G 0 𝑝 F f H quot G = 0 𝑝
72 df-0p 0 𝑝 = × 0
73 71 72 syl6eq F Poly S G Poly S G 0 𝑝 F f H quot G = × 0
74 ofsubeq0 V F : H quot G : F f H quot G = × 0 F = H quot G
75 18 20 29 74 syl3anc F Poly S G Poly S G 0 𝑝 F f H quot G = × 0 F = H quot G
76 73 75 mpbid F Poly S G Poly S G 0 𝑝 F = H quot G
77 76 eqcomd F Poly S G Poly S G 0 𝑝 H quot G = F