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 {evalSub}_{1} R$
	evls1expd.k	$⊢ K = {Base}_{S}$
	evls1expd.w	$⊢ W = {Poly}_{1} (U)$
	evls1expd.u	$⊢ U = S ↾_{𝑠} R$
	evls1expd.b	$⊢ B = {Base}_{W}$
	evls1expd.s	$⊢ φ \to S \in CRing$
	evls1expd.r	$⊢ φ \to R \in SubRing (S)$
	evls1expd.1	$⊢ \underset{˙}{\land} = \cdot_{{mulGrp}_{W}}$
	evls1expd.2	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{S}}$
	evls1expd.n	$⊢ φ \to N \in ℕ_{0}$
	evls1expd.m	$⊢ φ \to M \in B$
	evls1expd.c	$⊢ φ \to C \in K$
Assertion	evls1expd	$⊢ φ \to Q (N \underset{˙}{\land} M) (C) = N \underset{˙}{\times} Q (M) (C)$

Proof

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

Metamath Proof Explorer

Theorem evls1expd

Proof