Theorem evls1var

Description: Univariate polynomial evaluation for subrings maps the variable to the identity function. (Contributed by AV, 13-Sep-2019)

	Ref	Expression
Hypotheses	evls1var.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
	evls1var.x	⊢ 𝑋 = ( var1 ‘ 𝑈 )
	evls1var.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evls1var.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evls1var.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evls1var.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
Assertion	evls1var	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑋 ) = ( I ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		evls1var.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2		evls1var.x	⊢ 𝑋 = ( var1 ‘ 𝑈 )
3		evls1var.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4		evls1var.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		evls1var.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
6		evls1var.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
7		eqid	⊢ ( var1 ‘ 𝑆 ) = ( var1 ‘ 𝑆 )
8	7 6 3	subrgvr1	⊢ ( 𝜑 → ( var1 ‘ 𝑆 ) = ( var1 ‘ 𝑈 ) )
9	2 8	eqtr4id	⊢ ( 𝜑 → 𝑋 = ( var1 ‘ 𝑆 ) )
10	9	fveq2d	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑋 ) = ( 𝑄 ‘ ( var1 ‘ 𝑆 ) ) )
11		eqid	⊢ ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 1o evalSub 𝑆 ) ‘ 𝑅 )
12		eqid	⊢ ( 1o eval 𝑆 ) = ( 1o eval 𝑆 )
13		eqid	⊢ ( 1o mVar 𝑈 ) = ( 1o mVar 𝑈 )
14		1on	⊢ 1o ∈ On
15	14	a1i	⊢ ( 𝜑 → 1o ∈ On )
16		0lt1o	⊢ ∅ ∈ 1o
17	16	a1i	⊢ ( 𝜑 → ∅ ∈ 1o )
18	11 12 13 3 4 15 5 6 17	evlsvarsrng	⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 1o mVar 𝑈 ) ‘ ∅ ) ) = ( ( 1o eval 𝑆 ) ‘ ( ( 1o mVar 𝑈 ) ‘ ∅ ) ) )
19	7	vr1val	⊢ ( var1 ‘ 𝑆 ) = ( ( 1o mVar 𝑆 ) ‘ ∅ )
20		eqid	⊢ ( 1o mVar 𝑆 ) = ( 1o mVar 𝑆 )
21	20 15 6 3	subrgmvr	⊢ ( 𝜑 → ( 1o mVar 𝑆 ) = ( 1o mVar 𝑈 ) )
22	21	fveq1d	⊢ ( 𝜑 → ( ( 1o mVar 𝑆 ) ‘ ∅ ) = ( ( 1o mVar 𝑈 ) ‘ ∅ ) )
23	19 22	eqtrid	⊢ ( 𝜑 → ( var1 ‘ 𝑆 ) = ( ( 1o mVar 𝑈 ) ‘ ∅ ) )
24	23	fveq2d	⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( var1 ‘ 𝑆 ) ) = ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 1o mVar 𝑈 ) ‘ ∅ ) ) )
25	23	fveq2d	⊢ ( 𝜑 → ( ( 1o eval 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) = ( ( 1o eval 𝑆 ) ‘ ( ( 1o mVar 𝑈 ) ‘ ∅ ) ) )
26	18 24 25	3eqtr4d	⊢ ( 𝜑 → ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( var1 ‘ 𝑆 ) ) = ( ( 1o eval 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) )
27	26	coeq1d	⊢ ( 𝜑 → ( ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( var1 ‘ 𝑆 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( ( 1o eval 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
28		eqid	⊢ ( Poly1 ‘ 𝑈 ) = ( Poly1 ‘ 𝑈 )
29		eqid	⊢ ( Poly1 ‘ ( 𝑆 ↾s 𝑅 ) ) = ( Poly1 ‘ ( 𝑆 ↾s 𝑅 ) )
30	3	fveq2i	⊢ ( Poly1 ‘ 𝑈 ) = ( Poly1 ‘ ( 𝑆 ↾s 𝑅 ) )
31	30	fveq2i	⊢ ( Base ‘ ( Poly1 ‘ 𝑈 ) ) = ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝑅 ) ) )
32	29 31	ply1bas	⊢ ( Base ‘ ( Poly1 ‘ 𝑈 ) ) = ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) )
33	32	eqcomi	⊢ ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝑈 ) )
34	7 6 3 28 33	subrgvr1cl	⊢ ( 𝜑 → ( var1 ‘ 𝑆 ) ∈ ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
35		eqid	⊢ ( 1o evalSub 𝑆 ) = ( 1o evalSub 𝑆 )
36		eqid	⊢ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) = ( 1o mPoly ( 𝑆 ↾s 𝑅 ) )
37		eqid	⊢ ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) ) = ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) )
38	1 35 4 36 37	evls1val	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ ( var1 ‘ 𝑆 ) ∈ ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) → ( 𝑄 ‘ ( var1 ‘ 𝑆 ) ) = ( ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( var1 ‘ 𝑆 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
39	5 6 34 38	syl3anc	⊢ ( 𝜑 → ( 𝑄 ‘ ( var1 ‘ 𝑆 ) ) = ( ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( var1 ‘ 𝑆 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
40		crngring	⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
41		eqid	⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
42		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
43	41 42	ply1bas	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( 1o mPoly 𝑆 ) )
44	43	eqcomi	⊢ ( Base ‘ ( 1o mPoly 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
45	7 41 44	vr1cl	⊢ ( 𝑆 ∈ Ring → ( var1 ‘ 𝑆 ) ∈ ( Base ‘ ( 1o mPoly 𝑆 ) ) )
46	5 40 45	3syl	⊢ ( 𝜑 → ( var1 ‘ 𝑆 ) ∈ ( Base ‘ ( 1o mPoly 𝑆 ) ) )
47		eqid	⊢ ( eval1 ‘ 𝑆 ) = ( eval1 ‘ 𝑆 )
48		eqid	⊢ ( 1o mPoly 𝑆 ) = ( 1o mPoly 𝑆 )
49		eqid	⊢ ( Base ‘ ( 1o mPoly 𝑆 ) ) = ( Base ‘ ( 1o mPoly 𝑆 ) )
50	47 12 4 48 49	evl1val	⊢ ( ( 𝑆 ∈ CRing ∧ ( var1 ‘ 𝑆 ) ∈ ( Base ‘ ( 1o mPoly 𝑆 ) ) ) → ( ( eval1 ‘ 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) = ( ( ( 1o eval 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
51	5 46 50	syl2anc	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) = ( ( ( 1o eval 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
52	27 39 51	3eqtr4d	⊢ ( 𝜑 → ( 𝑄 ‘ ( var1 ‘ 𝑆 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) )
53	47 7 4	evl1var	⊢ ( 𝑆 ∈ CRing → ( ( eval1 ‘ 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) = ( I ↾ 𝐵 ) )
54	5 53	syl	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) = ( I ↾ 𝐵 ) )
55	10 52 54	3eqtrd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑋 ) = ( I ↾ 𝐵 ) )