Theorem ply1val

Description: The value of the set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	ply1val.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1val.2	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
Assertion	ply1val	⊢ 𝑃 = ( 𝑆 ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1val.2	⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
3		fveq2	⊢ ( 𝑟 = 𝑅 → ( PwSer1 ‘ 𝑟 ) = ( PwSer1 ‘ 𝑅 ) )
4	3 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( PwSer1 ‘ 𝑟 ) = 𝑆 )
5		oveq2	⊢ ( 𝑟 = 𝑅 → ( 1o mPoly 𝑟 ) = ( 1o mPoly 𝑅 ) )
6	5	fveq2d	⊢ ( 𝑟 = 𝑅 → ( Base ‘ ( 1o mPoly 𝑟 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) ) )
7	4 6	oveq12d	⊢ ( 𝑟 = 𝑅 → ( ( PwSer1 ‘ 𝑟 ) ↾s ( Base ‘ ( 1o mPoly 𝑟 ) ) ) = ( 𝑆 ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) ) )
8		df-ply1	⊢ Poly1 = ( 𝑟 ∈ V ↦ ( ( PwSer1 ‘ 𝑟 ) ↾s ( Base ‘ ( 1o mPoly 𝑟 ) ) ) )
9		ovex	⊢ ( 𝑆 ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) ) ∈ V
10	7 8 9	fvmpt	⊢ ( 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ( 𝑆 ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) ) )
11		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ∅ )
12		ress0	⊢ ( ∅ ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) ) = ∅
13	11 12	eqtr4di	⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ( ∅ ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) ) )
14		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( PwSer1 ‘ 𝑅 ) = ∅ )
15	2 14	eqtrid	⊢ ( ¬ 𝑅 ∈ V → 𝑆 = ∅ )
16	15	oveq1d	⊢ ( ¬ 𝑅 ∈ V → ( 𝑆 ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) ) = ( ∅ ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) ) )
17	13 16	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ( 𝑆 ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) ) )
18	10 17	pm2.61i	⊢ ( Poly1 ‘ 𝑅 ) = ( 𝑆 ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
19	1 18	eqtri	⊢ 𝑃 = ( 𝑆 ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )