This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
Assertion ply1nzb ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ 𝑃 ∈ NzRing ) )

Proof

Step Hyp Ref Expression
1 ply1domn.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 1 ply1nz ⊢ ( 𝑅 ∈ NzRing → 𝑃 ∈ NzRing )
3 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → 𝑅 ∈ Ring )
4 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
5 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
6 4 5 nzrnz ⊢ ( 𝑃 ∈ NzRing → ( 1r ‘ 𝑃 ) ≠ ( 0g ‘ 𝑃 ) )
7 6 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → ( 1r ‘ 𝑃 ) ≠ ( 0g ‘ 𝑃 ) )
8 ifeq1 ⊢ ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑦 = ( 1o × { 0 } ) , ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
9 ifid ⊢ if ( 𝑦 = ( 1o × { 0 } ) , ( 0g ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 )
10 8 9 eqtrdi ⊢ ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
11 10 ralrimivw ⊢ ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → ∀ 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
12 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
13 eqid ⊢ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } = { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin }
14 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
15 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
16 12 1 4 ply1mpl1 ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ ( 1o mPoly 𝑅 ) )
17 1on ⊢ 1o ∈ On
18 17 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → 1o ∈ On )
19 12 13 14 15 16 18 3 mpl1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → ( 1r ‘ 𝑃 ) = ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
20 12 1 5 ply1mpl0 ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ ( 1o mPoly 𝑅 ) )
21 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
22 3 21 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → 𝑅 ∈ Grp )
23 12 13 14 20 18 22 mpl0 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → ( 0g ‘ 𝑃 ) = ( { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) )
24 fconstmpt ⊢ ( { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) = ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( 0g ‘ 𝑅 ) )
25 23 24 eqtrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( 0g ‘ 𝑅 ) ) )
26 19 25 eqeq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → ( ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑃 ) ↔ ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( 0g ‘ 𝑅 ) ) ) )
27 fvex ⊢ ( 1r ‘ 𝑅 ) ∈ V
28 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
29 27 28 ifex ⊢ if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ V
30 29 rgenw ⊢ ∀ 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ V
31 mpteqb ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ V → ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
32 30 31 ax-mp ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } ↦ ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
33 26 32 bitrdi ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → ( ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑃 ) ↔ ∀ 𝑦 ∈ { 𝑥 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑥 “ ℕ ) ∈ Fin } if ( 𝑦 = ( 1o × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
34 11 33 imbitrrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → ( ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) → ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑃 ) ) )
35 34 necon3d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → ( ( 1r ‘ 𝑃 ) ≠ ( 0g ‘ 𝑃 ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
36 7 35 mpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
37 15 14 isnzr ⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) ) )
38 3 36 37 sylanbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑃 ∈ NzRing ) → 𝑅 ∈ NzRing )
39 38 ex ⊢ ( 𝑅 ∈ Ring → ( 𝑃 ∈ NzRing → 𝑅 ∈ NzRing ) )
40 2 39 impbid2 ⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ 𝑃 ∈ NzRing ) )