Metamath Proof Explorer

Theorem elmzpcl

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

Ref Expression
Assertion elmzpcl 
|- ( V e. _V -> ( P e. ( mzPolyCld ` V ) <-> ( P C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mzpclval 
 |-  ( V e. _V -> ( mzPolyCld ` V ) = { p e. ~P ( ZZ ^m ( ZZ ^m V ) ) | ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } )
2 1 eleq2d 
 |-  ( V e. _V -> ( P e. ( mzPolyCld ` V ) <-> P e. { p e. ~P ( ZZ ^m ( ZZ ^m V ) ) | ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } ) )
3 eleq2 
 |-  ( p = P -> ( ( ( ZZ ^m V ) X. { i } ) e. p <-> ( ( ZZ ^m V ) X. { i } ) e. P ) )
4 3 ralbidv 
 |-  ( p = P -> ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p <-> A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P ) )
5 eleq2 
 |-  ( p = P -> ( ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p <-> ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) )
6 5 ralbidv 
 |-  ( p = P -> ( A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p <-> A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) )
7 4 6 anbi12d 
 |-  ( p = P -> ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p ) <-> ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) ) )
8 eleq2 
 |-  ( p = P -> ( ( f oF + g ) e. p <-> ( f oF + g ) e. P ) )
9 eleq2 
 |-  ( p = P -> ( ( f oF x. g ) e. p <-> ( f oF x. g ) e. P ) )
10 8 9 anbi12d 
 |-  ( p = P -> ( ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) <-> ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) )
11 10 raleqbi1dv 
 |-  ( p = P -> ( A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) <-> A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) )
12 11 raleqbi1dv 
 |-  ( p = P -> ( A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) <-> A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) )
13 7 12 anbi12d 
 |-  ( p = P -> ( ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) <-> ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) )
14 13 elrab 
 |-  ( P e. { p e. ~P ( ZZ ^m ( ZZ ^m V ) ) | ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } <-> ( P e. ~P ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) )
15 ovex 
 |-  ( ZZ ^m ( ZZ ^m V ) ) e. _V
16 15 elpw2 
 |-  ( P e. ~P ( ZZ ^m ( ZZ ^m V ) ) <-> P C_ ( ZZ ^m ( ZZ ^m V ) ) )
17 16 anbi1i 
 |-  ( ( P e. ~P ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) <-> ( P C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) )
18 14 17 bitri 
 |-  ( P e. { p e. ~P ( ZZ ^m ( ZZ ^m V ) ) | ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } <-> ( P C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) )
19 2 18 bitrdi 
 |-  ( V e. _V -> ( P e. ( mzPolyCld ` V ) <-> ( P C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) ) )