Theorem 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	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
	uc1pmon1p.m	⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
	uc1pmon1p.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	uc1pmon1p.t	⊢ · = ( .r ‘ 𝑃 )
	uc1pmon1p.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	uc1pmon1p.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	uc1pmon1p.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
Assertion	uc1pmon1p	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		uc1pmon1p.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
2		uc1pmon1p.m	⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
3		uc1pmon1p.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		uc1pmon1p.t	⊢ · = ( .r ‘ 𝑃 )
5		uc1pmon1p.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
6		uc1pmon1p.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
7		uc1pmon1p.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
8	3	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
9	8	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → 𝑃 ∈ Ring )
10		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
12	3 5 10 11	ply1sclf	⊢ ( 𝑅 ∈ Ring → 𝐴 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
13	12	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → 𝐴 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑃 ) )
14		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
15	6 14 1	uc1pldg	⊢ ( 𝑋 ∈ 𝐶 → ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ∈ ( Unit ‘ 𝑅 ) )
16	14 7 10	ringinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝑅 ) )
17	15 16	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝑅 ) )
18	13 17	ffvelcdmd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
19	3 11 1	uc1pcl	⊢ ( 𝑋 ∈ 𝐶 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
20	19	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
21	11 4	ringcl	⊢ ( ( 𝑃 ∈ Ring ∧ ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
22	9 18 20 21	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
23		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → 𝑅 ∈ Ring )
24		eqid	⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
25	24 14	unitrrg	⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) )
26	25	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) )
27	14 7	unitinvcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( Unit ‘ 𝑅 ) )
28	15 27	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( Unit ‘ 𝑅 ) )
29	26 28	sseldd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( RLReg ‘ 𝑅 ) )
30	6 3 24 11 4 5	deg1mul3	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( RLReg ‘ 𝑅 ) ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) = ( 𝐷 ‘ 𝑋 ) )
31	23 29 20 30	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) = ( 𝐷 ‘ 𝑋 ) )
32	6 1	uc1pdeg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐷 ‘ 𝑋 ) ∈ ℕ0 )
33	31 32	eqeltrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ∈ ℕ0 )
34		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
35	6 3 34 11	deg1nn0clb	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ≠ ( 0g ‘ 𝑃 ) ↔ ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ∈ ℕ0 ) )
36	22 35	syldan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ≠ ( 0g ‘ 𝑃 ) ↔ ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ∈ ℕ0 ) )
37	33 36	mpbird	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ≠ ( 0g ‘ 𝑃 ) )
38	31	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ‘ ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ) = ( ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) )
39		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
40	3 11 10 5 4 39	coe1sclmul	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) = ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) )
41	23 17 20 40	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) = ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) )
42	41	fveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) = ( ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) )
43		nn0ex	⊢ ℕ0 ∈ V
44	43	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ℕ0 ∈ V )
45		fvexd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ∈ V )
46		eqid	⊢ ( coe1 ‘ 𝑋 ) = ( coe1 ‘ 𝑋 )
47	46 11 3 10	coe1f	⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( coe1 ‘ 𝑋 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
48		ffn	⊢ ( ( coe1 ‘ 𝑋 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) → ( coe1 ‘ 𝑋 ) Fn ℕ0 )
49	20 47 48	3syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( coe1 ‘ 𝑋 ) Fn ℕ0 )
50		eqidd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ℕ0 ) → ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) = ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) )
51	44 45 49 50	ofc1	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) ∧ ( 𝐷 ‘ 𝑋 ) ∈ ℕ0 ) → ( ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) )
52	32 51	mpdan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) = ( ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) )
53		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
54	14 7 39 53	unitlinv	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) = ( 1r ‘ 𝑅 ) )
55	15 54	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ( .r ‘ 𝑅 ) ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) = ( 1r ‘ 𝑅 ) )
56	52 55	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( ( ℕ0 × { ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) } ) ∘f ( .r ‘ 𝑅 ) ( coe1 ‘ 𝑋 ) ) ‘ ( 𝐷 ‘ 𝑋 ) ) = ( 1r ‘ 𝑅 ) )
57	38 42 56	3eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ‘ ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ) = ( 1r ‘ 𝑅 ) )
58	3 11 34 6 2 53	ismon1p	⊢ ( ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ 𝑀 ↔ ( ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ≠ ( 0g ‘ 𝑃 ) ∧ ( ( coe1 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ‘ ( 𝐷 ‘ ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ) ) = ( 1r ‘ 𝑅 ) ) )
59	22 37 57 58	syl3anbrc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐴 ‘ ( 𝐼 ‘ ( ( coe1 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ 𝑀 )