evls1fvcl

Description: Variant of fveval1fvcl for the subring evaluation function evalSub1 (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	evls1maprhm.q	⊢ 𝑂 = ( 𝑅 evalSub₁ 𝑆 )
	evls1maprhm.p	⊢ 𝑃 = ( Poly₁ ‘ ( 𝑅 ↾_s 𝑆 ) )
	evls1maprhm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evls1maprhm.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	evls1maprhm.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evls1maprhm.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
	evls1fvcl.1	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	evls1fvcl.2	⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
Assertion	evls1fvcl	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		evls1maprhm.q	⊢ 𝑂 = ( 𝑅 evalSub₁ 𝑆 )
2		evls1maprhm.p	⊢ 𝑃 = ( Poly₁ ‘ ( 𝑅 ↾_s 𝑆 ) )
3		evls1maprhm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		evls1maprhm.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
5		evls1maprhm.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		evls1maprhm.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7		evls1fvcl.1	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		evls1fvcl.2	⊢ ( 𝜑 → 𝑀 ∈ 𝑈 )
9		eqid	⊢ ( 𝑅 ↾_s 𝑆 ) = ( 𝑅 ↾_s 𝑆 )
10		eqid	⊢ ( eval₁ ‘ 𝑅 ) = ( eval₁ ‘ 𝑅 )
11	1 3 2 9 4 10 5 6	ressply1evl	⊢ ( 𝜑 → 𝑂 = ( ( eval₁ ‘ 𝑅 ) ↾ 𝑈 ) )
12	11	fveq1d	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) = ( ( ( eval₁ ‘ 𝑅 ) ↾ 𝑈 ) ‘ 𝑀 ) )
13	8	fvresd	⊢ ( 𝜑 → ( ( ( eval₁ ‘ 𝑅 ) ↾ 𝑈 ) ‘ 𝑀 ) = ( ( eval₁ ‘ 𝑅 ) ‘ 𝑀 ) )
14	12 13	eqtrd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑀 ) = ( ( eval₁ ‘ 𝑅 ) ‘ 𝑀 ) )
15	14	fveq1d	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) = ( ( ( eval₁ ‘ 𝑅 ) ‘ 𝑀 ) ‘ 𝑌 ) )
16		eqid	⊢ ( Poly₁ ‘ 𝑅 ) = ( Poly₁ ‘ 𝑅 )
17		eqid	⊢ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) = ( Base ‘ ( Poly₁ ‘ 𝑅 ) )
18		eqid	⊢ ( ( Poly₁ ‘ 𝑅 ) ↾_s 𝑈 ) = ( ( Poly₁ ‘ 𝑅 ) ↾_s 𝑈 )
19	16 9 2 4 6 18	ressply1bas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ ( ( Poly₁ ‘ 𝑅 ) ↾_s 𝑈 ) ) )
20	18 17	ressbasss	⊢ ( Base ‘ ( ( Poly₁ ‘ 𝑅 ) ↾_s 𝑈 ) ) ⊆ ( Base ‘ ( Poly₁ ‘ 𝑅 ) )
21	19 20	eqsstrdi	⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
22	21 8	sseldd	⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
23	10 16 3 17 5 7 22	fveval1fvcl	⊢ ( 𝜑 → ( ( ( eval₁ ‘ 𝑅 ) ‘ 𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )
24	15 23	eqeltrd	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )

Metamath Proof Explorer

Theorem evls1fvcl

Proof