Metamath Proof Explorer

Theorem idomnnzpownz

Description: A non-zero power in an integral domain is non-zero. (Contributed by metakunt, 5-May-2025)

Ref Expression
Hypotheses idomnnzpownz.1 
|- ( ph -> R e. IDomn )
idomnnzpownz.2 
|- ( ph -> A e. ( Base ` R ) )
idomnnzpownz.3 
|- ( ph -> A =/= ( 0g ` R ) )
idomnnzpownz.4 
|- ( ph -> N e. NN0 )
idomnnzpownz.5 
|- .^ = ( .g ` ( mulGrp ` R ) )
Assertion idomnnzpownz 
|- ( ph -> ( N .^ A ) =/= ( 0g ` R ) )

Proof

Step Hyp Ref Expression
1 idomnnzpownz.1 
 |-  ( ph -> R e. IDomn )
2 idomnnzpownz.2 
 |-  ( ph -> A e. ( Base ` R ) )
3 idomnnzpownz.3 
 |-  ( ph -> A =/= ( 0g ` R ) )
4 idomnnzpownz.4 
 |-  ( ph -> N e. NN0 )
5 idomnnzpownz.5 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
6 4 ancli 
 |-  ( ph -> ( ph /\ N e. NN0 ) )
7 oveq1 
 |-  ( x = 0 -> ( x .^ A ) = ( 0 .^ A ) )
8 7 neeq1d 
 |-  ( x = 0 -> ( ( x .^ A ) =/= ( 0g ` R ) <-> ( 0 .^ A ) =/= ( 0g ` R ) ) )
9 oveq1 
 |-  ( x = y -> ( x .^ A ) = ( y .^ A ) )
10 9 neeq1d 
 |-  ( x = y -> ( ( x .^ A ) =/= ( 0g ` R ) <-> ( y .^ A ) =/= ( 0g ` R ) ) )
11 oveq1 
 |-  ( x = ( y + 1 ) -> ( x .^ A ) = ( ( y + 1 ) .^ A ) )
12 11 neeq1d 
 |-  ( x = ( y + 1 ) -> ( ( x .^ A ) =/= ( 0g ` R ) <-> ( ( y + 1 ) .^ A ) =/= ( 0g ` R ) ) )
13 oveq1 
 |-  ( x = N -> ( x .^ A ) = ( N .^ A ) )
14 13 neeq1d 
 |-  ( x = N -> ( ( x .^ A ) =/= ( 0g ` R ) <-> ( N .^ A ) =/= ( 0g ` R ) ) )
15 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
16 eqid 
 |-  ( Base ` R ) = ( Base ` R )
17 15 16 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
18 2 17 eleqtrdi 
 |-  ( ph -> A e. ( Base ` ( mulGrp ` R ) ) )
19 eqid 
 |-  ( Base ` ( mulGrp ` R ) ) = ( Base ` ( mulGrp ` R ) )
20 eqid 
 |-  ( 0g ` ( mulGrp ` R ) ) = ( 0g ` ( mulGrp ` R ) )
21 19 20 5 mulg0 
 |-  ( A e. ( Base ` ( mulGrp ` R ) ) -> ( 0 .^ A ) = ( 0g ` ( mulGrp ` R ) ) )
22 18 21 syl 
 |-  ( ph -> ( 0 .^ A ) = ( 0g ` ( mulGrp ` R ) ) )
23 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
24 15 23 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
25 22 24 eqtr4di 
 |-  ( ph -> ( 0 .^ A ) = ( 1r ` R ) )
26 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
27 26 simprbi 
 |-  ( R e. IDomn -> R e. Domn )
28 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
29 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
30 23 29 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
31 1 27 28 30 4syl 
 |-  ( ph -> ( 1r ` R ) =/= ( 0g ` R ) )
32 25 31 eqnetrd 
 |-  ( ph -> ( 0 .^ A ) =/= ( 0g ` R ) )
33 1 idomringd 
 |-  ( ph -> R e. Ring )
34 15 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
35 33 34 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
36 35 adantr 
 |-  ( ( ph /\ y e. NN0 ) -> ( mulGrp ` R ) e. Mnd )
37 36 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( mulGrp ` R ) e. Mnd )
38 simplr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> y e. NN0 )
39 18 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> A e. ( Base ` ( mulGrp ` R ) ) )
40 eqid 
 |-  ( +g ` ( mulGrp ` R ) ) = ( +g ` ( mulGrp ` R ) )
41 19 5 40 mulgnn0p1 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ y e. NN0 /\ A e. ( Base ` ( mulGrp ` R ) ) ) -> ( ( y + 1 ) .^ A ) = ( ( y .^ A ) ( +g ` ( mulGrp ` R ) ) A ) )
42 37 38 39 41 syl3anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( ( y + 1 ) .^ A ) = ( ( y .^ A ) ( +g ` ( mulGrp ` R ) ) A ) )
43 eqid 
 |-  ( .r ` R ) = ( .r ` R )
44 15 43 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
45 44 a1i 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( .r ` R ) = ( +g ` ( mulGrp ` R ) ) )
46 45 eqcomd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( +g ` ( mulGrp ` R ) ) = ( .r ` R ) )
47 46 oveqd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( ( y .^ A ) ( +g ` ( mulGrp ` R ) ) A ) = ( ( y .^ A ) ( .r ` R ) A ) )
48 1 27 syl 
 |-  ( ph -> R e. Domn )
49 48 adantr 
 |-  ( ( ph /\ y e. NN0 ) -> R e. Domn )
50 49 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> R e. Domn )
51 19 5 mulgnn0cl 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ y e. NN0 /\ A e. ( Base ` ( mulGrp ` R ) ) ) -> ( y .^ A ) e. ( Base ` ( mulGrp ` R ) ) )
52 37 38 39 51 syl3anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( y .^ A ) e. ( Base ` ( mulGrp ` R ) ) )
53 17 eqcomi 
 |-  ( Base ` ( mulGrp ` R ) ) = ( Base ` R )
54 53 a1i 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( Base ` ( mulGrp ` R ) ) = ( Base ` R ) )
55 52 54 eleqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( y .^ A ) e. ( Base ` R ) )
56 simpr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( y .^ A ) =/= ( 0g ` R ) )
57 55 56 jca 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( ( y .^ A ) e. ( Base ` R ) /\ ( y .^ A ) =/= ( 0g ` R ) ) )
58 2 3 jca 
 |-  ( ph -> ( A e. ( Base ` R ) /\ A =/= ( 0g ` R ) ) )
