Metamath Proof Explorer


Theorem mvrval2

Description: Value of the generating elements of the power series structure. (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
mvrval2.f φFD
Assertion mvrval2 φVXF=ifF=yIify=X101˙0˙

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 mvrval2.f φFD
9 1 2 3 4 5 6 7 mvrval φVX=fDiff=yIify=X101˙0˙
10 9 fveq1d φVXF=fDiff=yIify=X101˙0˙F
11 eqeq1 f=Ff=yIify=X10F=yIify=X10
12 11 ifbid f=Fiff=yIify=X101˙0˙=ifF=yIify=X101˙0˙
13 eqid fDiff=yIify=X101˙0˙=fDiff=yIify=X101˙0˙
14 4 fvexi 1˙V
15 3 fvexi 0˙V
16 14 15 ifex ifF=yIify=X101˙0˙V
17 12 13 16 fvmpt FDfDiff=yIify=X101˙0˙F=ifF=yIify=X101˙0˙
18 8 17 syl φfDiff=yIify=X101˙0˙F=ifF=yIify=X101˙0˙
19 10 18 eqtrd φVXF=ifF=yIify=X101˙0˙