Theorem domnexpgn0cl

Description: In a domain, a (nonnegative) power of a nonzero element is nonzero. (Contributed by SN, 6-Jul-2024)

	Ref	Expression
Hypotheses	domnexpgn0cl.b	$$⊢B={\mathrm{Base}}_R$$
	domnexpgn0cl.0	$$⊢\underset{\dot{}}{0}=0_R$$
	domnexpgn0cl.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
	domnexpgn0cl.r	$$⊢\phi \to R\in \mathrm{Domn}$$
	domnexpgn0cl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	domnexpgn0cl.x	$$⊢\phi \to X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	domnexpgn0cl	$$⊢\phi \to N\underset{\dot{}}{\times }X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		domnexpgn0cl.b	$$⊢B={\mathrm{Base}}_R$$
2		domnexpgn0cl.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		domnexpgn0cl.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
4		domnexpgn0cl.r	$$⊢\phi \to R\in \mathrm{Domn}$$
5		domnexpgn0cl.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
6		domnexpgn0cl.x	$$⊢\phi \to X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
7		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
8	7 1	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
9		domnring	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{Ring}$$
10	7	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
11	4 9 10	3syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
12	6	eldifad	$$⊢\phi \to X\in B$$
13	8 3 11 5 12	mulgnn0cld	$$⊢\phi \to N\underset{\dot{}}{\times }X\in B$$
14		oveq1	$$⊢x=0\to x\underset{\dot{}}{\times }X=0\underset{\dot{}}{\times }X$$
15	14	neeq1d	$$⊢x=0\to \left(x\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\leftrightarrow 0\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)$$
16		oveq1	$$⊢x=y\to x\underset{\dot{}}{\times }X=y\underset{\dot{}}{\times }X$$
17	16	neeq1d	$$⊢x=y\to \left(x\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\leftrightarrow y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)$$
18		oveq1	$$⊢x=y+1\to x\underset{\dot{}}{\times }X=\left(y+1\right)\underset{\dot{}}{\times }X$$
19	18	neeq1d	$$⊢x=y+1\to \left(x\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\leftrightarrow \left(y+1\right)\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)$$
20		oveq1	$$⊢x=N\to x\underset{\dot{}}{\times }X=N\underset{\dot{}}{\times }X$$
21	20	neeq1d	$$⊢x=N\to \left(x\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\leftrightarrow N\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)$$
22		eqid	$$⊢1_R=1_R$$
23	7 22	ringidval	$$⊢1_R=0_{{\mathrm{mulGrp}}_R}$$
24	8 23 3	mulg0	$$⊢X\in B\to 0\underset{\dot{}}{\times }X=1_R$$
25	12 24	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }X=1_R$$
26		domnnzr	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$
27	22 2	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne \underset{\dot{}}{0}$$
28	4 26 27	3syl	$$⊢\phi \to 1_R\ne \underset{\dot{}}{0}$$
29	25 28	eqnetrd	$$⊢\phi \to 0\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}$$
30	11	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
31		simplr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\to y\in {\mathbb{N}}_0$$
32	12	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\to X\in B$$
33		eqid	$$⊢{\cdot }_R={\cdot }_R$$
34	7 33	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
35	8 3 34	mulgnn0p1	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge X\in B\right)\to \left(y+1\right)\underset{\dot{}}{\times }X=\left(y\underset{\dot{}}{\times }X\right){\cdot }_{R}X$$
36	30 31 32 35	syl3anc	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\to \left(y+1\right)\underset{\dot{}}{\times }X=\left(y\underset{\dot{}}{\times }X\right){\cdot }_{R}X$$
37	4	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\to R\in \mathrm{Domn}$$
38	8 3 30 31 32	mulgnn0cld	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\to y\underset{\dot{}}{\times }X\in B$$
39		simpr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\to y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}$$
40		eldifsni	$$⊢X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
41	6 40	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
42	41	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\to X\ne \underset{\dot{}}{0}$$
43	1 33 2	domnmuln0	$$⊢\left(R\in \mathrm{Domn}\wedge \left(y\underset{\dot{}}{\times }X\in B\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\wedge \left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)\right)\to \left(y\underset{\dot{}}{\times }X\right){\cdot }_{R}X\ne \underset{\dot{}}{0}$$
44	37 38 39 32 42 43	syl122anc	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\to \left(y\underset{\dot{}}{\times }X\right){\cdot }_{R}X\ne \underset{\dot{}}{0}$$
45	36 44	eqnetrd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}\right)\to \left(y+1\right)\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}$$
46	15 17 19 21 29 45	nn0indd	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\right)\to N\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}$$
47	5 46	mpdan	$$⊢\phi \to N\underset{\dot{}}{\times }X\ne \underset{\dot{}}{0}$$
48	13 47	eldifsnd	$$⊢\phi \to N\underset{\dot{}}{\times }X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$