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	$$⊢S=I\mathrm{mPwSer}R$$
	psrnzr.i	$$⊢\phi \to I\in V$$
	psrnzr.r	$$⊢\phi \to R\in \mathrm{NzRing}$$
Assertion	psrnzr	$$⊢\phi \to S\in \mathrm{NzRing}$$

Proof

Step	Hyp	Ref	Expression
1		psrnzr.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrnzr.i	$$⊢\phi \to I\in V$$
3		psrnzr.r	$$⊢\phi \to R\in \mathrm{NzRing}$$
4		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
5	3 4	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
6	1 2 5	psrring	$$⊢\phi \to S\in \mathrm{Ring}$$
7		eqid	$$⊢1_R=1_R$$
8		eqid	$$⊢0_R=0_R$$
9	7 8	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne 0_R$$
10	3 9	syl	$$⊢\phi \to 1_R\ne 0_R$$
11		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
12		eqid	$$⊢1_S=1_S$$
13	1 2 5 11 8 7 12	psr1	$$⊢\phi \to 1_S=\left(x\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼if\left(x=I\times \left\{0\right\},1_R,0_R\right)\right)$$
14		simpr	$$⊢\left(\phi \wedge x=I\times \left\{0\right\}\right)\to x=I\times \left\{0\right\}$$
15	14	iftrued	$$⊢\left(\phi \wedge x=I\times \left\{0\right\}\right)\to if\left(x=I\times \left\{0\right\},1_R,0_R\right)=1_R$$
16	11	psrbag0	$$⊢I\in V\to I\times \left\{0\right\}\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
17	2 16	syl	$$⊢\phi \to I\times \left\{0\right\}\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
18		fvexd	$$⊢\phi \to 1_R\in \mathrm{V}$$
19	13 15 17 18	fvmptd	$$⊢\phi \to 1_S\left(I\times \left\{0\right\}\right)=1_R$$
20	5	ringgrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
21		eqid	$$⊢0_S=0_S$$
22	1 2 20 11 8 21	psr0	$$⊢\phi \to 0_S=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{0_R\right\}$$
23	22	fveq1d	$$⊢\phi \to 0_S\left(I\times \left\{0\right\}\right)=\left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{0_R\right\}\right)\left(I\times \left\{0\right\}\right)$$
24		fvex	$$⊢0_R\in \mathrm{V}$$
25	24	fvconst2	$$⊢I\times \left\{0\right\}\in \left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\to \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{0_R\right\}\right)\left(I\times \left\{0\right\}\right)=0_R$$
26	17 25	syl	$$⊢\phi \to \left(\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\times \left\{0_R\right\}\right)\left(I\times \left\{0\right\}\right)=0_R$$
27	23 26	eqtrd	$$⊢\phi \to 0_S\left(I\times \left\{0\right\}\right)=0_R$$
28	10 19 27	3netr4d	$$⊢\phi \to 1_S\left(I\times \left\{0\right\}\right)\ne 0_S\left(I\times \left\{0\right\}\right)$$
29		fveq1	$$⊢1_S=0_S\to 1_S\left(I\times \left\{0\right\}\right)=0_S\left(I\times \left\{0\right\}\right)$$
30	29	necon3i	$$⊢1_S\left(I\times \left\{0\right\}\right)\ne 0_S\left(I\times \left\{0\right\}\right)\to 1_S\ne 0_S$$
31	28 30	syl	$$⊢\phi \to 1_S\ne 0_S$$
32	12 21	isnzr	$$⊢S\in \mathrm{NzRing}\leftrightarrow \left(S\in \mathrm{Ring}\wedge 1_S\ne 0_S\right)$$
33	6 31 32	sylanbrc	$$⊢\phi \to S\in \mathrm{NzRing}$$