uc1pmon1p

Description: Make a unitic polynomial monic by multiplying a factor to normalize the leading coefficient. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	uc1pmon1p.c	$⊢ C = {Unic}_{1p} (R)$
	uc1pmon1p.m	$⊢ M = {Monic}_{1p} (R)$
	uc1pmon1p.p	$⊢ P = {Poly}_{1} (R)$
	uc1pmon1p.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	uc1pmon1p.a	$⊢ A = algSc (P)$
	uc1pmon1p.d	$⊢ D = \deg_{1} (R)$
	uc1pmon1p.i	$⊢ I = {inv}_{r} (R)$
Assertion	uc1pmon1p	$⊢ (R \in Ring \land X \in C) \to A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \in M$

Proof

Step	Hyp	Ref	Expression
1		uc1pmon1p.c	$⊢ C = {Unic}_{1p} (R)$
2		uc1pmon1p.m	$⊢ M = {Monic}_{1p} (R)$
3		uc1pmon1p.p	$⊢ P = {Poly}_{1} (R)$
4		uc1pmon1p.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		uc1pmon1p.a	$⊢ A = algSc (P)$
6		uc1pmon1p.d	$⊢ D = \deg_{1} (R)$
7		uc1pmon1p.i	$⊢ I = {inv}_{r} (R)$
8	3	ply1ring	$⊢ R \in Ring \to P \in Ring$
9	8	adantr	$⊢ (R \in Ring \land X \in C) \to P \in Ring$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11		eqid	$⊢ {Base}_{P} = {Base}_{P}$
12	3 5 10 11	ply1sclf	$⊢ R \in Ring \to A : {Base}_{R} ⟶ {Base}_{P}$
13	12	adantr	$⊢ (R \in Ring \land X \in C) \to A : {Base}_{R} ⟶ {Base}_{P}$
14		eqid	$⊢ Unit (R) = Unit (R)$
15	6 14 1	uc1pldg	$⊢ X \in C \to {coe}_{1} (X) (D (X)) \in Unit (R)$
16	14 7 10	ringinvcl	$⊢ (R \in Ring \land {coe}_{1} (X) (D (X)) \in Unit (R)) \to I ({coe}_{1} (X) (D (X))) \in {Base}_{R}$
17	15 16	sylan2	$⊢ (R \in Ring \land X \in C) \to I ({coe}_{1} (X) (D (X))) \in {Base}_{R}$
18	13 17	ffvelrnd	$⊢ (R \in Ring \land X \in C) \to A (I ({coe}_{1} (X) (D (X)))) \in {Base}_{P}$
19	3 11 1	uc1pcl	$⊢ X \in C \to X \in {Base}_{P}$
20	19	adantl	$⊢ (R \in Ring \land X \in C) \to X \in {Base}_{P}$
21	11 4	ringcl	$⊢ (P \in Ring \land A (I ({coe}_{1} (X) (D (X)))) \in {Base}_{P} \land X \in {Base}_{P}) \to A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \in {Base}_{P}$
22	9 18 20 21	syl3anc	$⊢ (R \in Ring \land X \in C) \to A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \in {Base}_{P}$
23		simpl	$⊢ (R \in Ring \land X \in C) \to R \in Ring$
24		eqid	$⊢ RLReg (R) = RLReg (R)$
25	24 14	unitrrg	$⊢ R \in Ring \to Unit (R) \subseteq RLReg (R)$
26	25	adantr	$⊢ (R \in Ring \land X \in C) \to Unit (R) \subseteq RLReg (R)$
27	14 7	unitinvcl	$⊢ (R \in Ring \land {coe}_{1} (X) (D (X)) \in Unit (R)) \to I ({coe}_{1} (X) (D (X))) \in Unit (R)$
28	15 27	sylan2	$⊢ (R \in Ring \land X \in C) \to I ({coe}_{1} (X) (D (X))) \in Unit (R)$
29	26 28	sseldd	$⊢ (R \in Ring \land X \in C) \to I ({coe}_{1} (X) (D (X))) \in RLReg (R)$
30	6 3 24 11 4 5	deg1mul3	$⊢ (R \in Ring \land I ({coe}_{1} (X) (D (X))) \in RLReg (R) \land X \in {Base}_{P}) \to D (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) = D (X)$
31	23 29 20 30	syl3anc	$⊢ (R \in Ring \land X \in C) \to D (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) = D (X)$
32	6 1	uc1pdeg	$⊢ (R \in Ring \land X \in C) \to D (X) \in ℕ_{0}$
33	31 32	eqeltrd	$⊢ (R \in Ring \land X \in C) \to D (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) \in ℕ_{0}$
34		eqid	$⊢ 0_{P} = 0_{P}$
35	6 3 34 11	deg1nn0clb	$⊢ (R \in Ring \land A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \in {Base}_{P}) \to (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \neq 0_{P} \leftrightarrow D (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) \in ℕ_{0})$
36	22 35	syldan	$⊢ (R \in Ring \land X \in C) \to (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \neq 0_{P} \leftrightarrow D (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) \in ℕ_{0})$
37	33 36	mpbird	$⊢ (R \in Ring \land X \in C) \to A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \neq 0_{P}$
38	31	fveq2d	$⊢ (R \in Ring \land X \in C) \to {coe}_{1} (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) (D (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X)) = {coe}_{1} (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) (D (X))$
39		eqid	$⊢ \cdot_{R} = \cdot_{R}$
40	3 11 10 5 4 39	coe1sclmul	$⊢ (R \in Ring \land I ({coe}_{1} (X) (D (X))) \in {Base}_{R} \land X \in {Base}_{P}) \to {coe}_{1} (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) = (ℕ_{0} \times \{I ({coe}_{1} (X) (D (X)))\}) {\cdot_{R}}_{f} {coe}_{1} (X)$
41	23 17 20 40	syl3anc	$⊢ (R \in Ring \land X \in C) \to {coe}_{1} (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) = (ℕ_{0} \times \{I ({coe}_{1} (X) (D (X)))\}) {\cdot_{R}}_{f} {coe}_{1} (X)$
42	41	fveq1d	$⊢ (R \in Ring \land X \in C) \to {coe}_{1} (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) (D (X)) = ((ℕ_{0} \times \{I ({coe}_{1} (X) (D (X)))\}) {\cdot_{R}}_{f} {coe}_{1} (X)) (D (X))$
43		nn0ex	$⊢ ℕ_{0} \in V$
44	43	a1i	$⊢ (R \in Ring \land X \in C) \to ℕ_{0} \in V$
45		fvexd	$⊢ (R \in Ring \land X \in C) \to I ({coe}_{1} (X) (D (X))) \in V$
46		eqid	$⊢ {coe}_{1} (X) = {coe}_{1} (X)$
47	46 11 3 10	coe1f	$⊢ X \in {Base}_{P} \to {coe}_{1} (X) : ℕ_{0} ⟶ {Base}_{R}$
48		ffn	$⊢ {coe}_{1} (X) : ℕ_{0} ⟶ {Base}_{R} \to {coe}_{1} (X) Fn ℕ_{0}$
49	20 47 48	3syl	$⊢ (R \in Ring \land X \in C) \to {coe}_{1} (X) Fn ℕ_{0}$
50		eqidd	$⊢ ((R \in Ring \land X \in C) \land D (X) \in ℕ_{0}) \to {coe}_{1} (X) (D (X)) = {coe}_{1} (X) (D (X))$
51	44 45 49 50	ofc1	$⊢ ((R \in Ring \land X \in C) \land D (X) \in ℕ_{0}) \to ((ℕ_{0} \times \{I ({coe}_{1} (X) (D (X)))\}) {\cdot_{R}}_{f} {coe}_{1} (X)) (D (X)) = I ({coe}_{1} (X) (D (X))) \cdot_{R} {coe}_{1} (X) (D (X))$
52	32 51	mpdan	$⊢ (R \in Ring \land X \in C) \to ((ℕ_{0} \times \{I ({coe}_{1} (X) (D (X)))\}) {\cdot_{R}}_{f} {coe}_{1} (X)) (D (X)) = I ({coe}_{1} (X) (D (X))) \cdot_{R} {coe}_{1} (X) (D (X))$
53		eqid	$⊢ 1_{R} = 1_{R}$
54	14 7 39 53	unitlinv	$⊢ (R \in Ring \land {coe}_{1} (X) (D (X)) \in Unit (R)) \to I ({coe}_{1} (X) (D (X))) \cdot_{R} {coe}_{1} (X) (D (X)) = 1_{R}$
55	15 54	sylan2	$⊢ (R \in Ring \land X \in C) \to I ({coe}_{1} (X) (D (X))) \cdot_{R} {coe}_{1} (X) (D (X)) = 1_{R}$
56	52 55	eqtrd	$⊢ (R \in Ring \land X \in C) \to ((ℕ_{0} \times \{I ({coe}_{1} (X) (D (X)))\}) {\cdot_{R}}_{f} {coe}_{1} (X)) (D (X)) = 1_{R}$
57	38 42 56	3eqtrd	$⊢ (R \in Ring \land X \in C) \to {coe}_{1} (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) (D (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X)) = 1_{R}$
58	3 11 34 6 2 53	ismon1p	$⊢ A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \in M \leftrightarrow (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \in {Base}_{P} \land A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \neq 0_{P} \land {coe}_{1} (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X) (D (A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X)) = 1_{R})$
59	22 37 57 58	syl3anbrc	$⊢ (R \in Ring \land X \in C) \to A (I ({coe}_{1} (X) (D (X)))) \underset{˙}{\cdot} X \in M$

Metamath Proof Explorer

Theorem uc1pmon1p

Proof