Theorem abvexp

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

	Ref	Expression
Hypotheses	abvexp.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
	abvexp.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
	abvexp.b	$$⊢B={\mathrm{Base}}_R$$
	abvexp.r	$$⊢\phi \to R\in \mathrm{NzRing}$$
	abvexp.f	$$⊢\phi \to F\in A$$
	abvexp.x	$$⊢\phi \to X\in B$$
	abvexp.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	abvexp	$$⊢\phi \to F\left(N\underset{\dot{}}{\times }X\right)={F\left(X\right)}^N$$

Proof

Step	Hyp	Ref	Expression
1		abvexp.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvexp.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
3		abvexp.b	$$⊢B={\mathrm{Base}}_R$$
4		abvexp.r	$$⊢\phi \to R\in \mathrm{NzRing}$$
5		abvexp.f	$$⊢\phi \to F\in A$$
6		abvexp.x	$$⊢\phi \to X\in B$$
7		abvexp.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
8		fvoveq1	$$⊢x=0\to F\left(x\underset{\dot{}}{\times }X\right)=F\left(0\underset{\dot{}}{\times }X\right)$$
9		oveq2	$$⊢x=0\to {F\left(X\right)}^x={F\left(X\right)}^0$$
10	8 9	eqeq12d	$$⊢x=0\to \left(F\left(x\underset{\dot{}}{\times }X\right)={F\left(X\right)}^x\leftrightarrow F\left(0\underset{\dot{}}{\times }X\right)={F\left(X\right)}^0\right)$$
11		fvoveq1	$$⊢x=y\to F\left(x\underset{\dot{}}{\times }X\right)=F\left(y\underset{\dot{}}{\times }X\right)$$
12		oveq2	$$⊢x=y\to {F\left(X\right)}^x={F\left(X\right)}^y$$
13	11 12	eqeq12d	$$⊢x=y\to \left(F\left(x\underset{\dot{}}{\times }X\right)={F\left(X\right)}^x\leftrightarrow F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)$$
14		fvoveq1	$$⊢x=y+1\to F\left(x\underset{\dot{}}{\times }X\right)=F\left(\left(y+1\right)\underset{\dot{}}{\times }X\right)$$
15		oveq2	$$⊢x=y+1\to {F\left(X\right)}^x={F\left(X\right)}^{y+1}$$
16	14 15	eqeq12d	$$⊢x=y+1\to \left(F\left(x\underset{\dot{}}{\times }X\right)={F\left(X\right)}^x\leftrightarrow F\left(\left(y+1\right)\underset{\dot{}}{\times }X\right)={F\left(X\right)}^{y+1}\right)$$
17		fvoveq1	$$⊢x=N\to F\left(x\underset{\dot{}}{\times }X\right)=F\left(N\underset{\dot{}}{\times }X\right)$$
18		oveq2	$$⊢x=N\to {F\left(X\right)}^x={F\left(X\right)}^N$$
19	17 18	eqeq12d	$$⊢x=N\to \left(F\left(x\underset{\dot{}}{\times }X\right)={F\left(X\right)}^x\leftrightarrow F\left(N\underset{\dot{}}{\times }X\right)={F\left(X\right)}^N\right)$$
20		eqid	$$⊢1_R=1_R$$
21		eqid	$$⊢0_R=0_R$$
22	20 21	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne 0_R$$
23	4 22	syl	$$⊢\phi \to 1_R\ne 0_R$$
24	1 20 21	abv1z	$$⊢\left(F\in A\wedge 1_R\ne 0_R\right)\to F\left(1_R\right)=1$$
25	5 23 24	syl2anc	$$⊢\phi \to F\left(1_R\right)=1$$
26		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
27	26 3	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
28	26 20	ringidval	$$⊢1_R=0_{{\mathrm{mulGrp}}_R}$$
29	27 28 2	mulg0	$$⊢X\in B\to 0\underset{\dot{}}{\times }X=1_R$$
30	6 29	syl	$$⊢\phi \to 0\underset{\dot{}}{\times }X=1_R$$
31	30	fveq2d	$$⊢\phi \to F\left(0\underset{\dot{}}{\times }X\right)=F\left(1_R\right)$$
32	1 3	abvcl	$$⊢\left(F\in A\wedge X\in B\right)\to F\left(X\right)\in ℝ$$
33	5 6 32	syl2anc	$$⊢\phi \to F\left(X\right)\in ℝ$$
34	33	recnd	$$⊢\phi \to F\left(X\right)\in ℂ$$
35	34	exp0d	$$⊢\phi \to {F\left(X\right)}^0=1$$
36	25 31 35	3eqtr4d	$$⊢\phi \to F\left(0\underset{\dot{}}{\times }X\right)={F\left(X\right)}^0$$
37	5	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to F\in A$$
38		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
39	26	ringmgp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
40	4 38 39	3syl	$$⊢\phi \to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
41	40	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to {\mathrm{mulGrp}}_R\in \mathrm{Mnd}$$
42		simplr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to y\in {\mathbb{N}}_0$$
43	6	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to X\in B$$
44	27 2 41 42 43	mulgnn0cld	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to y\underset{\dot{}}{\times }X\in B$$
45		eqid	$$⊢{\cdot }_R={\cdot }_R$$
46	1 3 45	abvmul	$$⊢\left(F\in A\wedge y\underset{\dot{}}{\times }X\in B\wedge X\in B\right)\to F\left(\left(y\underset{\dot{}}{\times }X\right){\cdot }_{R}X\right)=F\left(y\underset{\dot{}}{\times }X\right)F\left(X\right)$$
47	37 44 43 46	syl3anc	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to F\left(\left(y\underset{\dot{}}{\times }X\right){\cdot }_{R}X\right)=F\left(y\underset{\dot{}}{\times }X\right)F\left(X\right)$$
48		simpr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y$$
49	48	oveq1d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to F\left(y\underset{\dot{}}{\times }X\right)F\left(X\right)={F\left(X\right)}^{y}F\left(X\right)$$
50	47 49	eqtrd	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to F\left(\left(y\underset{\dot{}}{\times }X\right){\cdot }_{R}X\right)={F\left(X\right)}^{y}F\left(X\right)$$
51	26 45	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
52	27 2 51	mulgnn0p1	$$⊢\left({\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge X\in B\right)\to \left(y+1\right)\underset{\dot{}}{\times }X=\left(y\underset{\dot{}}{\times }X\right){\cdot }_{R}X$$
53	41 42 43 52	syl3anc	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to \left(y+1\right)\underset{\dot{}}{\times }X=\left(y\underset{\dot{}}{\times }X\right){\cdot }_{R}X$$
54	53	fveq2d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to F\left(\left(y+1\right)\underset{\dot{}}{\times }X\right)=F\left(\left(y\underset{\dot{}}{\times }X\right){\cdot }_{R}X\right)$$
55	34	ad2antrr	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to F\left(X\right)\in ℂ$$
56	55 42	expp1d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to {F\left(X\right)}^{y+1}={F\left(X\right)}^{y}F\left(X\right)$$
57	50 54 56	3eqtr4d	$$⊢\left(\left(\phi \wedge y\in {\mathbb{N}}_0\right)\wedge F\left(y\underset{\dot{}}{\times }X\right)={F\left(X\right)}^y\right)\to F\left(\left(y+1\right)\underset{\dot{}}{\times }X\right)={F\left(X\right)}^{y+1}$$
58	10 13 16 19 36 57	nn0indd	$$⊢\left(\phi \wedge N\in {\mathbb{N}}_0\right)\to F\left(N\underset{\dot{}}{\times }X\right)={F\left(X\right)}^N$$
59	7 58	mpdan	$$⊢\phi \to F\left(N\underset{\dot{}}{\times }X\right)={F\left(X\right)}^N$$