Theorem evls1expd

Description: Univariate polynomial evaluation builder for an exponential. See also evl1expd . (Contributed by Thierry Arnoux, 24-Jan-2025)

	Ref	Expression
Hypotheses	evls1expd.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
	evls1expd.k	$$⊢K={\mathrm{Base}}_S$$
	evls1expd.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
	evls1expd.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	evls1expd.b	$$⊢B={\mathrm{Base}}_W$$
	evls1expd.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evls1expd.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	evls1expd.1	$$⊢\underset{\dot{}}{\wedge }={\cdot }_{{\mathrm{mulGrp}}_W}$$
	evls1expd.2	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
	evls1expd.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	evls1expd.m	$$⊢\phi \to M\in B$$
	evls1expd.c	$$⊢\phi \to C\in K$$
Assertion	evls1expd	$$⊢\phi \to Q\left(N\underset{\dot{}}{\wedge }M\right)\left(C\right)=N\underset{\dot{}}{\times }Q\left(M\right)\left(C\right)$$

Proof

Step	Hyp	Ref	Expression
1		evls1expd.q	$$⊢Q=S{\mathrm{evalSub}}_{1}R$$
2		evls1expd.k	$$⊢K={\mathrm{Base}}_S$$
3		evls1expd.w	$$⊢W={\mathrm{Poly}}_1\left(U\right)$$
4		evls1expd.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
5		evls1expd.b	$$⊢B={\mathrm{Base}}_W$$
6		evls1expd.s	$$⊢\phi \to S\in \mathrm{CRing}$$
7		evls1expd.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
8		evls1expd.1	$$⊢\underset{\dot{}}{\wedge }={\cdot }_{{\mathrm{mulGrp}}_W}$$
9		evls1expd.2	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_S}$$
10		evls1expd.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11		evls1expd.m	$$⊢\phi \to M\in B$$
12		evls1expd.c	$$⊢\phi \to C\in K$$
13		eqid	$$⊢{\mathrm{mulGrp}}_W={\mathrm{mulGrp}}_W$$
14	1 4 3 13 2 5 8 6 7 10 11	evls1pw	$$⊢\phi \to Q\left(N\underset{\dot{}}{\wedge }M\right)=N{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}}Q\left(M\right)$$
15	14	fveq1d	$$⊢\phi \to Q\left(N\underset{\dot{}}{\wedge }M\right)\left(C\right)=\left(N{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}}Q\left(M\right)\right)\left(C\right)$$
16		eqid	$$⊢S{\uparrow }_{𝑠}K=S{\uparrow }_{𝑠}K$$
17		eqid	$$⊢{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}={\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
18		eqid	$$⊢{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}={\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
19		eqid	$$⊢{\mathrm{mulGrp}}_S={\mathrm{mulGrp}}_S$$
20		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}}={\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}}$$
21	6	crngringd	$$⊢\phi \to S\in \mathrm{Ring}$$
22	2	fvexi	$$⊢K\in \mathrm{V}$$
23	22	a1i	$$⊢\phi \to K\in \mathrm{V}$$
24	1 2 16 4 3	evls1rhm	$$⊢\left(S\in \mathrm{CRing}\wedge R\in \mathrm{SubRing}\left(S\right)\right)\to Q\in \left(W\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)$$
25	6 7 24	syl2anc	$$⊢\phi \to Q\in \left(W\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)$$
26	5 17	rhmf	$$⊢Q\in \left(W\mathrm{RingHom}\left(S{\uparrow }_{𝑠}K\right)\right)\to Q:B⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
27	25 26	syl	$$⊢\phi \to Q:B⟶{\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
28	27 11	ffvelcdmd	$$⊢\phi \to Q\left(M\right)\in {\mathrm{Base}}_{\left(S{\uparrow }_{𝑠}K\right)}$$
29	16 17 18 19 20 9 21 23 10 28 12	pwsexpg	$$⊢\phi \to \left(N{\cdot }_{{\mathrm{mulGrp}}_{\left(S{\uparrow }_{𝑠}K\right)}}Q\left(M\right)\right)\left(C\right)=N\underset{\dot{}}{\times }Q\left(M\right)\left(C\right)$$
30	15 29	eqtrd	$$⊢\phi \to Q\left(N\underset{\dot{}}{\wedge }M\right)\left(C\right)=N\underset{\dot{}}{\times }Q\left(M\right)\left(C\right)$$