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 ˙