# Metamath Proof Explorer

## Theorem cply1coe0bi

Description: A polynomial is constant (i.e. a "lifted scalar") iff all but the first coefficient are zero. (Contributed by AV, 16-Nov-2019)

Ref Expression
Hypotheses cply1coe0.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
cply1coe0.0
cply1coe0.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
cply1coe0.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
cply1coe0.a ${⊢}{A}=\mathrm{algSc}\left({P}\right)$
Assertion cply1coe0bi

### Proof

Step Hyp Ref Expression
1 cply1coe0.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
2 cply1coe0.0
3 cply1coe0.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
4 cply1coe0.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
5 cply1coe0.a ${⊢}{A}=\mathrm{algSc}\left({P}\right)$
6 1 2 3 4 5 cply1coe0
8 fveq2 ${⊢}{M}={A}\left({s}\right)\to {\mathrm{coe}}_{1}\left({M}\right)={\mathrm{coe}}_{1}\left({A}\left({s}\right)\right)$
9 8 fveq1d ${⊢}{M}={A}\left({s}\right)\to {\mathrm{coe}}_{1}\left({M}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({A}\left({s}\right)\right)\left({n}\right)$
10 9 eqeq1d
11 10 ralbidv
13 7 12 mpbird
14 13 rexlimdva2
15 simpr ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {M}\in {B}$
16 0nn0 ${⊢}0\in {ℕ}_{0}$
17 eqid ${⊢}{\mathrm{coe}}_{1}\left({M}\right)={\mathrm{coe}}_{1}\left({M}\right)$
18 17 4 3 1 coe1fvalcl ${⊢}\left({M}\in {B}\wedge 0\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\in {K}$
19 15 16 18 sylancl ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\in {K}$
21 fveq2 ${⊢}{s}={\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\to {A}\left({s}\right)={A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)$
22 21 eqeq2d ${⊢}{s}={\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\to \left({M}={A}\left({s}\right)↔{M}={A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)$
24 simpl ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {R}\in \mathrm{Ring}$
25 eqid ${⊢}\mathrm{Scalar}\left({P}\right)=\mathrm{Scalar}\left({P}\right)$
26 3 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
27 3 ply1lmod ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{LMod}$
28 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
29 5 25 26 27 28 4 asclf ${⊢}{R}\in \mathrm{Ring}\to {A}:{\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}⟶{B}$
30 29 adantr ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {A}:{\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}⟶{B}$
31 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
32 17 4 3 31 coe1fvalcl ${⊢}\left({M}\in {B}\wedge 0\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\in {\mathrm{Base}}_{{R}}$
33 15 16 32 sylancl ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\in {\mathrm{Base}}_{{R}}$
34 3 ply1sca ${⊢}{R}\in \mathrm{Ring}\to {R}=\mathrm{Scalar}\left({P}\right)$
35 34 eqcomd ${⊢}{R}\in \mathrm{Ring}\to \mathrm{Scalar}\left({P}\right)={R}$
36 35 fveq2d ${⊢}{R}\in \mathrm{Ring}\to {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{{R}}$
37 36 adantr ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{{R}}$
38 33 37 eleqtrrd ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
39 30 38 ffvelrnd ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\in {B}$
40 24 15 39 3jca ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to \left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\in {B}\right)$
42 simpr
43 3 5 1 2 coe1scl
44 19 43 syldan
46 nnne0 ${⊢}{n}\in ℕ\to {n}\ne 0$
47 46 neneqd ${⊢}{n}\in ℕ\to ¬{n}=0$
48 47 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {n}\in ℕ\right)\to ¬{n}=0$
49 48 adantr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {n}\in ℕ\right)\wedge {k}={n}\right)\to ¬{n}=0$
50 eqeq1 ${⊢}{k}={n}\to \left({k}=0↔{n}=0\right)$
51 50 notbid ${⊢}{k}={n}\to \left(¬{k}=0↔¬{n}=0\right)$
52 51 adantl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {n}\in ℕ\right)\wedge {k}={n}\right)\to \left(¬{k}=0↔¬{n}=0\right)$
53 49 52 mpbird ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {n}\in ℕ\right)\wedge {k}={n}\right)\to ¬{k}=0$
54 53 iffalsed
55 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
56 55 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {n}\in ℕ\right)\to {n}\in {ℕ}_{0}$
57 2 fvexi
58 57 a1i
59 45 54 56 58 fvmptd
60 59 eqcomd
62 42 61 eqtrd
63 62 ex
64 63 ralimdva
65 64 imp
66 3 5 1 ply1sclid ${⊢}\left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\in {K}\right)\to {\mathrm{coe}}_{1}\left({M}\right)\left(0\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left(0\right)$
67 19 66 syldan ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {\mathrm{coe}}_{1}\left({M}\right)\left(0\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left(0\right)$
69 df-n0 ${⊢}{ℕ}_{0}=ℕ\cup \left\{0\right\}$
70 69 raleqi ${⊢}\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({M}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left({n}\right)↔\forall {n}\in \left(ℕ\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({M}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left({n}\right)$
71 c0ex ${⊢}0\in \mathrm{V}$
72 fveq2 ${⊢}{n}=0\to {\mathrm{coe}}_{1}\left({M}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({M}\right)\left(0\right)$
73 fveq2 ${⊢}{n}=0\to {\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left({n}\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left(0\right)$
74 72 73 eqeq12d ${⊢}{n}=0\to \left({\mathrm{coe}}_{1}\left({M}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left({n}\right)↔{\mathrm{coe}}_{1}\left({M}\right)\left(0\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left(0\right)\right)$
75 74 ralunsn ${⊢}0\in \mathrm{V}\to \left(\forall {n}\in \left(ℕ\cup \left\{0\right\}\right)\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({M}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left({n}\right)↔\left(\forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({M}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left({n}\right)\wedge {\mathrm{coe}}_{1}\left({M}\right)\left(0\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left(0\right)\right)\right)$
76 71 75 mp1i
77 70 76 syl5bb
78 65 68 77 mpbir2and
79 eqid ${⊢}{\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)$
80 3 4 17 79 eqcoe1ply1eq ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\in {B}\right)\to \left(\forall {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({M}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)\left({n}\right)\to {M}={A}\left({\mathrm{coe}}_{1}\left({M}\right)\left(0\right)\right)\right)$
81 41 78 80 sylc
82 20 23 81 rspcedvd
83 82 ex
84 14 83 impbid