This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) )