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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	domnexpgn0cl.0	⊢ 0 = ( 0g ‘ 𝑅 )
	domnexpgn0cl.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
	domnexpgn0cl.r	⊢ ( 𝜑 → 𝑅 ∈ Domn )
	domnexpgn0cl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	domnexpgn0cl.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ { 0 } ) )
Assertion	domnexpgn0cl	⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ∈ ( 𝐵 ∖ { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		domnexpgn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		domnexpgn0cl.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		domnexpgn0cl.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
4		domnexpgn0cl.r	⊢ ( 𝜑 → 𝑅 ∈ Domn )
5		domnexpgn0cl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		domnexpgn0cl.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ { 0 } ) )
7		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
8	7 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
9		domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
10	7	ringmgp	⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
11	4 9 10	3syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
12	6	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
13	8 3 11 5 12	mulgnn0cld	⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ∈ 𝐵 )
14		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 ↑ 𝑋 ) = ( 0 ↑ 𝑋 ) )
15	14	neeq1d	⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ 𝑋 ) ≠ 0 ↔ ( 0 ↑ 𝑋 ) ≠ 0 ) )
16		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 𝑋 ) = ( 𝑦 ↑ 𝑋 ) )
17	16	neeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 𝑋 ) ≠ 0 ↔ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) )
18		oveq1	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ↑ 𝑋 ) = ( ( 𝑦 + 1 ) ↑ 𝑋 ) )
19	18	neeq1d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 ↑ 𝑋 ) ≠ 0 ↔ ( ( 𝑦 + 1 ) ↑ 𝑋 ) ≠ 0 ) )
20		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 ↑ 𝑋 ) = ( 𝑁 ↑ 𝑋 ) )
21	20	neeq1d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ↑ 𝑋 ) ≠ 0 ↔ ( 𝑁 ↑ 𝑋 ) ≠ 0 ) )
22		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
23	7 22	ringidval	⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ ( mulGrp ‘ 𝑅 ) )
24	8 23 3	mulg0	⊢ ( 𝑋 ∈ 𝐵 → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑅 ) )
25	12 24	syl	⊢ ( 𝜑 → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑅 ) )
26		domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
27	22 2	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
28	4 26 27	3syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ 0 )
29	25 28	eqnetrd	⊢ ( 𝜑 → ( 0 ↑ 𝑋 ) ≠ 0 )
30	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
31		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) → 𝑦 ∈ ℕ0 )
32	12	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) → 𝑋 ∈ 𝐵 )
33		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
34	7 33	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
35	8 3 34	mulgnn0p1	⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑦 + 1 ) ↑ 𝑋 ) = ( ( 𝑦 ↑ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) )
36	30 31 32 35	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) → ( ( 𝑦 + 1 ) ↑ 𝑋 ) = ( ( 𝑦 ↑ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) )
37	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) → 𝑅 ∈ Domn )
38	8 3 30 31 32	mulgnn0cld	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) → ( 𝑦 ↑ 𝑋 ) ∈ 𝐵 )
39		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) → ( 𝑦 ↑ 𝑋 ) ≠ 0 )
40		eldifsni	⊢ ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) → 𝑋 ≠ 0 )
41	6 40	syl	⊢ ( 𝜑 → 𝑋 ≠ 0 )
42	41	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) → 𝑋 ≠ 0 )
43	1 33 2	domnmuln0	⊢ ( ( 𝑅 ∈ Domn ∧ ( ( 𝑦 ↑ 𝑋 ) ∈ 𝐵 ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝑦 ↑ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) ≠ 0 )
44	37 38 39 32 42 43	syl122anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) → ( ( 𝑦 ↑ 𝑋 ) ( .r ‘ 𝑅 ) 𝑋 ) ≠ 0 )
45	36 44	eqnetrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℕ0 ) ∧ ( 𝑦 ↑ 𝑋 ) ≠ 0 ) → ( ( 𝑦 + 1 ) ↑ 𝑋 ) ≠ 0 )
46	15 17 19 21 29 45	nn0indd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑋 ) ≠ 0 )
47	5 46	mpdan	⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ≠ 0 )
48	13 47	eldifsnd	⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ∈ ( 𝐵 ∖ { 0 } ) )