Theorem evls1val

Description: Value of the univariate polynomial evaluation map. (Contributed by AV, 10-Sep-2019)

	Ref	Expression
Hypotheses	evls1fval.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
	evls1fval.e	⊢ 𝐸 = ( 1o evalSub 𝑆 )
	evls1fval.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evls1val.m	⊢ 𝑀 = ( 1o mPoly ( 𝑆 ↾s 𝑅 ) )
	evls1val.k	⊢ 𝐾 = ( Base ‘ 𝑀 )
Assertion	evls1val	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → ( 𝑄 ‘ 𝐴 ) = ( ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		evls1fval.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2		evls1fval.e	⊢ 𝐸 = ( 1o evalSub 𝑆 )
3		evls1fval.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		evls1val.m	⊢ 𝑀 = ( 1o mPoly ( 𝑆 ↾s 𝑅 ) )
5		evls1val.k	⊢ 𝐾 = ( Base ‘ 𝑀 )
6	3	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐵 )
7	6	adantl	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅 ⊆ 𝐵 )
8		elpwg	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵 ) )
9	8	adantl	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑅 ∈ 𝒫 𝐵 ↔ 𝑅 ⊆ 𝐵 ) )
10	7 9	mpbird	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑅 ∈ 𝒫 𝐵 )
11	1 2 3	evls1fval	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ 𝒫 𝐵 ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸 ‘ 𝑅 ) ) )
12	10 11	syldan	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸 ‘ 𝑅 ) ) )
13	12	fveq1d	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝑄 ‘ 𝐴 ) = ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸 ‘ 𝑅 ) ) ‘ 𝐴 ) )
14	13	3adant3	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → ( 𝑄 ‘ 𝐴 ) = ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸 ‘ 𝑅 ) ) ‘ 𝐴 ) )
15		1on	⊢ 1o ∈ On
16		simp1	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → 𝑆 ∈ CRing )
17		simp2	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
18	2	fveq1i	⊢ ( 𝐸 ‘ 𝑅 ) = ( ( 1o evalSub 𝑆 ) ‘ 𝑅 )
19		eqid	⊢ ( 𝑆 ↾s 𝑅 ) = ( 𝑆 ↾s 𝑅 )
20		eqid	⊢ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) = ( 𝑆 ↑s ( 𝐵 ↑m 1o ) )
21	18 4 19 20 3	evlsrhm	⊢ ( ( 1o ∈ On ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( 𝐸 ‘ 𝑅 ) ∈ ( 𝑀 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
22	15 16 17 21	mp3an2i	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → ( 𝐸 ‘ 𝑅 ) ∈ ( 𝑀 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
23		eqid	⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) )
24	5 23	rhmf	⊢ ( ( 𝐸 ‘ 𝑅 ) ∈ ( 𝑀 RingHom ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) → ( 𝐸 ‘ 𝑅 ) : 𝐾 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
25	22 24	syl	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → ( 𝐸 ‘ 𝑅 ) : 𝐾 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
26		simp3	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ 𝐾 )
27		fvco3	⊢ ( ( ( 𝐸 ‘ 𝑅 ) : 𝐾 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) ∧ 𝐴 ∈ 𝐾 ) → ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸 ‘ 𝑅 ) ) ‘ 𝐴 ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ) )
28	25 26 27	syl2anc	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → ( ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 𝐸 ‘ 𝑅 ) ) ‘ 𝐴 ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ) )
29	25 26	ffvelcdmd	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
30		ovex	⊢ ( 𝐵 ↑m 1o ) ∈ V
31	20 3	pwsbas	⊢ ( ( 𝑆 ∈ CRing ∧ ( 𝐵 ↑m 1o ) ∈ V ) → ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
32	16 30 31	sylancl	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 1o ) ) ) )
33	29 32	eleqtrrd	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) )
34		coeq1	⊢ ( 𝑥 = ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) → ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
35		eqid	⊢ ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
36		fvex	⊢ ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ∈ V
37	3	fvexi	⊢ 𝐵 ∈ V
38	37	mptex	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ∈ V
39	36 38	coex	⊢ ( ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ V
40	34 35 39	fvmpt	⊢ ( ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ) = ( ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
41	33 40	syl	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ) = ( ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
42	14 28 41	3eqtrd	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ 𝐴 ∈ 𝐾 ) → ( 𝑄 ‘ 𝐴 ) = ( ( ( 𝐸 ‘ 𝑅 ) ‘ 𝐴 ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )