evls1expd

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

	Ref	Expression
Hypotheses	evls1expd.q	⊢ 𝑄 = ( 𝑆 evalSub₁ 𝑅 )
	evls1expd.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	evls1expd.w	⊢ 𝑊 = ( Poly₁ ‘ 𝑈 )
	evls1expd.u	⊢ 𝑈 = ( 𝑆 ↾_s 𝑅 )
	evls1expd.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	evls1expd.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evls1expd.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evls1expd.1	⊢ ∧ = ( ._g ‘ ( mulGrp ‘ 𝑊 ) )
	evls1expd.2	⊢ ↑ = ( ._g ‘ ( mulGrp ‘ 𝑆 ) )
	evls1expd.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
	evls1expd.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
	evls1expd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion	evls1expd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑀 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evls1expd.q	⊢ 𝑄 = ( 𝑆 evalSub₁ 𝑅 )
2		evls1expd.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
3		evls1expd.w	⊢ 𝑊 = ( Poly₁ ‘ 𝑈 )
4		evls1expd.u	⊢ 𝑈 = ( 𝑆 ↾_s 𝑅 )
5		evls1expd.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
6		evls1expd.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
7		evls1expd.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8		evls1expd.1	⊢ ∧ = ( ._g ‘ ( mulGrp ‘ 𝑊 ) )
9		evls1expd.2	⊢ ↑ = ( ._g ‘ ( mulGrp ‘ 𝑆 ) )
10		evls1expd.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
11		evls1expd.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
12		evls1expd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
13		eqid	⊢ ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ 𝑊 )
14	1 4 3 13 2 5 8 6 7 10 11	evls1pw	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ∧ 𝑀 ) ) = ( 𝑁 ( ._g ‘ ( mulGrp ‘ ( 𝑆 ↑_s 𝐾 ) ) ) ( 𝑄 ‘ 𝑀 ) ) )
15	14	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑀 ) ) ‘ 𝐶 ) = ( ( 𝑁 ( ._g ‘ ( mulGrp ‘ ( 𝑆 ↑_s 𝐾 ) ) ) ( 𝑄 ‘ 𝑀 ) ) ‘ 𝐶 ) )
16		eqid	⊢ ( 𝑆 ↑_s 𝐾 ) = ( 𝑆 ↑_s 𝐾 )
17		eqid	⊢ ( Base ‘ ( 𝑆 ↑_s 𝐾 ) ) = ( Base ‘ ( 𝑆 ↑_s 𝐾 ) )
18		eqid	⊢ ( mulGrp ‘ ( 𝑆 ↑_s 𝐾 ) ) = ( mulGrp ‘ ( 𝑆 ↑_s 𝐾 ) )
19		eqid	⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
20		eqid	⊢ ( ._g ‘ ( mulGrp ‘ ( 𝑆 ↑_s 𝐾 ) ) ) = ( ._g ‘ ( mulGrp ‘ ( 𝑆 ↑_s 𝐾 ) ) )
21	6	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
22	2	fvexi	⊢ 𝐾 ∈ V
23	22	a1i	⊢ ( 𝜑 → 𝐾 ∈ V )
24	1 2 16 4 3	evls1rhm	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑_s 𝐾 ) ) )
25	6 7 24	syl2anc	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑_s 𝐾 ) ) )
26	5 17	rhmf	⊢ ( 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑_s 𝐾 ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑_s 𝐾 ) ) )
27	25 26	syl	⊢ ( 𝜑 → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑_s 𝐾 ) ) )
28	27 11	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑆 ↑_s 𝐾 ) ) )
29	16 17 18 19 20 9 21 23 10 28 12	pwsexpg	⊢ ( 𝜑 → ( ( 𝑁 ( ._g ‘ ( mulGrp ‘ ( 𝑆 ↑_s 𝐾 ) ) ) ( 𝑄 ‘ 𝑀 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) ) )
30	15 29	eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑀 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) ) )

Metamath Proof Explorer

Theorem evls1expd

Proof