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 = Poly 1 ⁡ R
Assertion ply1nzb ⊢ R ∈ Ring → R ∈ NzRing ↔ P ∈ NzRing

Proof

Step Hyp Ref Expression
1 ply1domn.p ⊢ P = Poly 1 ⁡ R
2 1 ply1nz ⊢ R ∈ NzRing → P ∈ NzRing
3 simpl ⊢ R ∈ Ring ∧ P ∈ NzRing → R ∈ Ring
4 eqid ⊢ 1 P = 1 P
5 eqid ⊢ 0 P = 0 P
6 4 5 nzrnz ⊢ P ∈ NzRing → 1 P ≠ 0 P
7 6 adantl ⊢ R ∈ Ring ∧ P ∈ NzRing → 1 P ≠ 0 P
8 ifeq1 ⊢ 1 R = 0 R → if y = 1 𝑜 × 0 1 R 0 R = if y = 1 𝑜 × 0 0 R 0 R
9 ifid ⊢ if y = 1 𝑜 × 0 0 R 0 R = 0 R
10 8 9 eqtrdi ⊢ 1 R = 0 R → if y = 1 𝑜 × 0 1 R 0 R = 0 R
11 10 ralrimivw ⊢ 1 R = 0 R → ∀ y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin if y = 1 𝑜 × 0 1 R 0 R = 0 R
12 eqid ⊢ 1 𝑜 mPoly R = 1 𝑜 mPoly R
13 eqid ⊢ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin = x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin
14 eqid ⊢ 0 R = 0 R
15 eqid ⊢ 1 R = 1 R
16 12 1 4 ply1mpl1 ⊢ 1 P = 1 1 𝑜 mPoly R
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 → 1 P = y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin ⟼ if y = 1 𝑜 × 0 1 R 0 R
20 12 1 5 ply1mpl0 ⊢ 0 P = 0 1 𝑜 mPoly R
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 → 0 P = x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin × 0 R
24 fconstmpt ⊢ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin × 0 R = y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin ⟼ 0 R
25 23 24 eqtrdi ⊢ R ∈ Ring ∧ P ∈ NzRing → 0 P = y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin ⟼ 0 R
26 19 25 eqeq12d ⊢ R ∈ Ring ∧ P ∈ NzRing → 1 P = 0 P ↔ y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin ⟼ if y = 1 𝑜 × 0 1 R 0 R = y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin ⟼ 0 R
27 fvex ⊢ 1 R ∈ V
28 fvex ⊢ 0 R ∈ V
29 27 28 ifex ⊢ if y = 1 𝑜 × 0 1 R 0 R ∈ V
30 29 rgenw ⊢ ∀ y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin if y = 1 𝑜 × 0 1 R 0 R ∈ V
31 mpteqb ⊢ ∀ y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin if y = 1 𝑜 × 0 1 R 0 R ∈ V → y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin ⟼ if y = 1 𝑜 × 0 1 R 0 R = y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin ⟼ 0 R ↔ ∀ y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin if y = 1 𝑜 × 0 1 R 0 R = 0 R
32 30 31 ax-mp ⊢ y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin ⟼ if y = 1 𝑜 × 0 1 R 0 R = y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin ⟼ 0 R ↔ ∀ y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin if y = 1 𝑜 × 0 1 R 0 R = 0 R
33 26 32 bitrdi ⊢ R ∈ Ring ∧ P ∈ NzRing → 1 P = 0 P ↔ ∀ y ∈ x ∈ ℕ 0 1 𝑜 | x -1 ℕ ∈ Fin if y = 1 𝑜 × 0 1 R 0 R = 0 R
34 11 33 syl5ibr ⊢ R ∈ Ring ∧ P ∈ NzRing → 1 R = 0 R → 1 P = 0 P
35 34 necon3d ⊢ R ∈ Ring ∧ P ∈ NzRing → 1 P ≠ 0 P → 1 R ≠ 0 R
36 7 35 mpd ⊢ R ∈ Ring ∧ P ∈ NzRing → 1 R ≠ 0 R
37 15 14 isnzr ⊢ R ∈ NzRing ↔ R ∈ Ring ∧ 1 R ≠ 0 R
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