Theorem evl1vard

Description: Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	evl1var.q	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	evl1var.v	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	evl1var.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evl1vard.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	evl1vard.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	evl1vard.1	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evl1vard.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	evl1vard	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑌 ) = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		evl1var.q	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2		evl1var.v	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		evl1var.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		evl1vard.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		evl1vard.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
6		evl1vard.1	⊢ ( 𝜑 → 𝑅 ∈ CRing )
7		evl1vard.2	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
9	2 4 5	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝑈 )
10	6 8 9	3syl	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
11	1 2 3	evl1var	⊢ ( 𝑅 ∈ CRing → ( 𝑂 ‘ 𝑋 ) = ( I ↾ 𝐵 ) )
12	6 11	syl	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ( I ↾ 𝐵 ) )
13	12	fveq1d	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑌 ) = ( ( I ↾ 𝐵 ) ‘ 𝑌 ) )
14		fvresi	⊢ ( 𝑌 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑌 ) = 𝑌 )
15	7 14	syl	⊢ ( 𝜑 → ( ( I ↾ 𝐵 ) ‘ 𝑌 ) = 𝑌 )
16	13 15	eqtrd	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑌 ) = 𝑌 )
17	10 16	jca	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑌 ) = 𝑌 ) )