Theorem ressply1evl

Description: Evaluation of a univariate subring polynomial is the same as the evaluation in the bigger ring. (Contributed by Thierry Arnoux, 23-Jan-2025)

	Ref	Expression
Hypotheses	ressply1evl2.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
	ressply1evl2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	ressply1evl2.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
	ressply1evl2.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	ressply1evl2.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	ressply1evl.e	⊢ 𝐸 = ( eval1 ‘ 𝑆 )
	ressply1evl.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	ressply1evl.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
Assertion	ressply1evl	⊢ ( 𝜑 → 𝑄 = ( 𝐸 ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ressply1evl2.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2		ressply1evl2.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
3		ressply1evl2.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4		ressply1evl2.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5		ressply1evl2.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
6		ressply1evl.e	⊢ 𝐸 = ( eval1 ‘ 𝑆 )
7		ressply1evl.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
8		ressply1evl.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
9	6 2	evl1fval1	⊢ 𝐸 = ( 𝑆 evalSub1 𝐾 )
10		eqid	⊢ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) = ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) )
11		eqid	⊢ ( 𝑆 ↾s 𝐾 ) = ( 𝑆 ↾s 𝐾 )
12		eqid	⊢ ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) )
13	7	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → 𝑆 ∈ CRing )
14	7	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
15	2	subrgid	⊢ ( 𝑆 ∈ Ring → 𝐾 ∈ ( SubRing ‘ 𝑆 ) )
16	14 15	syl	⊢ ( 𝜑 → 𝐾 ∈ ( SubRing ‘ 𝑆 ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → 𝐾 ∈ ( SubRing ‘ 𝑆 ) )
18		eqid	⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
19		eqid	⊢ ( PwSer1 ‘ 𝑈 ) = ( PwSer1 ‘ 𝑈 )
20		eqid	⊢ ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑈 ) )
21		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
22	18 4 3 5 8 19 20 21	ressply1bas2	⊢ ( 𝜑 → 𝐵 = ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) )
23		inss2	⊢ ( ( Base ‘ ( PwSer1 ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) )
24	22 23	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
25	2	ressid	⊢ ( 𝑆 ∈ CRing → ( 𝑆 ↾s 𝐾 ) = 𝑆 )
26	7 25	syl	⊢ ( 𝜑 → ( 𝑆 ↾s 𝐾 ) = 𝑆 )
27	26	fveq2d	⊢ ( 𝜑 → ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) = ( Poly1 ‘ 𝑆 ) )
28	27	fveq2d	⊢ ( 𝜑 → ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
29	24 28	sseqtrrd	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) ) )
30	29	sselda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → 𝑚 ∈ ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝐾 ) ) ) )
31		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
32		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑆 ) ) = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
33		eqid	⊢ ( coe1 ‘ 𝑚 ) = ( coe1 ‘ 𝑚 )
34	9 2 10 11 12 13 17 30 31 32 33	evls1fpws	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → ( 𝐸 ‘ 𝑚 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑆 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑚 ) ‘ 𝑘 ) ( .r ‘ 𝑆 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑥 ) ) ) ) ) )
35	8	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
36		simpr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → 𝑚 ∈ 𝐵 )
37	1 2 3 4 5 13 35 36 31 32 33	evls1fpws	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → ( 𝑄 ‘ 𝑚 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑆 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑚 ) ‘ 𝑘 ) ( .r ‘ 𝑆 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) 𝑥 ) ) ) ) ) )
38	34 37	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐵 ) → ( 𝐸 ‘ 𝑚 ) = ( 𝑄 ‘ 𝑚 ) )
39	38	ralrimiva	⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝐵 ( 𝐸 ‘ 𝑚 ) = ( 𝑄 ‘ 𝑚 ) )
40		eqid	⊢ ( 𝑆 ↑s 𝐾 ) = ( 𝑆 ↑s 𝐾 )
41	6 18 40 2	evl1rhm	⊢ ( 𝑆 ∈ CRing → 𝐸 ∈ ( ( Poly1 ‘ 𝑆 ) RingHom ( 𝑆 ↑s 𝐾 ) ) )
42		eqid	⊢ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) = ( Base ‘ ( 𝑆 ↑s 𝐾 ) )
43	21 42	rhmf	⊢ ( 𝐸 ∈ ( ( Poly1 ‘ 𝑆 ) RingHom ( 𝑆 ↑s 𝐾 ) ) → 𝐸 : ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
44	7 41 43	3syl	⊢ ( 𝜑 → 𝐸 : ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
45	44	ffnd	⊢ ( 𝜑 → 𝐸 Fn ( Base ‘ ( Poly1 ‘ 𝑆 ) ) )
46	1 2 40 4 3	evls1rhm	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) )
47	7 8 46	syl2anc	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) )
48	5 42	rhmf	⊢ ( 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
49	47 48	syl	⊢ ( 𝜑 → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
50	49	ffnd	⊢ ( 𝜑 → 𝑄 Fn 𝐵 )
51		fvreseq1	⊢ ( ( ( 𝐸 Fn ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ∧ 𝑄 Fn 𝐵 ) ∧ 𝐵 ⊆ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) ) → ( ( 𝐸 ↾ 𝐵 ) = 𝑄 ↔ ∀ 𝑚 ∈ 𝐵 ( 𝐸 ‘ 𝑚 ) = ( 𝑄 ‘ 𝑚 ) ) )
52	45 50 24 51	syl21anc	⊢ ( 𝜑 → ( ( 𝐸 ↾ 𝐵 ) = 𝑄 ↔ ∀ 𝑚 ∈ 𝐵 ( 𝐸 ‘ 𝑚 ) = ( 𝑄 ‘ 𝑚 ) ) )
53	39 52	mpbird	⊢ ( 𝜑 → ( 𝐸 ↾ 𝐵 ) = 𝑄 )
54	53	eqcomd	⊢ ( 𝜑 → 𝑄 = ( 𝐸 ↾ 𝐵 ) )