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

Metamath Proof Explorer

Theorem mvrid

Description: The X i -th coefficient of the term X i is 1 . (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses mvrfval.v ⊢ V = I mVar R
mvrfval.d ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
mvrfval.z ⊢ 0 ˙ = 0 R
mvrfval.o ⊢ 1 ˙ = 1 R
mvrfval.i ⊢ φ → I ∈ W
mvrfval.r ⊢ φ → R ∈ Y
mvrval.x ⊢ φ → X ∈ I
Assertion mvrid ⊢ φ → V ⁡ X ⁡ y ∈ I ⟼ if y = X 1 0 = 1 ˙

Proof

Step Hyp Ref Expression
1 mvrfval.v ⊢ V = I mVar R
2 mvrfval.d ⊢ D = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
3 mvrfval.z ⊢ 0 ˙ = 0 R
4 mvrfval.o ⊢ 1 ˙ = 1 R
5 mvrfval.i ⊢ φ → I ∈ W
6 mvrfval.r ⊢ φ → R ∈ Y
7 mvrval.x ⊢ φ → X ∈ I
8 1nn0 ⊢ 1 ∈ ℕ 0
9 2 snifpsrbag ⊢ I ∈ W ∧ 1 ∈ ℕ 0 → y ∈ I ⟼ if y = X 1 0 ∈ D
10 5 8 9 sylancl ⊢ φ → y ∈ I ⟼ if y = X 1 0 ∈ D
11 1 2 3 4 5 6 7 10 mvrval2 ⊢ φ → V ⁡ X ⁡ y ∈ I ⟼ if y = X 1 0 = if y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = X 1 0 1 ˙ 0 ˙
12 eqid ⊢ y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = X 1 0
13 12 iftruei ⊢ if y ∈ I ⟼ if y = X 1 0 = y ∈ I ⟼ if y = X 1 0 1 ˙ 0 ˙ = 1 ˙
14 11 13 eqtrdi ⊢ φ → V ⁡ X ⁡ y ∈ I ⟼ if y = X 1 0 = 1 ˙