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

Metamath Proof Explorer

Theorem abvexp

Description: Move exponentiation in and out of absolute value. (Contributed by SN, 3-Jul-2025)

Ref Expression
Hypotheses abvexp.a 
|- A = ( AbsVal ` R )
abvexp.e 
|- .^ = ( .g ` ( mulGrp ` R ) )
abvexp.b 
|- B = ( Base ` R )
abvexp.r 
|- ( ph -> R e. NzRing )
abvexp.f 
|- ( ph -> F e. A )
abvexp.x 
|- ( ph -> X e. B )
abvexp.n 
|- ( ph -> N e. NN0 )
Assertion abvexp 
|- ( ph -> ( F ` ( N .^ X ) ) = ( ( F ` X ) ^ N ) )

Proof

Step Hyp Ref Expression
1 abvexp.a 
 |-  A = ( AbsVal ` R )
2 abvexp.e 
 |-  .^ = ( .g ` ( mulGrp ` R ) )
3 abvexp.b 
 |-  B = ( Base ` R )
4 abvexp.r 
 |-  ( ph -> R e. NzRing )
5 abvexp.f 
 |-  ( ph -> F e. A )
6 abvexp.x 
 |-  ( ph -> X e. B )
7 abvexp.n 
 |-  ( ph -> N e. NN0 )
8 fvoveq1 
 |-  ( x = 0 -> ( F ` ( x .^ X ) ) = ( F ` ( 0 .^ X ) ) )
9 oveq2 
 |-  ( x = 0 -> ( ( F ` X ) ^ x ) = ( ( F ` X ) ^ 0 ) )
10 8 9 eqeq12d 
 |-  ( x = 0 -> ( ( F ` ( x .^ X ) ) = ( ( F ` X ) ^ x ) <-> ( F ` ( 0 .^ X ) ) = ( ( F ` X ) ^ 0 ) ) )
11 fvoveq1 
 |-  ( x = y -> ( F ` ( x .^ X ) ) = ( F ` ( y .^ X ) ) )
12 oveq2 
 |-  ( x = y -> ( ( F ` X ) ^ x ) = ( ( F ` X ) ^ y ) )
13 11 12 eqeq12d 
 |-  ( x = y -> ( ( F ` ( x .^ X ) ) = ( ( F ` X ) ^ x ) <-> ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) )
14 fvoveq1 
 |-  ( x = ( y + 1 ) -> ( F ` ( x .^ X ) ) = ( F ` ( ( y + 1 ) .^ X ) ) )
15 oveq2 
 |-  ( x = ( y + 1 ) -> ( ( F ` X ) ^ x ) = ( ( F ` X ) ^ ( y + 1 ) ) )
16 14 15 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( F ` ( x .^ X ) ) = ( ( F ` X ) ^ x ) <-> ( F ` ( ( y + 1 ) .^ X ) ) = ( ( F ` X ) ^ ( y + 1 ) ) ) )
17 fvoveq1 
 |-  ( x = N -> ( F ` ( x .^ X ) ) = ( F ` ( N .^ X ) ) )
18 oveq2 
 |-  ( x = N -> ( ( F ` X ) ^ x ) = ( ( F ` X ) ^ N ) )
19 17 18 eqeq12d 
 |-  ( x = N -> ( ( F ` ( x .^ X ) ) = ( ( F ` X ) ^ x ) <-> ( F ` ( N .^ X ) ) = ( ( F ` X ) ^ N ) ) )
20 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
21 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
22 20 21 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
23 4 22 syl 
 |-  ( ph -> ( 1r ` R ) =/= ( 0g ` R ) )
24 1 20 21 abv1z 
 |-  ( ( F e. A /\ ( 1r ` R ) =/= ( 0g ` R ) ) -> ( F ` ( 1r ` R ) ) = 1 )
25 5 23 24 syl2anc 
 |-  ( ph -> ( F ` ( 1r ` R ) ) = 1 )
26 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
27 26 3 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
28 26 20 ringidval 
 |-  ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
29 27 28 2 mulg0 
 |-  ( X e. B -> ( 0 .^ X ) = ( 1r ` R ) )
30 6 29 syl 
 |-  ( ph -> ( 0 .^ X ) = ( 1r ` R ) )
31 30 fveq2d 
 |-  ( ph -> ( F ` ( 0 .^ X ) ) = ( F ` ( 1r ` R ) ) )
32 1 3 abvcl 
 |-  ( ( F e. A /\ X e. B ) -> ( F ` X ) e. RR )
33 5 6 32 syl2anc 
 |-  ( ph -> ( F ` X ) e. RR )
34 33 recnd 
 |-  ( ph -> ( F ` X ) e. CC )
35 34 exp0d 
 |-  ( ph -> ( ( F ` X ) ^ 0 ) = 1 )
36 25 31 35 3eqtr4d 
 |-  ( ph -> ( F ` ( 0 .^ X ) ) = ( ( F ` X ) ^ 0 ) )
37 5 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> F e. A )
38 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
39 26 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
40 4 38 39 3syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
41 40 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( mulGrp ` R ) e. Mnd )
42 simplr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> y e. NN0 )
43 6 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> X e. B )
44 27 2 41 42 43 mulgnn0cld 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( y .^ X ) e. B )
45 eqid 
 |-  ( .r ` R ) = ( .r ` R )
46 1 3 45 abvmul 
 |-  ( ( F e. A /\ ( y .^ X ) e. B /\ X e. B ) -> ( F ` ( ( y .^ X ) ( .r ` R ) X ) ) = ( ( F ` ( y .^ X ) ) x. ( F ` X ) ) )
47 37 44 43 46 syl3anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( F ` ( ( y .^ X ) ( .r ` R ) X ) ) = ( ( F ` ( y .^ X ) ) x. ( F ` X ) ) )
48 simpr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) )
49 48 oveq1d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( ( F ` ( y .^ X ) ) x. ( F ` X ) ) = ( ( ( F ` X ) ^ y ) x. ( F ` X ) ) )
50 47 49 eqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( F ` ( ( y .^ X ) ( .r ` R ) X ) ) = ( ( ( F ` X ) ^ y ) x. ( F ` X ) ) )
51 26 45 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
52 27 2 51 mulgnn0p1 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ y e. NN0 /\ X e. B ) -> ( ( y + 1 ) .^ X ) = ( ( y .^ X ) ( .r ` R ) X ) )
53 41 42 43 52 syl3anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( ( y + 1 ) .^ X ) = ( ( y .^ X ) ( .r ` R ) X ) )
54 53 fveq2d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( F ` ( ( y + 1 ) .^ X ) ) = ( F ` ( ( y .^ X ) ( .r ` R ) X ) ) )
55 34 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( F ` X ) e. CC )
56 55 42 expp1d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( ( F ` X ) ^ ( y + 1 ) ) = ( ( ( F ` X ) ^ y ) x. ( F ` X ) ) )
57 50 54 56 3eqtr4d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( F ` ( y .^ X ) ) = ( ( F ` X ) ^ y ) ) -> ( F ` ( ( y + 1 ) .^ X ) ) = ( ( F ` X ) ^ ( y + 1 ) ) )
58 10 13 16 19 36 57 nn0indd 
 |-  ( ( ph /\ N e. NN0 ) -> ( F ` ( N .^ X ) ) = ( ( F ` X ) ^ N ) )
59 7 58 mpdan 
 |-  ( ph -> ( F ` ( N .^ X ) ) = ( ( F ` X ) ^ N ) )