quotcan

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

		Ref	Expression
	Hypothesis	quotcan.1	$⊢ H = F \times_{f} G$
	Assertion	quotcan	$⊢ (F \in Poly (S) \land G \in Poly (S) \land G \neq 0_{𝑝}) \to H quot G = F$

Proof

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

Metamath Proof Explorer

Theorem quotcan

Proof