Theorem evl1scad

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

	Ref	Expression
Hypotheses	evl1sca.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
	evl1sca.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	evl1sca.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evl1sca.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	evl1scad.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	evl1scad.1	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evl1scad.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	evl1scad.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	evl1scad	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑋 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝑌 ) = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		evl1sca.o	⊢ 𝑂 = ( eval1 ‘ 𝑅 )
2		evl1sca.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		evl1sca.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		evl1sca.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
5		evl1scad.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
6		evl1scad.1	⊢ ( 𝜑 → 𝑅 ∈ CRing )
7		evl1scad.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		evl1scad.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10	2 4 3 5	ply1sclf	⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐵 ⟶ 𝑈 )
11	6 9 10	3syl	⊢ ( 𝜑 → 𝐴 : 𝐵 ⟶ 𝑈 )
12	11 7	ffvelcdmd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ 𝑈 )
13	1 2 3 4	evl1sca	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )
14	6 7 13	syl2anc	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 × { 𝑋 } ) )
15	14	fveq1d	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝑌 ) = ( ( 𝐵 × { 𝑋 } ) ‘ 𝑌 ) )
16		fvconst2g	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐵 × { 𝑋 } ) ‘ 𝑌 ) = 𝑋 )
17	7 8 16	syl2anc	⊢ ( 𝜑 → ( ( 𝐵 × { 𝑋 } ) ‘ 𝑌 ) = 𝑋 )
18	15 17	eqtrd	⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝑌 ) = 𝑋 )
19	12 18	jca	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑋 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝑌 ) = 𝑋 ) )