Theorem ringexp0nn

Description: Zero to the power of a positive integer is zero. (Contributed by metakunt, 5-May-2025)

	Ref	Expression
Hypotheses	ringexp0nn.1	$$⊢\phi \to R\in \mathrm{Ring}$$
	ringexp0nn.2	$$⊢\phi \to N\in \mathbb{N}$$
	ringexp0nn.3	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
Assertion	ringexp0nn	$$⊢\phi \to N\underset{\dot{}}{\times }{0}_R=0_R$$

Proof

Step	Hyp	Ref	Expression
1		ringexp0nn.1	$$⊢\phi \to R\in \mathrm{Ring}$$
2		ringexp0nn.2	$$⊢\phi \to N\in \mathbb{N}$$
3		ringexp0nn.3	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
4	2	ancli	$$⊢\phi \to \left(\phi \wedge N\in \mathbb{N}\right)$$
5		oveq1	$$⊢x=1\to x\underset{\dot{}}{\times }{0}_R=1\underset{\dot{}}{\times }{0}_R$$
6	5	eqeq1d	$$⊢x=1\to \left(x\underset{\dot{}}{\times }{0}_R=0_R\leftrightarrow 1\underset{\dot{}}{\times }{0}_R=0_R\right)$$
7		oveq1	$$⊢x=y\to x\underset{\dot{}}{\times }{0}_R=y\underset{\dot{}}{\times }{0}_R$$
8	7	eqeq1d	$$⊢x=y\to \left(x\underset{\dot{}}{\times }{0}_R=0_R\leftrightarrow y\underset{\dot{}}{\times }{0}_R=0_R\right)$$
9		oveq1	$$⊢x=y+1\to x\underset{\dot{}}{\times }{0}_R=\left(y+1\right)\underset{\dot{}}{\times }{0}_R$$
10	9	eqeq1d	$$⊢x=y+1\to \left(x\underset{\dot{}}{\times }{0}_R=0_R\leftrightarrow \left(y+1\right)\underset{\dot{}}{\times }{0}_R=0_R\right)$$
11		oveq1	$$⊢x=N\to x\underset{\dot{}}{\times }{0}_R=N\underset{\dot{}}{\times }{0}_R$$
12	11	eqeq1d	$$⊢x=N\to \left(x\underset{\dot{}}{\times }{0}_R=0_R\leftrightarrow N\underset{\dot{}}{\times }{0}_R=0_R\right)$$
13		ringmnd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$
14	1 13	syl	$$⊢\phi \to R\in \mathrm{Mnd}$$
15		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
16		eqid	$$⊢0_R=0_R$$
17	15 16	mndidcl	$$⊢R\in \mathrm{Mnd}\to 0_R\in {\mathrm{Base}}_R$$
18	14 17	syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
19		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
20	19 15	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
21	20	a1i	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
22	18 21	eleqtrd	$$⊢\phi \to 0_R\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
23		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_R}={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
24	23 3	mulg1	$$⊢0_R\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}\to 1\underset{\dot{}}{\times }{0}_R=0_R$$
25	22 24	syl	$$⊢\phi \to 1\underset{\dot{}}{\times }{0}_R=0_R$$
26		simplr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge y\underset{\dot{}}{\times }{0}_R=0_R\right)\to y\in \mathbb{N}$$
27	22	ad2antrr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge y\underset{\dot{}}{\times }{0}_R=0_R\right)\to 0_R\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
28		eqid	$$⊢{+}_{{\mathrm{mulGrp}}_R}={+}_{{\mathrm{mulGrp}}_R}$$
29	23 3 28	mulgnnp1	$$⊢\left(y\in \mathbb{N}\wedge 0_R\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_R}\right)\to \left(y+1\right)\underset{\dot{}}{\times }{0}_R=\left(y\underset{\dot{}}{\times }{0}_R\right){+}_{{\mathrm{mulGrp}}_R}{0}_R$$
30	26 27 29	syl2anc	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge y\underset{\dot{}}{\times }{0}_R=0_R\right)\to \left(y+1\right)\underset{\dot{}}{\times }{0}_R=\left(y\underset{\dot{}}{\times }{0}_R\right){+}_{{\mathrm{mulGrp}}_R}{0}_R$$
31		simpr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge y\underset{\dot{}}{\times }{0}_R=0_R\right)\to y\underset{\dot{}}{\times }{0}_R=0_R$$
32	31	oveq1d	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge y\underset{\dot{}}{\times }{0}_R=0_R\right)\to \left(y\underset{\dot{}}{\times }{0}_R\right){+}_{{\mathrm{mulGrp}}_R}{0}_R=0_R{+}_{{\mathrm{mulGrp}}_R}{0}_R$$
33		eqid	$$⊢{\cdot }_R={\cdot }_R$$
34	19 33	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
35	34	eqcomi	$$⊢{+}_{{\mathrm{mulGrp}}_R}={\cdot }_R$$
36	15 35 16	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge 0_R\in {\mathrm{Base}}_R\right)\to 0_R{+}_{{\mathrm{mulGrp}}_R}{0}_R=0_R$$
37	1 18 36	syl2anc	$$⊢\phi \to 0_R{+}_{{\mathrm{mulGrp}}_R}{0}_R=0_R$$
38	37	adantr	$$⊢\left(\phi \wedge y\in \mathbb{N}\right)\to 0_R{+}_{{\mathrm{mulGrp}}_R}{0}_R=0_R$$
39	38	adantr	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge y\underset{\dot{}}{\times }{0}_R=0_R\right)\to 0_R{+}_{{\mathrm{mulGrp}}_R}{0}_R=0_R$$
40	32 39	eqtrd	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge y\underset{\dot{}}{\times }{0}_R=0_R\right)\to \left(y\underset{\dot{}}{\times }{0}_R\right){+}_{{\mathrm{mulGrp}}_R}{0}_R=0_R$$
41	30 40	eqtrd	$$⊢\left(\left(\phi \wedge y\in \mathbb{N}\right)\wedge y\underset{\dot{}}{\times }{0}_R=0_R\right)\to \left(y+1\right)\underset{\dot{}}{\times }{0}_R=0_R$$
42	6 8 10 12 25 41	nnindd	$$⊢\left(\phi \wedge N\in \mathbb{N}\right)\to N\underset{\dot{}}{\times }{0}_R=0_R$$
43	4 42	syl	$$⊢\phi \to N\underset{\dot{}}{\times }{0}_R=0_R$$