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	$$⊢S{\uparrow }_{𝑠}\left(K^I\right)=S{\uparrow }_{𝑠}\left(K^I\right)$$
15	1 2 3 14 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)$$
16	6 7 8 15	syl3anc	$$⊢\phi \to Q\in \left(P\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)$$
17		rhmrcl1	$$⊢Q\in \left(P\mathrm{RingHom}\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)\right)\to P\in \mathrm{Ring}$$
18		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
19	18	ringmgp	$$⊢P\in \mathrm{Ring}\to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
20	16 17 19	3syl	$$⊢\phi \to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
21	10	simpld	$$⊢\phi \to M\in B$$
22	18 5	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_P}$$
23	22 11	mulgnn0cl	$$⊢\left({\mathrm{mulGrp}}_P\in \mathrm{Mnd}\wedge N\in {\mathbb{N}}_0\wedge M\in B\right)\to N\underset{\dot{}}{\bullet }M\in B$$
24	20 13 21 23	syl3anc	$$⊢\phi \to N\underset{\dot{}}{\bullet }M\in B$$
25		eqid	$$⊢{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}={\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
26	1 2 18 11 3 14 25 4 5 6 7 8 13 21	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)$$
27	26	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)$$
28		eqid	$$⊢{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}={\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
29		eqid	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_S$$
30		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}={\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}}$$
31	7	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
32		ovexd	$$⊢\phi \to K^I\in \mathrm{V}$$
33	5 28	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)}$$
34	16 33	syl	$$⊢\phi \to Q:B⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
35	34 21	ffvelrnd	$$⊢\phi \to Q\left(M\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}\left(K^I\right)\right)}$$
36	14 28 25 29 30 12 31 32 13 35 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)$$
37	10	simprd	$$⊢\phi \to Q\left(M\right)\left(A\right)=V$$
38	37	oveq2d	$$⊢\phi \to N\underset{\dot{}}{\times }Q\left(M\right)\left(A\right)=N\underset{\dot{}}{\times }V$$
39	27 36 38	3eqtrd	$$⊢\phi \to Q\left(N\underset{\dot{}}{\bullet }M\right)\left(A\right)=N\underset{\dot{}}{\times }V$$
40	24 39	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)$$