This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 ) ) )