Theorem pwsexpg

Description: Value of a group exponentiation in a structure power. Compare pwsmulg . (Contributed by SN, 30-Jul-2024)

	Ref	Expression
Hypotheses	pwsexpg.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
	pwsexpg.b	$$⊢B={\mathrm{Base}}_Y$$
	pwsexpg.m	$$⊢M={\mathrm{mulGrp}}_Y$$
	pwsexpg.t	$$⊢T={\mathrm{mulGrp}}_R$$
	pwsexpg.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_M$$
	pwsexpg.g	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
	pwsexpg.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	pwsexpg.i	$$⊢\phi \to I\in V$$
	pwsexpg.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	pwsexpg.x	$$⊢\phi \to X\in B$$
	pwsexpg.a	$$⊢\phi \to A\in I$$
Assertion	pwsexpg	$$⊢\phi \to \left(N\underset{\dot{}}{\bullet }X\right)\left(A\right)=N\underset{\dot{}}{·}X\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwsexpg.y	$$⊢Y=R{\uparrow }_{𝑠}I$$
2		pwsexpg.b	$$⊢B={\mathrm{Base}}_Y$$
3		pwsexpg.m	$$⊢M={\mathrm{mulGrp}}_Y$$
4		pwsexpg.t	$$⊢T={\mathrm{mulGrp}}_R$$
5		pwsexpg.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_M$$
6		pwsexpg.g	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
7		pwsexpg.r	$$⊢\phi \to R\in \mathrm{Ring}$$
8		pwsexpg.i	$$⊢\phi \to I\in V$$
9		pwsexpg.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
10		pwsexpg.x	$$⊢\phi \to X\in B$$
11		pwsexpg.a	$$⊢\phi \to A\in I$$
12	1 2 3 4 7 8 11	pwspjmhmmgpd	$$⊢\phi \to \left(x\in B⟼x\left(A\right)\right)\in \left(M\mathrm{MndHom}T\right)$$
13	3 2	mgpbas	$$⊢B={\mathrm{Base}}_M$$
14	13 5 6	mhmmulg	$$⊢\left(\left(x\in B⟼x\left(A\right)\right)\in \left(M\mathrm{MndHom}T\right)\wedge N\in {\mathbb{N}}_0\wedge X\in B\right)\to \left(x\in B⟼x\left(A\right)\right)\left(N\underset{\dot{}}{\bullet }X\right)=N\underset{\dot{}}{·}\left(x\in B⟼x\left(A\right)\right)\left(X\right)$$
15	12 9 10 14	syl3anc	$$⊢\phi \to \left(x\in B⟼x\left(A\right)\right)\left(N\underset{\dot{}}{\bullet }X\right)=N\underset{\dot{}}{·}\left(x\in B⟼x\left(A\right)\right)\left(X\right)$$
16	1	pwsring	$$⊢\left(R\in \mathrm{Ring}\wedge I\in V\right)\to Y\in \mathrm{Ring}$$
17	7 8 16	syl2anc	$$⊢\phi \to Y\in \mathrm{Ring}$$
18	3	ringmgp	$$⊢Y\in \mathrm{Ring}\to M\in \mathrm{Mnd}$$
19	17 18	syl	$$⊢\phi \to M\in \mathrm{Mnd}$$
20	13 5	mulgnn0cl	$$⊢\left(M\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\wedge X\in B\right)\to N\underset{\dot{}}{\bullet }X\in B$$
21	19 9 10 20	syl3anc	$$⊢\phi \to N\underset{\dot{}}{\bullet }X\in B$$
22		fveq1	$$⊢x=N\underset{\dot{}}{\bullet }X\to x\left(A\right)=\left(N\underset{\dot{}}{\bullet }X\right)\left(A\right)$$
23		eqid	$$⊢\left(x\in B⟼x\left(A\right)\right)=\left(x\in B⟼x\left(A\right)\right)$$
24		fvex	$$⊢\left(N\underset{\dot{}}{\bullet }X\right)\left(A\right)\in \mathrm{V}$$
25	22 23 24	fvmpt	$$⊢N\underset{\dot{}}{\bullet }X\in B\to \left(x\in B⟼x\left(A\right)\right)\left(N\underset{\dot{}}{\bullet }X\right)=\left(N\underset{\dot{}}{\bullet }X\right)\left(A\right)$$
26	21 25	syl	$$⊢\phi \to \left(x\in B⟼x\left(A\right)\right)\left(N\underset{\dot{}}{\bullet }X\right)=\left(N\underset{\dot{}}{\bullet }X\right)\left(A\right)$$
27		fveq1	$$⊢x=X\to x\left(A\right)=X\left(A\right)$$
28		fvex	$$⊢X\left(A\right)\in \mathrm{V}$$
29	27 23 28	fvmpt	$$⊢X\in B\to \left(x\in B⟼x\left(A\right)\right)\left(X\right)=X\left(A\right)$$
30	10 29	syl	$$⊢\phi \to \left(x\in B⟼x\left(A\right)\right)\left(X\right)=X\left(A\right)$$
31	30	oveq2d	$$⊢\phi \to N\underset{\dot{}}{·}\left(x\in B⟼x\left(A\right)\right)\left(X\right)=N\underset{\dot{}}{·}X\left(A\right)$$
32	15 26 31	3eqtr3d	$$⊢\phi \to \left(N\underset{\dot{}}{\bullet }X\right)\left(A\right)=N\underset{\dot{}}{·}X\left(A\right)$$