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 evalSub1 R )
	evls1expd.k	\|- K = ( Base ` S )
	evls1expd.w	\|- W = ( Poly1 ` U )
	evls1expd.u	\|- U = ( S \|`s R )
	evls1expd.b	\|- B = ( Base ` W )
	evls1expd.s	\|- ( ph -> S e. CRing )
	evls1expd.r	\|- ( ph -> R e. ( SubRing ` S ) )
	evls1expd.1	\|- ./\ = ( .g ` ( mulGrp ` W ) )
	evls1expd.2	\|- .^ = ( .g ` ( mulGrp ` S ) )
	evls1expd.n	\|- ( ph -> N e. NN0 )
	evls1expd.m	\|- ( ph -> M e. B )
	evls1expd.c	\|- ( ph -> C e. K )
Assertion	evls1expd	\|- ( ph -> ( ( Q ` ( N ./\ M ) ) ` C ) = ( N .^ ( ( Q ` M ) ` C ) ) )

Proof

Step	Hyp	Ref	Expression
1		evls1expd.q	\|- Q = ( S evalSub1 R )
2		evls1expd.k	\|- K = ( Base ` S )
3		evls1expd.w	\|- W = ( Poly1 ` U )
4		evls1expd.u	\|- U = ( S \|`s R )
5		evls1expd.b	\|- B = ( Base ` W )
6		evls1expd.s	\|- ( ph -> S e. CRing )
7		evls1expd.r	\|- ( ph -> R e. ( SubRing ` S ) )
8		evls1expd.1	\|- ./\ = ( .g ` ( mulGrp ` W ) )
9		evls1expd.2	\|- .^ = ( .g ` ( mulGrp ` S ) )
10		evls1expd.n	\|- ( ph -> N e. NN0 )
11		evls1expd.m	\|- ( ph -> M e. B )
12		evls1expd.c	\|- ( ph -> C e. K )
13		eqid	\|- ( mulGrp ` W ) = ( mulGrp ` W )
14	1 4 3 13 2 5 8 6 7 10 11	evls1pw	\|- ( ph -> ( Q ` ( N ./\ M ) ) = ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` M ) ) )
15	14	fveq1d	\|- ( ph -> ( ( Q ` ( N ./\ M ) ) ` C ) = ( ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` M ) ) ` C ) )
16		eqid	\|- ( S ^s K ) = ( S ^s K )
17		eqid	\|- ( Base ` ( S ^s K ) ) = ( Base ` ( S ^s K ) )
18		eqid	\|- ( mulGrp ` ( S ^s K ) ) = ( mulGrp ` ( S ^s K ) )
19		eqid	\|- ( mulGrp ` S ) = ( mulGrp ` S )
20		eqid	\|- ( .g ` ( mulGrp ` ( S ^s K ) ) ) = ( .g ` ( mulGrp ` ( S ^s K ) ) )
21	6	crngringd	\|- ( ph -> S e. Ring )
22	2	fvexi	\|- K e. _V
23	22	a1i	\|- ( ph -> K e. _V )
24	1 2 16 4 3	evls1rhm	\|- ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom ( S ^s K ) ) )
25	6 7 24	syl2anc	\|- ( ph -> Q e. ( W RingHom ( S ^s K ) ) )
26	5 17	rhmf	\|- ( Q e. ( W RingHom ( S ^s K ) ) -> Q : B --> ( Base ` ( S ^s K ) ) )
27	25 26	syl	\|- ( ph -> Q : B --> ( Base ` ( S ^s K ) ) )
28	27 11	ffvelcdmd	\|- ( ph -> ( Q ` M ) e. ( Base ` ( S ^s K ) ) )
29	16 17 18 19 20 9 21 23 10 28 12	pwsexpg	\|- ( ph -> ( ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` M ) ) ` C ) = ( N .^ ( ( Q ` M ) ` C ) ) )
30	15 29	eqtrd	\|- ( ph -> ( ( Q ` ( N ./\ M ) ) ` C ) = ( N .^ ( ( Q ` M ) ` C ) ) )

Metamath Proof Explorer

Theorem evls1expd

Proof