Theorem idomnnzpownz

Description: A non-zero power in an integral domain is non-zero. (Contributed by metakunt, 5-May-2025)

	Ref	Expression
Hypotheses	idomnnzpownz.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
	idomnnzpownz.2	$$⊢\phi \to A\in {\mathrm{Base}}_R$$
	idomnnzpownz.3	$$⊢\phi \to A\ne 0_R$$
	idomnnzpownz.4	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	idomnnzpownz.5	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
Assertion	idomnnzpownz	$$⊢\phi \to N\underset{\dot{}}{\times }A\ne 0_R$$

Proof

Step	Hyp	Ref	Expression
1		idomnnzpownz.1	$$⊢\phi \to R\in \mathrm{IDomn}$$
2		idomnnzpownz.2	$$⊢\phi \to A\in {\mathrm{Base}}_R$$
3		idomnnzpownz.3	$$⊢\phi \to A\ne 0_R$$
4		idomnnzpownz.4	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		idomnnzpownz.5	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
6	4	ancli	$$⊢\phi \to \left(\phi \wedge N\in {\mathbb{N}}_0\right)$$
7		oveq1	$$⊢x=0\to x\underset{\dot{}}{\times }A=0\underset{\dot{}}{\times }A$$
8	7	neeq1d	$$⊢x=0\to \left(x\underset{\dot{}}{\times }A\ne 0_R\leftrightarrow 0\underset{\dot{}}{\times }A\ne 0_R\right)$$
9		oveq1	$$⊢x=y\to x\underset{\dot{}}{\times }A=y\underset{\dot{}}{\times }A$$
10	9	neeq1d	$$⊢x=y\to \left(x\underset{\dot{}}{\times }A\ne 0_R\leftrightarrow y\underset{\dot{}}{\times }A\ne 0_R\right)$$
11		oveq1	$$⊢x=y+1\to x\underset{\dot{}}{\times }A=\left(y+1\right)\underset{\dot{}}{\times }A$$
12	11	neeq1d	$$⊢x=y+1\to \left(x\underset{\dot{}}{\times }A\ne 0_R\leftrightarrow \left(y+1\right)\underset{\dot{}}{\times }A\ne 0_R\right)$$
13		oveq1	$$⊢x=N\to x\underset{\dot{}}{\times }A=N\underset{\dot{}}{\times }A$$
14	13	neeq1d	$$⊢x=N\to \left(x\underset{\dot{}}{\times }A\ne 0_R\leftrightarrow N\underset{\dot{}}{\times }A\ne 0_R\right)$$
15		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
16		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
17	15 16	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
18	2 17	eleqtrdi	$$⊢\phi \to A\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
19		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_R}={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
20		eqid	$$⊢0_{{\mathrm{mulGrp}}_R}=0_{{\mathrm{mulGrp}}_R}$$
21	19 20 5	mulg0	$$⊢A\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}\to 0\underset{\dot{}}{\times }A=0_{{\mathrm{mulGrp}}_R}$$
22	18 21	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }A=0_{{\mathrm{mulGrp}}_R}$$
23		eqid	$$⊢1_R=1_R$$
24	15 23	ringidval	$$⊢1_R=0_{{\mathrm{mulGrp}}_R}$$
25	22 24	eqtr4di	$$⊢\phi \to 0\underset{\dot{}}{\times }A=1_R$$
26		isidom	$$⊢R\in \mathrm{IDomn}\leftrightarrow \left(R\in \mathrm{CRing}\wedge R\in \mathrm{Domn}\right)$$
27	26	simprbi	$$⊢R\in \mathrm{IDomn}\to R\in \mathrm{Domn}$$
28		domnnzr	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{NzRing}$$
29		eqid	$$⊢0_R=0_R$$
30	23 29	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne 0_R$$
31	1 27 28 30	4syl	$$⊢\phi \to 1_R\ne 0_R$$
32	25 31	eqnetrd	$$⊢\phi \to 0\underset{\dot{}}{\times }A\ne 0_R$$
33	1	idomringd	$$⊢\phi \to R\in \mathrm{Ring}$$
34	15	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
35	33 34	syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
36	35	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
37	36	adantr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
38		simplr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to y\in {\mathbb{N}}_0$$
39	18	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to A\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
40		eqid	$$⊢{+}_{{\mathrm{mulGrp}}_R}={+}_{{\mathrm{mulGrp}}_R}$$
41	19 5 40	mulgnn0p1	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge A\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}\right)\to \left(y+1\right)\underset{\dot{}}{\times }A=\left(y\underset{\dot{}}{\times }A\right){+}_{{\mathrm{mulGrp}}_R}A$$
42	37 38 39 41	syl3anc	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to \left(y+1\right)\underset{\dot{}}{\times }A=\left(y\underset{\dot{}}{\times }A\right){+}_{{\mathrm{mulGrp}}_R}A$$
43		eqid	$$⊢{\cdot }_R={\cdot }_R$$
44	15 43	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
45	44	a1i	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to {\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
46	45	eqcomd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to {+}_{{\mathrm{mulGrp}}_R}={\cdot }_R$$
47	46	oveqd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to \left(y\underset{\dot{}}{\times }A\right){+}_{{\mathrm{mulGrp}}_R}A=\left(y\underset{\dot{}}{\times }A\right){\cdot }_{R}A$$
48	1 27	syl	$$⊢\phi \to R\in \mathrm{Domn}$$
49	48	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to R\in \mathrm{Domn}$$
50	49	adantr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to R\in \mathrm{Domn}$$
51	19 5	mulgnn0cl	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge A\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}\right)\to y\underset{\dot{}}{\times }A\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
52	37 38 39 51	syl3anc	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to y\underset{\dot{}}{\times }A\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
53	17	eqcomi	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_R}={\mathrm{Base}}_R$$
54	53	a1i	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}={\mathrm{Base}}_R$$
55	52 54	eleqtrd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to y\underset{\dot{}}{\times }A\in {\mathrm{Base}}_R$$
56		simpr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to y\underset{\dot{}}{\times }A\ne 0_R$$
57	55 56	jca	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to \left(y\underset{\dot{}}{\times }A\in {\mathrm{Base}}_R\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)$$
58	2 3	jca	$$⊢\phi \to \left(A\in {\mathrm{Base}}_R\wedge A\ne 0_R\right)$$
59	58	adantr	$$⊢\left(\phi \wedge y\in {\mathbb{N}}_0\right)\to \left(A\in {\mathrm{Base}}_R\wedge A\ne 0_R\right)$$
60	59	adantr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to \left(A\in {\mathrm{Base}}_R\wedge A\ne 0_R\right)$$
61	16 43 29	domnmuln0	$$⊢\left(R\in \mathrm{Domn}\wedge \left(y\underset{\dot{}}{\times }A\in {\mathrm{Base}}_R\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\wedge \left(A\in {\mathrm{Base}}_R\wedge A\ne 0_R\right)\right)\to \left(y\underset{\dot{}}{\times }A\right){\cdot }_{R}A\ne 0_R$$
62	50 57 60 61	syl3anc	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to \left(y\underset{\dot{}}{\times }A\right){\cdot }_{R}A\ne 0_R$$
63	47 62	eqnetrd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to \left(y\underset{\dot{}}{\times }A\right){+}_{{\mathrm{mulGrp}}_R}A\ne 0_R$$
64	42 63	eqnetrd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge y\underset{\dot{}}{\times }A\ne 0_R\right)\to \left(y+1\right)\underset{\dot{}}{\times }A\ne 0_R$$
65	8 10 12 14 32 64	nn0indd	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\right)\to N\underset{\dot{}}{\times }A\ne 0_R$$
66	6 65	syl	$$⊢\phi \to N\underset{\dot{}}{\times }A\ne 0_R$$