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=ImVarR
mvrfval.d D=h0I|h-1Fin
mvrfval.z 0˙=0R
mvrfval.o 1˙=1R
mvrfval.i φIW
mvrfval.r φRY
mvrval.x φXI
Assertion mvrid φVXyIify=X10=1˙

Proof

Step Hyp Ref Expression
1 mvrfval.v V=ImVarR
2 mvrfval.d D=h0I|h-1Fin
3 mvrfval.z 0˙=0R
4 mvrfval.o 1˙=1R
5 mvrfval.i φIW
6 mvrfval.r φRY
7 mvrval.x φXI
8 1nn0 10
9 2 snifpsrbag IW10yIify=X10D
10 5 8 9 sylancl φyIify=X10D
11 1 2 3 4 5 6 7 10 mvrval2 φVXyIify=X10=ifyIify=X10=yIify=X101˙0˙
12 eqid yIify=X10=yIify=X10
13 12 iftruei ifyIify=X10=yIify=X101˙0˙=1˙
14 11 13 eqtrdi φVXyIify=X10=1˙