Metamath Proof Explorer

Theorem ply1nzb

Description: Univariate polynomials are nonzero iff the base is nonzero. Or in contraposition, the univariate polynomials over the zero ring are also zero. (Contributed by Mario Carneiro, 13-Jun-2015)

Ref Expression
Hypothesis ply1domn.p ⊢P=Poly1⁡R
Assertion ply1nzb ⊢R∈Ring→R∈NzRing↔P∈NzRing

Proof

Step Hyp Ref Expression
1 ply1domn.p ⊢P=Poly1⁡R
2 1 ply1nz ⊢R∈NzRing→P∈NzRing
3 simpl ⊢R∈Ring∧P∈NzRing→R∈Ring
4 eqid ⊢1P=1P
5 eqid ⊢0P=0P
6 4 5 nzrnz ⊢P∈NzRing→1P≠0P
7 6 adantl ⊢R∈Ring∧P∈NzRing→1P≠0P
8 ifeq1 ⊢1R=0R→ify=1𝑜×01R0R=ify=1𝑜×00R0R
9 ifid ⊢ify=1𝑜×00R0R=0R
10 8 9 eqtrdi ⊢1R=0R→ify=1𝑜×01R0R=0R
11 10 ralrimivw ⊢1R=0R→∀y∈x∈ℕ01𝑜|x-1ℕ∈Finify=1𝑜×01R0R=0R
12 eqid ⊢1𝑜mPolyR=1𝑜mPolyR
13 eqid ⊢x∈ℕ01𝑜|x-1ℕ∈Fin=x∈ℕ01𝑜|x-1ℕ∈Fin
14 eqid ⊢0R=0R
15 eqid ⊢1R=1R
16 12 1 4 ply1mpl1 ⊢1P=11𝑜mPolyR
17 1on ⊢1𝑜∈On
18 17 a1i ⊢R∈Ring∧P∈NzRing→1𝑜∈On
19 12 13 14 15 16 18 3 mpl1 ⊢R∈Ring∧P∈NzRing→1P=y∈x∈ℕ01𝑜|x-1ℕ∈Fin⟼ify=1𝑜×01R0R
20 12 1 5 ply1mpl0 ⊢0P=01𝑜mPolyR
21 ringgrp ⊢R∈Ring→R∈Grp
22 3 21 syl ⊢R∈Ring∧P∈NzRing→R∈Grp
23 12 13 14 20 18 22 mpl0 ⊢R∈Ring∧P∈NzRing→0P=x∈ℕ01𝑜|x-1ℕ∈Fin×0R
24 fconstmpt ⊢x∈ℕ01𝑜|x-1ℕ∈Fin×0R=y∈x∈ℕ01𝑜|x-1ℕ∈Fin⟼0R
25 23 24 eqtrdi ⊢R∈Ring∧P∈NzRing→0P=y∈x∈ℕ01𝑜|x-1ℕ∈Fin⟼0R
26 19 25 eqeq12d ⊢R∈Ring∧P∈NzRing→1P=0P↔y∈x∈ℕ01𝑜|x-1ℕ∈Fin⟼ify=1𝑜×01R0R=y∈x∈ℕ01𝑜|x-1ℕ∈Fin⟼0R
27 fvex ⊢1R∈V
28 fvex ⊢0R∈V
29 27 28 ifex ⊢ify=1𝑜×01R0R∈V
30 29 rgenw ⊢∀y∈x∈ℕ01𝑜|x-1ℕ∈Finify=1𝑜×01R0R∈V
31 mpteqb ⊢∀y∈x∈ℕ01𝑜|x-1ℕ∈Finify=1𝑜×01R0R∈V→y∈x∈ℕ01𝑜|x-1ℕ∈Fin⟼ify=1𝑜×01R0R=y∈x∈ℕ01𝑜|x-1ℕ∈Fin⟼0R↔∀y∈x∈ℕ01𝑜|x-1ℕ∈Finify=1𝑜×01R0R=0R
32 30 31 ax-mp ⊢y∈x∈ℕ01𝑜|x-1ℕ∈Fin⟼ify=1𝑜×01R0R=y∈x∈ℕ01𝑜|x-1ℕ∈Fin⟼0R↔∀y∈x∈ℕ01𝑜|x-1ℕ∈Finify=1𝑜×01R0R=0R
33 26 32 bitrdi ⊢R∈Ring∧P∈NzRing→1P=0P↔∀y∈x∈ℕ01𝑜|x-1ℕ∈Finify=1𝑜×01R0R=0R
34 11 33 imbitrrid ⊢R∈Ring∧P∈NzRing→1R=0R→1P=0P
35 34 necon3d ⊢R∈Ring∧P∈NzRing→1P≠0P→1R≠0R
36 7 35 mpd ⊢R∈Ring∧P∈NzRing→1R≠0R
37 15 14 isnzr ⊢R∈NzRing↔R∈Ring∧1R≠0R
38 3 36 37 sylanbrc ⊢R∈Ring∧P∈NzRing→R∈NzRing
39 38 ex ⊢R∈Ring→P∈NzRing→R∈NzRing
40 2 39 impbid2 ⊢R∈Ring→R∈NzRing↔P∈NzRing