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

Metamath Proof Explorer

Theorem vr1val

Description: The value of the generator of the power series algebra (the X in R [ [ X ] ] ). Since all univariate polynomial rings over a fixed base ring R are isomorphic, we don't bother to pass this in as a parameter; internally we are actually using the empty set as this generator and 1o = { (/) } is the index set (but for most purposes this choice should not be visible anyway). (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypothesis vr1val.1 ⊢ 𝑋 = ( var1 ‘ 𝑅 )
Assertion vr1val 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )

Proof

Step Hyp Ref Expression
1 vr1val.1 ⊢ 𝑋 = ( var1 ‘ 𝑅 )
2 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 1o mVar 𝑟 ) = ( 1o mVar 𝑅 ) )
3 2 fveq1d ⊢ ( 𝑟 = 𝑅 → ( ( 1o mVar 𝑟 ) ‘ ∅ ) = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
4 df-vr1 ⊢ var1 = ( 𝑟 ∈ V ↦ ( ( 1o mVar 𝑟 ) ‘ ∅ ) )
5 fvex ⊢ ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ V
6 3 4 5 fvmpt ⊢ ( 𝑅 ∈ V → ( var1 ‘ 𝑅 ) = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
7 1 6 eqtrid ⊢ ( 𝑅 ∈ V → 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
8 fvprc ⊢ ( ¬ 𝑅 ∈ V → ( var1 ‘ 𝑅 ) = ∅ )
9 0fv ⊢ ( ∅ ‘ ∅ ) = ∅
10 8 1 9 3eqtr4g ⊢ ( ¬ 𝑅 ∈ V → 𝑋 = ( ∅ ‘ ∅ ) )
11 df-mvr ⊢ mVar = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )
12 11 reldmmpo ⊢ Rel dom mVar
13 12 ovprc2 ⊢ ( ¬ 𝑅 ∈ V → ( 1o mVar 𝑅 ) = ∅ )
14 13 fveq1d ⊢ ( ¬ 𝑅 ∈ V → ( ( 1o mVar 𝑅 ) ‘ ∅ ) = ( ∅ ‘ ∅ ) )
15 10 14 eqtr4d ⊢ ( ¬ 𝑅 ∈ V → 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
16 7 15 pm2.61i ⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )