Theorem evlsexpval

Description: Polynomial evaluation builder for exponentiation. (Contributed by SN, 27-Jul-2024)

	Ref	Expression
Hypotheses	evlsaddval.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
	evlsaddval.p	$$⊢P=I\mathrm{mPoly}U$$
	evlsaddval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evlsaddval.k	$$⊢K={\mathrm{Base}}_S$$
	evlsaddval.b	$$⊢B={\mathrm{Base}}_P$$
	evlsaddval.i	$$⊢\phi \to I\in Z$$
	evlsaddval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlsaddval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evlsaddval.a	$$⊢\phi \to A\in \left(K^I\right)$$
	evlsaddval.m	$$⊢\phi \to \left(M\in B\wedge Q\left(M\right)\left(A\right)=V\right)$$
	evlsexpval.g	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	evlsexpval.f	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
	evlsexpval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	evlsexpval	$$⊢\phi \to \left(N\underset{\dot{}}{\bullet }M\in B\wedge Q\left(N\underset{\dot{}}{\bullet }M\right)\left(A\right)=N\underset{\dot{}}{\times }V\right)$$

Proof

Step	Hyp	Ref	Expression
1		evlsaddval.q	$$⊢Q=\left(I\mathrm{evalSub}S\right)\left(R\right)$$
2		evlsaddval.p	$$⊢P=I\mathrm{mPoly}U$$
3		evlsaddval.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
4		evlsaddval.k	$$⊢K={\mathrm{Base}}_S$$
5		evlsaddval.b	$$⊢B={\mathrm{Base}}_P$$
6		evlsaddval.i	$$⊢\phi \to I\in Z$$
7		evlsaddval.s	$$⊢\phi \to S\in \mathrm{CRing}$$
8		evlsaddval.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
9		evlsaddval.a	$$⊢\phi \to A\in \left(K^I\right)$$
10		evlsaddval.m	$$⊢\phi \to \left(M\in B\wedge Q\left(M\right)\left(A\right)=V\right)$$
11		evlsexpval.g	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{{\mathrm{mulGrp}}_P}$$
12		evlsexpval.f	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
13		evlsexpval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
14		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
15	14 5	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_P}$$
16		eqid	$$⊢S{\uparrow }_{𝑠}\left(K^I\right)=S{\uparrow }_{𝑠}\left(K^I\right)$$
17	1 2 3 16 4	evlsrhm	$$⊢\left(I\in Z\wedge S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)\to Q\in \left(P\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)$$
18	6 7 8 17	syl3anc	$$⊢\phi \to Q\in \left(P\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)$$
19		rhmrcl1	$$⊢Q\in \left(P\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)\to P\in \mathrm{Ring}$$
20	14	ringmgp	$$⊢P\in \mathrm{Ring}\to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
21	18 19 20	3syl	$$⊢\phi \to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
22	10	simpld	$$⊢\phi \to M\in B$$
23	15 11 21 13 22	mulgnn0cld	$$⊢\phi \to N\underset{\dot{}}{\bullet }M\in B$$
24		eqid	$$⊢{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}={\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
25	1 2 14 11 3 16 24 4 5 6 7 8 13 22	evlspw	$$⊢\phi \to Q\left(N\underset{\dot{}}{\bullet }M\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}Q\left(M\right)$$
26	25	fveq1d	$$⊢\phi \to Q\left(N\underset{\dot{}}{\bullet }M\right)\left(A\right)=\left(N{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}Q\left(M\right)\right)\left(A\right)$$
27		eqid	$$⊢{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}={\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
28		eqid	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_S$$
29		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}={\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}$$
30	7	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
31		ovexd	$$⊢\phi \to K^I\in \mathrm{V}$$
32	5 27	rhmf	$$⊢Q\in \left(P\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)\to Q:B⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
33	18 32	syl	$$⊢\phi \to Q:B⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
34	33 22	ffvelcdmd	$$⊢\phi \to Q\left(M\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
35	16 27 24 28 29 12 30 31 13 34 9	pwsexpg	$$⊢\phi \to \left(N{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}Q\left(M\right)\right)\left(A\right)=N\underset{\dot{}}{\times }Q\left(M\right)\left(A\right)$$
36	10	simprd	$$⊢\phi \to Q\left(M\right)\left(A\right)=V$$
37	36	oveq2d	$$⊢\phi \to N\underset{\dot{}}{\times }Q\left(M\right)\left(A\right)=N\underset{\dot{}}{\times }V$$
38	26 35 37	3eqtrd	$$⊢\phi \to Q\left(N\underset{\dot{}}{\bullet }M\right)\left(A\right)=N\underset{\dot{}}{\times }V$$
39	23 38	jca	$$⊢\phi \to \left(N\underset{\dot{}}{\bullet }M\in B\wedge Q\left(N\underset{\dot{}}{\bullet }M\right)\left(A\right)=N\underset{\dot{}}{\times }V\right)$$