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