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 ) )