Metamath Proof Explorer


Theorem mzpcompact2

Description: Polynomials are finitary objects and can only reference a finite number of variables, even if the index set is infinite. Thus, every polynomial can be expressed as a (uniquely minimal, although we do not prove that) polynomial on a finite number of variables, which is then extended by adding an arbitrary set of ignored variables. (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Assertion mzpcompact2 AmzPolyBaFinbmzPolyaaBA=cBbca

Proof

Step Hyp Ref Expression
1 elfvex AmzPolyBBV
2 fveq2 d=BmzPolyd=mzPolyB
3 2 eleq2d d=BAmzPolydAmzPolyB
4 sseq2 d=BadaB
5 oveq2 d=Bd=B
6 5 mpteq1d d=Bcdbca=cBbca
7 6 eqeq2d d=BA=cdbcaA=cBbca
8 4 7 anbi12d d=BadA=cdbcaaBA=cBbca
9 8 2rexbidv d=BaFinbmzPolyaadA=cdbcaaFinbmzPolyaaBA=cBbca
10 3 9 imbi12d d=BAmzPolydaFinbmzPolyaadA=cdbcaAmzPolyBaFinbmzPolyaaBA=cBbca
11 vex dV
12 11 mzpcompact2lem AmzPolydaFinbmzPolyaadA=cdbca
13 10 12 vtoclg BVAmzPolyBaFinbmzPolyaaBA=cBbca
14 1 13 mpcom AmzPolyBaFinbmzPolyaaBA=cBbca