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 ⊢ X = var 1 ⁡ R
Assertion vr1val ⊢ X = 1 𝑜 mVar R ⁡ ∅

Proof

Step Hyp Ref Expression
1 vr1val.1 ⊢ X = var 1 ⁡ R
2 oveq2 ⊢ r = R → 1 𝑜 mVar r = 1 𝑜 mVar R
3 2 fveq1d ⊢ r = R → 1 𝑜 mVar r ⁡ ∅ = 1 𝑜 mVar R ⁡ ∅
4 df-vr1 ⊢ var 1 = r ∈ V ⟼ 1 𝑜 mVar r ⁡ ∅
5 fvex ⊢ 1 𝑜 mVar R ⁡ ∅ ∈ V
6 3 4 5 fvmpt ⊢ R ∈ V → var 1 ⁡ R = 1 𝑜 mVar R ⁡ ∅
7 1 6 eqtrid ⊢ R ∈ V → X = 1 𝑜 mVar R ⁡ ∅
8 fvprc ⊢ ¬ R ∈ V → var 1 ⁡ R = ∅
9 0fv ⊢ ∅ ⁡ ∅ = ∅
10 8 1 9 3eqtr4g ⊢ ¬ R ∈ V → X = ∅ ⁡ ∅
11 df-mvr ⊢ mVar = i ∈ V , r ∈ V ⟼ x ∈ i ⟼ f ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ if f = y ∈ i ⟼ if y = x 1 0 1 r 0 r
12 11 reldmmpo ⊢ Rel ⁡ dom ⁡ mVar
13 12 ovprc2 ⊢ ¬ R ∈ V → 1 𝑜 mVar R = ∅
14 13 fveq1d ⊢ ¬ R ∈ V → 1 𝑜 mVar R ⁡ ∅ = ∅ ⁡ ∅
15 10 14 eqtr4d ⊢ ¬ R ∈ V → X = 1 𝑜 mVar R ⁡ ∅
16 7 15 pm2.61i ⊢ X = 1 𝑜 mVar R ⁡ ∅