59 58 adantr 
 |-  ( ( ph /\ y e. NN0 ) -> ( A e. ( Base ` R ) /\ A =/= ( 0g ` R ) ) )
60 59 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( A e. ( Base ` R ) /\ A =/= ( 0g ` R ) ) )
61 16 43 29 domnmuln0 
 |-  ( ( R e. Domn /\ ( ( y .^ A ) e. ( Base ` R ) /\ ( y .^ A ) =/= ( 0g ` R ) ) /\ ( A e. ( Base ` R ) /\ A =/= ( 0g ` R ) ) ) -> ( ( y .^ A ) ( .r ` R ) A ) =/= ( 0g ` R ) )
62 50 57 60 61 syl3anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( ( y .^ A ) ( .r ` R ) A ) =/= ( 0g ` R ) )
63 47 62 eqnetrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( ( y .^ A ) ( +g ` ( mulGrp ` R ) ) A ) =/= ( 0g ` R ) )
64 42 63 eqnetrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( y .^ A ) =/= ( 0g ` R ) ) -> ( ( y + 1 ) .^ A ) =/= ( 0g ` R ) )
65 8 10 12 14 32 64 nn0indd 
 |-  ( ( ph /\ N e. NN0 ) -> ( N .^ A ) =/= ( 0g ` R ) )
66 6 65 syl 
 |-  ( ph -> ( N .^ A ) =/= ( 0g ` R ) )