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 
|- B = ( Base ` R )
domnexpgn0cl.0 
|- .0. = ( 0g ` R )
domnexpgn0cl.e 
|- .^ = ( .g ` ( mulGrp ` R ) )
domnexpgn0cl.r 
|- ( ph -> R e. Domn )
domnexpgn0cl.n 
|- ( ph -> N e. NN0 )
domnexpgn0cl.x 
|- ( ph -> X e. ( B \ { .0. } ) )
Assertion domnexpgn0cl 
|- ( ph -> ( N .^ X ) e. ( B \ { .0. } ) )

Proof

Step Hyp Ref Expression
1 domnexpgn0cl.b 
 |-  B = ( Base ` R )
2 domnexpgn0cl.0 
 |-  .0. = ( 0g ` R )
3 domnexpgn0cl.e 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
4 domnexpgn0cl.r 
 |-  ( ph -> R e. Domn )
5 domnexpgn0cl.n 
 |-  ( ph -> N e. NN0 )
6 domnexpgn0cl.x 
 |-  ( ph -> X e. ( B \ { .0. } ) )
7 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
8 7 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
9 domnring 
 |-  ( R e. Domn -> R e. Ring )
10 7 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
11 4 9 10 3syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
12 6 eldifad 
 |-  ( ph -> X e. B )
13 8 3 11 5 12 mulgnn0cld 
 |-  ( ph -> ( N .^ X ) e. B )
14 oveq1 
 |-  ( x = 0 -> ( x .^ X ) = ( 0 .^ X ) )
15 14 neeq1d 
 |-  ( x = 0 -> ( ( x .^ X ) =/= .0. <-> ( 0 .^ X ) =/= .0. ) )
16 oveq1 
 |-  ( x = y -> ( x .^ X ) = ( y .^ X ) )
17 16 neeq1d 
 |-  ( x = y -> ( ( x .^ X ) =/= .0. <-> ( y .^ X ) =/= .0. ) )
18 oveq1 
 |-  ( x = ( y + 1 ) -> ( x .^ X ) = ( ( y + 1 ) .^ X ) )
19 18 neeq1d 
 |-  ( x = ( y + 1 ) -> ( ( x .^ X ) =/= .0. <-> ( ( y + 1 ) .^ X ) =/= .0. ) )
20 oveq1 
 |-  ( x = N -> ( x .^ X ) = ( N .^ X ) )
21 20 neeq1d 
 |-  ( x = N -> ( ( x .^ X ) =/= .0. <-> ( N .^ X ) =/= .0. ) )
22 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
23 7 22 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
24 8 23 3 mulg0 
 |-  ( X e. B -> ( 0 .^ X ) = ( 1r ` R ) )
25 12 24 syl 
 |-  ( ph -> ( 0 .^ X ) = ( 1r ` R ) )
26 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
27 22 2 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= .0. )
28 4 26 27 3syl 
 |-  ( ph -> ( 1r ` R ) =/= .0. )
29 25 28 eqnetrd 
 |-  ( ph -> ( 0 .^ X ) =/= .0. )
30 11 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) =/= .0. ) -> ( mulGrp ` R ) e. Mnd )
31 simplr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) =/= .0. ) -> y e. NN0 )
32 12 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) =/= .0. ) -> X e. B )
33 eqid 
 |-  ( .r ` R ) = ( .r ` R )
34 7 33 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
35 8 3 34 mulgnn0p1 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ y e. NN0 /\ X e. B ) -> ( ( y + 1 ) .^ X ) = ( ( y .^ X ) ( .r ` R ) X ) )
36 30 31 32 35 syl3anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) =/= .0. ) -> ( ( y + 1 ) .^ X ) = ( ( y .^ X ) ( .r ` R ) X ) )
37 4 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) =/= .0. ) -> R e. Domn )
38 8 3 30 31 32 mulgnn0cld 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) =/= .0. ) -> ( y .^ X ) e. B )
39 simpr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) =/= .0. ) -> ( y .^ X ) =/= .0. )
40 eldifsni 
 |-  ( X e. ( B \ { .0. } ) -> X =/= .0. )
41 6 40 syl 
 |-  ( ph -> X =/= .0. )
42 41 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) =/= .0. ) -> X =/= .0. )
43 1 33 2 domnmuln0 
 |-  ( ( R e. Domn /\ ( ( y .^ X ) e. B /\ ( y .^ X ) =/= .0. ) /\ ( X e. B /\ X =/= .0. ) ) -> ( ( y .^ X ) ( .r ` R ) X ) =/= .0. )
44 37 38 39 32 42 43 syl122anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) =/= .0. ) -> ( ( y .^ X ) ( .r ` R ) X ) =/= .0. )
45 36 44 eqnetrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ X ) =/= .0. ) -> ( ( y + 1 ) .^ X ) =/= .0. )
46 15 17 19 21 29 45 nn0indd 
 |-  ( ( ph /\ N e. NN0 ) -> ( N .^ X ) =/= .0. )
47 5 46 mpdan 
 |-  ( ph -> ( N .^ X ) =/= .0. )
48 13 47 eldifsnd 
 |-  ( ph -> ( N .^ X ) e. ( B \ { .0. } ) )