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	syl5eq	⊢ ( 𝜑 → ( 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		eqid	⊢ ( PwSer1 ‘ ( 𝑆 ↾s 𝑅 ) ) = ( PwSer1 ‘ ( 𝑆 ↾s 𝑅 ) )
31	3	fveq2i	⊢ ( Poly1 ‘ 𝑈 ) = ( Poly1 ‘ ( 𝑆 ↾s 𝑅 ) )
32	31	fveq2i	⊢ ( Base ‘ ( Poly1 ‘ 𝑈 ) ) = ( Base ‘ ( Poly1 ‘ ( 𝑆 ↾s 𝑅 ) ) )
33	29 30 32	ply1bas	⊢ ( Base ‘ ( Poly1 ‘ 𝑈 ) ) = ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) )
34	33	eqcomi	⊢ ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝑈 ) )
35	7 6 3 28 34	subrgvr1cl	⊢ ( 𝜑 → ( var1 ‘ 𝑆 ) ∈ ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
36		eqid	⊢ ( 1o evalSub 𝑆 ) = ( 1o evalSub 𝑆 )
37		eqid	⊢ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) = ( 1o mPoly ( 𝑆 ↾s 𝑅 ) )
38		eqid	⊢ ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) ) = ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) )
39	1 36 4 37 38	evls1val	⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ∧ ( var1 ‘ 𝑆 ) ∈ ( Base ‘ ( 1o mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) → ( 𝑄 ‘ ( var1 ‘ 𝑆 ) ) = ( ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( var1 ‘ 𝑆 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
40	5 6 35 39	syl3anc	⊢ ( 𝜑 → ( 𝑄 ‘ ( var1 ‘ 𝑆 ) ) = ( ( ( ( 1o evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( var1 ‘ 𝑆 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
41		crngring	⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
42		eqid	⊢ ( Poly1 ‘ 𝑆 ) = ( Poly1 ‘ 𝑆 )
43		eqid	⊢ ( PwSer1 ‘ 𝑆 ) = ( PwSer1 ‘ 𝑆 )
44		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
45	42 43 44	ply1bas	⊢ ( Base ‘ ( Poly1 ‘ 𝑆 ) ) = ( Base ‘ ( 1o mPoly 𝑆 ) )
46	45	eqcomi	⊢ ( Base ‘ ( 1o mPoly 𝑆 ) ) = ( Base ‘ ( Poly1 ‘ 𝑆 ) )
47	7 42 46	vr1cl	⊢ ( 𝑆 ∈ Ring → ( var1 ‘ 𝑆 ) ∈ ( Base ‘ ( 1o mPoly 𝑆 ) ) )
48	5 41 47	3syl	⊢ ( 𝜑 → ( var1 ‘ 𝑆 ) ∈ ( Base ‘ ( 1o mPoly 𝑆 ) ) )
49		eqid	⊢ ( eval1 ‘ 𝑆 ) = ( eval1 ‘ 𝑆 )
50		eqid	⊢ ( 1o mPoly 𝑆 ) = ( 1o mPoly 𝑆 )
51		eqid	⊢ ( Base ‘ ( 1o mPoly 𝑆 ) ) = ( Base ‘ ( 1o mPoly 𝑆 ) )
52	49 12 4 50 51	evl1val	⊢ ( ( 𝑆 ∈ CRing ∧ ( var1 ‘ 𝑆 ) ∈ ( Base ‘ ( 1o mPoly 𝑆 ) ) ) → ( ( eval1 ‘ 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) = ( ( ( 1o eval 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
53	5 48 52	syl2anc	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) = ( ( ( 1o eval 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
54	27 40 53	3eqtr4d	⊢ ( 𝜑 → ( 𝑄 ‘ ( var1 ‘ 𝑆 ) ) = ( ( eval1 ‘ 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) )
55	49 7 4	evl1var	⊢ ( 𝑆 ∈ CRing → ( ( eval1 ‘ 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) = ( I ↾ 𝐵 ) )
56	5 55	syl	⊢ ( 𝜑 → ( ( eval1 ‘ 𝑆 ) ‘ ( var1 ‘ 𝑆 ) ) = ( I ↾ 𝐵 ) )
57	10 54 56	3eqtrd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑋 ) = ( I ↾ 𝐵 ) )