evl1fpws

Description: Evaluation of a univariate polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025)

	Ref	Expression
Hypotheses	evl1fpws.q	⊢ 𝑂 = ( eval₁ ‘ 𝑅 )
	evl1fpws.w	⊢ 𝑊 = ( Poly₁ ‘ 𝑅 )
	evl1fpws.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evl1fpws.u	⊢ 𝑈 = ( Base ‘ 𝑊 )
	evl1fpws.s	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evl1fpws.y	⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
	evl1fpws.1	⊢ · = ( ._r ‘ 𝑅 )
	evl1fpws.2	⊢ ↑ = ( ._g ‘ ( mulGrp ‘ 𝑅 ) )
	evl1fpws.a	⊢ 𝐴 = ( coe₁ ‘ 𝑀 )
Assertion	evl1fpws	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evl1fpws.q	⊢ 𝑂 = ( eval₁ ‘ 𝑅 )
2		evl1fpws.w	⊢ 𝑊 = ( Poly₁ ‘ 𝑅 )
3		evl1fpws.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		evl1fpws.u	⊢ 𝑈 = ( Base ‘ 𝑊 )
5		evl1fpws.s	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		evl1fpws.y	⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
7		evl1fpws.1	⊢ · = ( ._r ‘ 𝑅 )
8		evl1fpws.2	⊢ ↑ = ( ._g ‘ ( mulGrp ‘ 𝑅 ) )
9		evl1fpws.a	⊢ 𝐴 = ( coe₁ ‘ 𝑀 )
10	1 3	evl1fval1	⊢ 𝑂 = ( 𝑅 evalSub₁ 𝐵 )
11	10	fveq1i	⊢ ( 𝑂 ‘ 𝑀 ) = ( ( 𝑅 evalSub₁ 𝐵 ) ‘ 𝑀 )
12		eqid	⊢ ( 𝑅 evalSub₁ 𝐵 ) = ( 𝑅 evalSub₁ 𝐵 )
13		eqid	⊢ ( Poly₁ ‘ ( 𝑅 ↾_s 𝐵 ) ) = ( Poly₁ ‘ ( 𝑅 ↾_s 𝐵 ) )
14		eqid	⊢ ( 𝑅 ↾_s 𝐵 ) = ( 𝑅 ↾_s 𝐵 )
15		eqid	⊢ ( Base ‘ ( Poly₁ ‘ ( 𝑅 ↾_s 𝐵 ) ) ) = ( Base ‘ ( Poly₁ ‘ ( 𝑅 ↾_s 𝐵 ) ) )
16	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
17	3	subrgid	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
18	16 17	syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
19	3	ressid	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾_s 𝐵 ) = 𝑅 )
20	5 19	syl	⊢ ( 𝜑 → ( 𝑅 ↾_s 𝐵 ) = 𝑅 )
21	20	fveq2d	⊢ ( 𝜑 → ( Poly₁ ‘ ( 𝑅 ↾_s 𝐵 ) ) = ( Poly₁ ‘ 𝑅 ) )
22	21 2	eqtr4di	⊢ ( 𝜑 → ( Poly₁ ‘ ( 𝑅 ↾_s 𝐵 ) ) = 𝑊 )
23	22	fveq2d	⊢ ( 𝜑 → ( Base ‘ ( Poly₁ ‘ ( 𝑅 ↾_s 𝐵 ) ) ) = ( Base ‘ 𝑊 ) )
24	23 4	eqtr4di	⊢ ( 𝜑 → ( Base ‘ ( Poly₁ ‘ ( 𝑅 ↾_s 𝐵 ) ) ) = 𝑈 )
25	6 24	eleqtrrd	⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( Poly₁ ‘ ( 𝑅 ↾_s 𝐵 ) ) ) )
26	12 3 13 14 15 5 18 25 7 8 9	evls1fpws	⊢ ( 𝜑 → ( ( 𝑅 evalSub₁ 𝐵 ) ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ) )
27	11 26	eqtrid	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ) )

Metamath Proof Explorer

Theorem evl1fpws

Proof