Metamath Proof Explorer


Theorem elmzpcl

Description: Double substitution lemma for mzPolyCld . (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion elmzpcl V V P mzPolyCld V P V i V × i P j V x V x j P f P g P f + f g P f × f g P

Proof

Step Hyp Ref Expression
1 mzpclval V V mzPolyCld V = p 𝒫 V | i V × i p j V x V x j p f p g p f + f g p f × f g p
2 1 eleq2d V V P mzPolyCld V P p 𝒫 V | i V × i p j V x V x j p f p g p f + f g p f × f g p
3 eleq2 p = P V × i p V × i P
4 3 ralbidv p = P i V × i p i V × i P
5 eleq2 p = P x V x j p x V x j P
6 5 ralbidv p = P j V x V x j p j V x V x j P
7 4 6 anbi12d p = P i V × i p j V x V x j p i V × i P j V x V x j P
8 eleq2 p = P f + f g p f + f g P
9 eleq2 p = P f × f g p f × f g P
10 8 9 anbi12d p = P f + f g p f × f g p f + f g P f × f g P
11 10 raleqbi1dv p = P g p f + f g p f × f g p g P f + f g P f × f g P
12 11 raleqbi1dv p = P f p g p f + f g p f × f g p f P g P f + f g P f × f g P
13 7 12 anbi12d p = P i V × i p j V x V x j p f p g p f + f g p f × f g p i V × i P j V x V x j P f P g P f + f g P f × f g P
14 13 elrab P p 𝒫 V | i V × i p j V x V x j p f p g p f + f g p f × f g p P 𝒫 V i V × i P j V x V x j P f P g P f + f g P f × f g P
15 ovex V V
16 15 elpw2 P 𝒫 V P V
17 16 anbi1i P 𝒫 V i V × i P j V x V x j P f P g P f + f g P f × f g P P V i V × i P j V x V x j P f P g P f + f g P f × f g P
18 14 17 bitri P p 𝒫 V | i V × i p j V x V x j p f p g p f + f g p f × f g p P V i V × i P j V x V x j P f P g P f + f g P f × f g P
19 2 18 bitrdi V V P mzPolyCld V P V i V × i P j V x V x j P f P g P f + f g P f × f g P