q1pdir

Description: Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	r1padd1.p	$⊢ P = {Poly}_{1} (R)$
	r1padd1.u	$⊢ U = {Base}_{P}$
	r1padd1.n	$⊢ N = {Unic}_{1p} (R)$
	q1pdir.d	$⊢ \underset{˙}{\times} = {quot}_{1p} (R)$
	q1pdir.r	$⊢ φ \to R \in Ring$
	q1pdir.a	$⊢ φ \to A \in U$
	q1pdir.c	$⊢ φ \to C \in N$
	q1pdir.b	$⊢ φ \to B \in U$
	q1pdir.1	$⊢ \underset{˙}{+} = +_{P}$
Assertion	q1pdir	$⊢ φ \to (A \underset{˙}{+} B) \underset{˙}{\times} C = (A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)$

Proof

Step	Hyp	Ref	Expression
1		r1padd1.p	$⊢ P = {Poly}_{1} (R)$
2		r1padd1.u	$⊢ U = {Base}_{P}$
3		r1padd1.n	$⊢ N = {Unic}_{1p} (R)$
4		q1pdir.d	$⊢ \underset{˙}{\times} = {quot}_{1p} (R)$
5		q1pdir.r	$⊢ φ \to R \in Ring$
6		q1pdir.a	$⊢ φ \to A \in U$
7		q1pdir.c	$⊢ φ \to C \in N$
8		q1pdir.b	$⊢ φ \to B \in U$
9		q1pdir.1	$⊢ \underset{˙}{+} = +_{P}$
10	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
11	5 10	syl	$⊢ φ \to P \in Ring$
12	11	ringgrpd	$⊢ φ \to P \in Grp$
13	2 9 12 6 8	grpcld	$⊢ φ \to A \underset{˙}{+} B \in U$
14	4 1 2 3	q1pcl	$⊢ (R \in Ring \land A \in U \land C \in N) \to A \underset{˙}{\times} C \in U$
15	5 6 7 14	syl3anc	$⊢ φ \to A \underset{˙}{\times} C \in U$
16	4 1 2 3	q1pcl	$⊢ (R \in Ring \land B \in U \land C \in N) \to B \underset{˙}{\times} C \in U$
17	5 8 7 16	syl3anc	$⊢ φ \to B \underset{˙}{\times} C \in U$
18	2 9 12 15 17	grpcld	$⊢ φ \to (A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C) \in U$
19	1 2 3	uc1pcl	$⊢ C \in N \to C \in U$
20	7 19	syl	$⊢ φ \to C \in U$
21		eqid	$⊢ \cdot_{P} = \cdot_{P}$
22	2 9 21	ringdir	$⊢ (P \in Ring \land (A \underset{˙}{\times} C \in U \land B \underset{˙}{\times} C \in U \land C \in U)) \to ((A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)) \cdot_{P} C = ((A \underset{˙}{\times} C) \cdot_{P} C) \underset{˙}{+} ((B \underset{˙}{\times} C) \cdot_{P} C)$
23	11 15 17 20 22	syl13anc	$⊢ φ \to ((A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)) \cdot_{P} C = ((A \underset{˙}{\times} C) \cdot_{P} C) \underset{˙}{+} ((B \underset{˙}{\times} C) \cdot_{P} C)$
24	23	oveq2d	$⊢ φ \to (A \underset{˙}{+} B) -_{P} (((A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)) \cdot_{P} C) = (A \underset{˙}{+} B) -_{P} (((A \underset{˙}{\times} C) \cdot_{P} C) \underset{˙}{+} ((B \underset{˙}{\times} C) \cdot_{P} C))$
25	11	ringabld	$⊢ φ \to P \in Abel$
26	2 21 11 15 20	ringcld	$⊢ φ \to (A \underset{˙}{\times} C) \cdot_{P} C \in U$
27	2 21 11 17 20	ringcld	$⊢ φ \to (B \underset{˙}{\times} C) \cdot_{P} C \in U$
28		eqid	$⊢ -_{P} = -_{P}$
29	2 9 28	ablsub4	$⊢ (P \in Abel \land (A \in U \land B \in U) \land ((A \underset{˙}{\times} C) \cdot_{P} C \in U \land (B \underset{˙}{\times} C) \cdot_{P} C \in U)) \to (A \underset{˙}{+} B) -_{P} (((A \underset{˙}{\times} C) \cdot_{P} C) \underset{˙}{+} ((B \underset{˙}{\times} C) \cdot_{P} C)) = (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)) \underset{˙}{+} (B -_{P} ((B \underset{˙}{\times} C) \cdot_{P} C))$
30	25 6 8 26 27 29	syl122anc	$⊢ φ \to (A \underset{˙}{+} B) -_{P} (((A \underset{˙}{\times} C) \cdot_{P} C) \underset{˙}{+} ((B \underset{˙}{\times} C) \cdot_{P} C)) = (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)) \underset{˙}{+} (B -_{P} ((B \underset{˙}{\times} C) \cdot_{P} C))$
31	24 30	eqtrd	$⊢ φ \to (A \underset{˙}{+} B) -_{P} (((A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)) \cdot_{P} C) = (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)) \underset{˙}{+} (B -_{P} ((B \underset{˙}{\times} C) \cdot_{P} C))$
32	31	fveq2d	$⊢ φ \to \deg_{1} (R) ((A \underset{˙}{+} B) -_{P} (((A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)) \cdot_{P} C)) = \deg_{1} (R) ((A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)) \underset{˙}{+} (B -_{P} ((B \underset{˙}{\times} C) \cdot_{P} C)))$
33		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
34		eqid	$⊢ {rem}_{1p} (R) = {rem}_{1p} (R)$
35	34 1 2 4 21 28	r1pval	$⊢ (A \in U \land C \in U) \to A {rem}_{1p} (R) C = A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)$
36	6 20 35	syl2anc	$⊢ φ \to A {rem}_{1p} (R) C = A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)$
37	34 1 2 3	r1pcl	$⊢ (R \in Ring \land A \in U \land C \in N) \to A {rem}_{1p} (R) C \in U$
38	5 6 7 37	syl3anc	$⊢ φ \to A {rem}_{1p} (R) C \in U$
39	36 38	eqeltrrd	$⊢ φ \to A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C) \in U$
40	34 1 2 4 21 28	r1pval	$⊢ (B \in U \land C \in U) \to B {rem}_{1p} (R) C = B -_{P} ((B \underset{˙}{\times} C) \cdot_{P} C)$
41	8 20 40	syl2anc	$⊢ φ \to B {rem}_{1p} (R) C = B -_{P} ((B \underset{˙}{\times} C) \cdot_{P} C)$
42	34 1 2 3	r1pcl	$⊢ (R \in Ring \land B \in U \land C \in N) \to B {rem}_{1p} (R) C \in U$
43	5 8 7 42	syl3anc	$⊢ φ \to B {rem}_{1p} (R) C \in U$
44	41 43	eqeltrrd	$⊢ φ \to B -_{P} ((B \underset{˙}{\times} C) \cdot_{P} C) \in U$
45	33 1 2	deg1xrcl	$⊢ C \in U \to \deg_{1} (R) (C) \in ℝ^{*}$
46	20 45	syl	$⊢ φ \to \deg_{1} (R) (C) \in ℝ^{*}$
47	36	fveq2d	$⊢ φ \to \deg_{1} (R) (A {rem}_{1p} (R) C) = \deg_{1} (R) (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C))$
48	34 1 2 3 33	r1pdeglt	$⊢ (R \in Ring \land A \in U \land C \in N) \to \deg_{1} (R) (A {rem}_{1p} (R) C) < \deg_{1} (R) (C)$
49	5 6 7 48	syl3anc	$⊢ φ \to \deg_{1} (R) (A {rem}_{1p} (R) C) < \deg_{1} (R) (C)$
50	47 49	eqbrtrrd	$⊢ φ \to \deg_{1} (R) (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)) < \deg_{1} (R) (C)$
51	41	fveq2d	$⊢ φ \to \deg_{1} (R) (B {rem}_{1p} (R) C) = \deg_{1} (R) (B -_{P} ((B \underset{˙}{\times} C) \cdot_{P} C))$
52	34 1 2 3 33	r1pdeglt	$⊢ (R \in Ring \land B \in U \land C \in N) \to \deg_{1} (R) (B {rem}_{1p} (R) C) < \deg_{1} (R) (C)$
53	5 8 7 52	syl3anc	$⊢ φ \to \deg_{1} (R) (B {rem}_{1p} (R) C) < \deg_{1} (R) (C)$
54	51 53	eqbrtrrd	$⊢ φ \to \deg_{1} (R) (B -_{P} ((B \underset{˙}{\times} C) \cdot_{P} C)) < \deg_{1} (R) (C)$
55	1 33 5 2 9 39 44 46 50 54	deg1addlt	$⊢ φ \to \deg_{1} (R) ((A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)) \underset{˙}{+} (B -_{P} ((B \underset{˙}{\times} C) \cdot_{P} C))) < \deg_{1} (R) (C)$
56	32 55	eqbrtrd	$⊢ φ \to \deg_{1} (R) ((A \underset{˙}{+} B) -_{P} (((A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)) \cdot_{P} C)) < \deg_{1} (R) (C)$
57	4 1 2 33 28 21 3	q1peqb	$⊢ (R \in Ring \land A \underset{˙}{+} B \in U \land C \in N) \to (((A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C) \in U \land \deg_{1} (R) ((A \underset{˙}{+} B) -_{P} (((A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)) \cdot_{P} C)) < \deg_{1} (R) (C)) \leftrightarrow (A \underset{˙}{+} B) \underset{˙}{\times} C = (A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C))$
58	57	biimpa	$⊢ ((R \in Ring \land A \underset{˙}{+} B \in U \land C \in N) \land ((A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C) \in U \land \deg_{1} (R) ((A \underset{˙}{+} B) -_{P} (((A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)) \cdot_{P} C)) < \deg_{1} (R) (C))) \to (A \underset{˙}{+} B) \underset{˙}{\times} C = (A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)$
59	5 13 7 18 56 58	syl32anc	$⊢ φ \to (A \underset{˙}{+} B) \underset{˙}{\times} C = (A \underset{˙}{\times} C) \underset{˙}{+} (B \underset{˙}{\times} C)$

Metamath Proof Explorer

Theorem q1pdir

Proof