Metamath Proof Explorer

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 ‘ 𝑋 ) ‘ ( 𝐷 ‘ 𝑋 ) ) ) ) · 𝑋 ) ∈ 𝑀 )