Theorem psrnzr

Description: The ring of power series over a nonzero ring form a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Hypotheses	psrnzr.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	psrnzr.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	psrnzr.r	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
Assertion	psrnzr	⊢ ( 𝜑 → 𝑆 ∈ NzRing )

Proof

Step	Hyp	Ref	Expression
1		psrnzr.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		psrnzr.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		psrnzr.r	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
4		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
5	3 4	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6	1 2 5	psrring	⊢ ( 𝜑 → 𝑆 ∈ Ring )
7		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9	7 8	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
10	3 9	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
11		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
12		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
13	1 2 5 11 8 7 12	psr1	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝐼 × { 0 } ) ) → 𝑥 = ( 𝐼 × { 0 } ) )
15	14	iftrued	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝐼 × { 0 } ) ) → if ( 𝑥 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
16	11	psrbag0	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { 0 } ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
17	2 16	syl	⊢ ( 𝜑 → ( 𝐼 × { 0 } ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
18		fvexd	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ V )
19	13 15 17 18	fvmptd	⊢ ( 𝜑 → ( ( 1r ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) = ( 1r ‘ 𝑅 ) )
20	5	ringgrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
21		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
22	1 2 20 11 8 21	psr0	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) )
23	22	fveq1d	⊢ ( 𝜑 → ( ( 0g ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐼 × { 0 } ) ) )
24		fvex	⊢ ( 0g ‘ 𝑅 ) ∈ V
25	24	fvconst2	⊢ ( ( 𝐼 × { 0 } ) ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } → ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐼 × { 0 } ) ) = ( 0g ‘ 𝑅 ) )
26	17 25	syl	⊢ ( 𝜑 → ( ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐼 × { 0 } ) ) = ( 0g ‘ 𝑅 ) )
27	23 26	eqtrd	⊢ ( 𝜑 → ( ( 0g ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) = ( 0g ‘ 𝑅 ) )
28	10 19 27	3netr4d	⊢ ( 𝜑 → ( ( 1r ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) ≠ ( ( 0g ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) )
29		fveq1	⊢ ( ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑆 ) → ( ( 1r ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) = ( ( 0g ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) )
30	29	necon3i	⊢ ( ( ( 1r ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) ≠ ( ( 0g ‘ 𝑆 ) ‘ ( 𝐼 × { 0 } ) ) → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
31	28 30	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
32	12 21	isnzr	⊢ ( 𝑆 ∈ NzRing ↔ ( 𝑆 ∈ Ring ∧ ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) ) )
33	6 31 32	sylanbrc	⊢ ( 𝜑 → 𝑆 ∈ NzRing )