q1pvsca

Description: Scalar multiplication property of the polynomial division. (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$
	q1pvsca.1	$⊢ \underset{˙}{\times} = \cdot_{P}$
	q1pvsca.k	$⊢ K = {Base}_{R}$
	q1pvsca.8	$⊢ φ \to B \in K$
Assertion	q1pvsca	$⊢ φ \to (B \underset{˙}{\times} A) \underset{˙}{\times} C = B \underset{˙}{\times} (A \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		q1pvsca.1	$⊢ \underset{˙}{\times} = \cdot_{P}$
9		q1pvsca.k	$⊢ K = {Base}_{R}$
10		q1pvsca.8	$⊢ φ \to B \in K$
11		eqid	$⊢ Scalar (P) = Scalar (P)$
12		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
13	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
14	5 13	syl	$⊢ φ \to P \in LMod$
15	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
16	5 15	syl	$⊢ φ \to R = Scalar (P)$
17	16	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (P)}$
18	9 17	eqtrid	$⊢ φ \to K = {Base}_{Scalar (P)}$
19	10 18	eleqtrd	$⊢ φ \to B \in {Base}_{Scalar (P)}$
20	2 11 8 12 14 19 6	lmodvscld	$⊢ φ \to B \underset{˙}{\times} A \in U$
21	4 1 2 3	q1pcl	$⊢ (R \in Ring \land A \in U \land C \in N) \to A \underset{˙}{\times} C \in U$
22	5 6 7 21	syl3anc	$⊢ φ \to A \underset{˙}{\times} C \in U$
23	2 11 8 12 14 19 22	lmodvscld	$⊢ φ \to B \underset{˙}{\times} (A \underset{˙}{\times} C) \in U$
24	14	lmodgrpd	$⊢ φ \to P \in Grp$
25		eqid	$⊢ \cdot_{P} = \cdot_{P}$
26	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
27	5 26	syl	$⊢ φ \to P \in Ring$
28	1 2 3	uc1pcl	$⊢ C \in N \to C \in U$
29	7 28	syl	$⊢ φ \to C \in U$
30	2 25 27 23 29	ringcld	$⊢ φ \to (B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C \in U$
31		eqid	$⊢ -_{P} = -_{P}$
32	2 31	grpsubcl	$⊢ (P \in Grp \land B \underset{˙}{\times} A \in U \land (B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C \in U) \to (B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C) \in U$
33	24 20 30 32	syl3anc	$⊢ φ \to (B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C) \in U$
34		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
35	34 1 2	deg1xrcl	$⊢ (B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C) \in U \to \deg_{1} (R) ((B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C)) \in ℝ^{*}$
36	33 35	syl	$⊢ φ \to \deg_{1} (R) ((B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C)) \in ℝ^{*}$
37		eqid	$⊢ {rem}_{1p} (R) = {rem}_{1p} (R)$
38	37 1 2 4 25 31	r1pval	$⊢ (A \in U \land C \in U) \to A {rem}_{1p} (R) C = A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)$
39	6 29 38	syl2anc	$⊢ φ \to A {rem}_{1p} (R) C = A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)$
40	2 25 27 22 29	ringcld	$⊢ φ \to (A \underset{˙}{\times} C) \cdot_{P} C \in U$
41	2 31	grpsubcl	$⊢ (P \in Grp \land A \in U \land (A \underset{˙}{\times} C) \cdot_{P} C \in U) \to A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C) \in U$
42	24 6 40 41	syl3anc	$⊢ φ \to A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C) \in U$
43	39 42	eqeltrd	$⊢ φ \to A {rem}_{1p} (R) C \in U$
44	34 1 2	deg1xrcl	$⊢ A {rem}_{1p} (R) C \in U \to \deg_{1} (R) (A {rem}_{1p} (R) C) \in ℝ^{*}$
45	43 44	syl	$⊢ φ \to \deg_{1} (R) (A {rem}_{1p} (R) C) \in ℝ^{*}$
46	34 1 2	deg1xrcl	$⊢ C \in U \to \deg_{1} (R) (C) \in ℝ^{*}$
47	29 46	syl	$⊢ φ \to \deg_{1} (R) (C) \in ℝ^{*}$
48	1 34 5 2 9 8 10 42	deg1vscale	$⊢ φ \to \deg_{1} (R) (B \underset{˙}{\times} (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C))) \leq \deg_{1} (R) (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C))$
49	1 25 2 9 8	ply1ass23l	$⊢ (R \in Ring \land (B \in K \land A \underset{˙}{\times} C \in U \land C \in U)) \to (B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C = B \underset{˙}{\times} ((A \underset{˙}{\times} C) \cdot_{P} C)$
50	5 10 22 29 49	syl13anc	$⊢ φ \to (B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C = B \underset{˙}{\times} ((A \underset{˙}{\times} C) \cdot_{P} C)$
51	50	oveq2d	$⊢ φ \to (B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C) = (B \underset{˙}{\times} A) -_{P} (B \underset{˙}{\times} ((A \underset{˙}{\times} C) \cdot_{P} C))$
52	2 8 11 12 31 14 19 6 40	lmodsubdi	$⊢ φ \to B \underset{˙}{\times} (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)) = (B \underset{˙}{\times} A) -_{P} (B \underset{˙}{\times} ((A \underset{˙}{\times} C) \cdot_{P} C))$
53	51 52	eqtr4d	$⊢ φ \to (B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C) = B \underset{˙}{\times} (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C))$
54	53	fveq2d	$⊢ φ \to \deg_{1} (R) ((B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C)) = \deg_{1} (R) (B \underset{˙}{\times} (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C)))$
55	39	fveq2d	$⊢ φ \to \deg_{1} (R) (A {rem}_{1p} (R) C) = \deg_{1} (R) (A -_{P} ((A \underset{˙}{\times} C) \cdot_{P} C))$
56	48 54 55	3brtr4d	$⊢ φ \to \deg_{1} (R) ((B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C)) \leq \deg_{1} (R) (A {rem}_{1p} (R) C)$
57	37 1 2 3 34	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)$
58	5 6 7 57	syl3anc	$⊢ φ \to \deg_{1} (R) (A {rem}_{1p} (R) C) < \deg_{1} (R) (C)$
59	36 45 47 56 58	xrlelttrd	$⊢ φ \to \deg_{1} (R) ((B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C)) < \deg_{1} (R) (C)$
60	4 1 2 34 31 25 3	q1peqb	$⊢ (R \in Ring \land B \underset{˙}{\times} A \in U \land C \in N) \to ((B \underset{˙}{\times} (A \underset{˙}{\times} C) \in U \land \deg_{1} (R) ((B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C)) < \deg_{1} (R) (C)) \leftrightarrow (B \underset{˙}{\times} A) \underset{˙}{\times} C = B \underset{˙}{\times} (A \underset{˙}{\times} C))$
61	60	biimpa	$⊢ ((R \in Ring \land B \underset{˙}{\times} A \in U \land C \in N) \land (B \underset{˙}{\times} (A \underset{˙}{\times} C) \in U \land \deg_{1} (R) ((B \underset{˙}{\times} A) -_{P} ((B \underset{˙}{\times} (A \underset{˙}{\times} C)) \cdot_{P} C)) < \deg_{1} (R) (C))) \to (B \underset{˙}{\times} A) \underset{˙}{\times} C = B \underset{˙}{\times} (A \underset{˙}{\times} C)$
62	5 20 7 23 59 61	syl32anc	$⊢ φ \to (B \underset{˙}{\times} A) \underset{˙}{\times} C = B \underset{˙}{\times} (A \underset{˙}{\times} C)$

Metamath Proof Explorer

Theorem q1pvsca

Proof