Theorem ringexp0nn

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

	Ref	Expression
Hypotheses	ringexp0nn.1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ringexp0nn.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	ringexp0nn.3	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
Assertion	ringexp0nn	⊢ ( 𝜑 → ( 𝑁 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ringexp0nn.1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
2		ringexp0nn.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		ringexp0nn.3	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
4	2	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ 𝑁 ∈ ℕ ) )
5		oveq1	⊢ ( 𝑥 = 1 → ( 𝑥 ↑ ( 0g ‘ 𝑅 ) ) = ( 1 ↑ ( 0g ‘ 𝑅 ) ) )
6	5	eqeq1d	⊢ ( 𝑥 = 1 → ( ( 𝑥 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ↔ ( 1 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
7		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ ( 0g ‘ 𝑅 ) ) = ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) )
8	7	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
9		oveq1	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ↑ ( 0g ‘ 𝑅 ) ) = ( ( 𝑦 + 1 ) ↑ ( 0g ‘ 𝑅 ) ) )
10	9	eqeq1d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ↔ ( ( 𝑦 + 1 ) ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
11		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 ↑ ( 0g ‘ 𝑅 ) ) = ( 𝑁 ↑ ( 0g ‘ 𝑅 ) ) )
12	11	eqeq1d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑁 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
13		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
14	1 13	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
15		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17	15 16	mndidcl	⊢ ( 𝑅 ∈ Mnd → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
18	14 17	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
19		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
20	19 15	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
21	20	a1i	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
22	18 21	eleqtrd	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
23		eqid	⊢ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
24	23 3	mulg1	⊢ ( ( 0g ‘ 𝑅 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) → ( 1 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
25	22 24	syl	⊢ ( 𝜑 → ( 1 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
26		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) → 𝑦 ∈ ℕ )
27	22	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
28		eqid	⊢ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
29	23 3 28	mulgnnp1	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 0g ‘ 𝑅 ) ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) → ( ( 𝑦 + 1 ) ↑ ( 0g ‘ 𝑅 ) ) = ( ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) ( 0g ‘ 𝑅 ) ) )
30	26 27 29	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑦 + 1 ) ↑ ( 0g ‘ 𝑅 ) ) = ( ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) ( 0g ‘ 𝑅 ) ) )
31		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
32	31	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) ( 0g ‘ 𝑅 ) ) = ( ( 0g ‘ 𝑅 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) ( 0g ‘ 𝑅 ) ) )
33		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
34	19 33	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
35	34	eqcomi	⊢ ( +g ‘ ( mulGrp ‘ 𝑅 ) ) = ( .r ‘ 𝑅 )
36	15 35 16	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
37	1 18 36	syl2anc	⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
39	38	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 0g ‘ 𝑅 ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
40	32 39	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) ( +g ‘ ( mulGrp ‘ 𝑅 ) ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
41	30 40	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑦 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑦 + 1 ) ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
42	6 8 10 12 25 41	nnindd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
43	4 42	syl	⊢ ( 𝜑 → ( 𝑁 ↑ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )