Theorem evlvar

Description: Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019)

	Ref	Expression
Hypotheses	evlvar.q	⊢ 𝑄 = ( 𝐼 eval 𝑆 )
	evlvar.v	⊢ 𝑉 = ( 𝐼 mVar 𝑆 )
	evlvar.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evlvar.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	evlvar.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlvar.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion	evlvar	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlvar.q	⊢ 𝑄 = ( 𝐼 eval 𝑆 )
2		evlvar.v	⊢ 𝑉 = ( 𝐼 mVar 𝑆 )
3		evlvar.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		evlvar.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		evlvar.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
6		evlvar.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
7		eqid	⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
8		eqid	⊢ ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) )
9		eqid	⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
10		crngring	⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
11	3	subrgid	⊢ ( 𝑆 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
12	5 10 11	3syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
13	7 1 8 9 3 4 5 12 6	evlsvarsrng	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑄 ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) )
14	7 8 9 3 4 5 12 6	evlsvar	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
15	2 4 12 9	subrgmvr	⊢ ( 𝜑 → 𝑉 = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) )
16	15	fveq1d	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) = ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) )
17	16	eqcomd	⊢ ( 𝜑 → ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) = ( 𝑉 ‘ 𝑋 ) )
18	17	fveq2d	⊢ ( 𝜑 → ( 𝑄 ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) )
19	13 14 18	3eqtr3rd	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )