Metamath Proof Explorer

Theorem mzpclval

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

Ref Expression
Assertion 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 ) ) } )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( v = V -> ( ZZ ^m v ) = ( ZZ ^m V ) )
2 1 oveq2d 
 |-  ( v = V -> ( ZZ ^m ( ZZ ^m v ) ) = ( ZZ ^m ( ZZ ^m V ) ) )
3 2 pweqd 
 |-  ( v = V -> ~P ( ZZ ^m ( ZZ ^m v ) ) = ~P ( ZZ ^m ( ZZ ^m V ) ) )
4 1 xpeq1d 
 |-  ( v = V -> ( ( ZZ ^m v ) X. { a } ) = ( ( ZZ ^m V ) X. { a } ) )
5 4 eleq1d 
 |-  ( v = V -> ( ( ( ZZ ^m v ) X. { a } ) e. p <-> ( ( ZZ ^m V ) X. { a } ) e. p ) )
6 5 ralbidv 
 |-  ( v = V -> ( A. a e. ZZ ( ( ZZ ^m v ) X. { a } ) e. p <-> A. a e. ZZ ( ( ZZ ^m V ) X. { a } ) e. p ) )
7 sneq 
 |-  ( a = i -> { a } = { i } )
8 7 xpeq2d 
 |-  ( a = i -> ( ( ZZ ^m V ) X. { a } ) = ( ( ZZ ^m V ) X. { i } ) )
9 8 eleq1d 
 |-  ( a = i -> ( ( ( ZZ ^m V ) X. { a } ) e. p <-> ( ( ZZ ^m V ) X. { i } ) e. p ) )
10 9 cbvralvw 
 |-  ( A. a e. ZZ ( ( ZZ ^m V ) X. { a } ) e. p <-> A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p )
11 6 10 bitrdi 
 |-  ( v = V -> ( A. a e. ZZ ( ( ZZ ^m v ) X. { a } ) e. p <-> A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p ) )
12 1 mpteq1d 
 |-  ( v = V -> ( c e. ( ZZ ^m v ) |-> ( c ` b ) ) = ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) )
13 12 eleq1d 
 |-  ( v = V -> ( ( c e. ( ZZ ^m v ) |-> ( c ` b ) ) e. p <-> ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) e. p ) )
14 13 raleqbi1dv 
 |-  ( v = V -> ( A. b e. v ( c e. ( ZZ ^m v ) |-> ( c ` b ) ) e. p <-> A. b e. V ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) e. p ) )
15 fveq2 
 |-  ( b = j -> ( c ` b ) = ( c ` j ) )
16 15 mpteq2dv 
 |-  ( b = j -> ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) = ( c e. ( ZZ ^m V ) |-> ( c ` j ) ) )
17 16 eleq1d 
 |-  ( b = j -> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) e. p <-> ( c e. ( ZZ ^m V ) |-> ( c ` j ) ) e. p ) )
18 fveq1 
 |-  ( c = x -> ( c ` j ) = ( x ` j ) )
19 18 cbvmptv 
 |-  ( c e. ( ZZ ^m V ) |-> ( c ` j ) ) = ( x e. ( ZZ ^m V ) |-> ( x ` j ) )
20 19 eleq1i 
 |-  ( ( c e. ( ZZ ^m V ) |-> ( c ` j ) ) e. p <-> ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p )
21 17 20 bitrdi 
 |-  ( b = j -> ( ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) e. p <-> ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p ) )
22 21 cbvralvw 
 |-  ( A. b e. V ( c e. ( ZZ ^m V ) |-> ( c ` b ) ) e. p <-> A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p )
23 14 22 bitrdi 
 |-  ( v = V -> ( A. b e. v ( c e. ( ZZ ^m v ) |-> ( c ` b ) ) e. p <-> A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p ) )
24 11 23 anbi12d 
 |-  ( v = V -> ( ( A. a e. ZZ ( ( ZZ ^m v ) X. { a } ) e. p /\ A. b e. v ( c e. ( ZZ ^m v ) |-> ( c ` b ) ) 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 ) ) )
25 24 anbi1d 
 |-  ( v = V -> ( ( ( A. a e. ZZ ( ( ZZ ^m v ) X. { a } ) e. p /\ A. b e. v ( c e. ( ZZ ^m v ) |-> ( c ` b ) ) 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 ) ) ) )
26 3 25 rabeqbidv 
 |-  ( v = V -> { p e. ~P ( ZZ ^m ( ZZ ^m v ) ) | ( ( A. a e. ZZ ( ( ZZ ^m v ) X. { a } ) e. p /\ A. b e. v ( c e. ( ZZ ^m v ) |-> ( c ` b ) ) 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 ) ) } )
27 df-mzpcl 
 |-  mzPolyCld = ( v e. _V |-> { p e. ~P ( ZZ ^m ( ZZ ^m v ) ) | ( ( A. a e. ZZ ( ( ZZ ^m v ) X. { a } ) e. p /\ A. b e. v ( c e. ( ZZ ^m v ) |-> ( c ` b ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } )
28 ovex 
 |-  ( ZZ ^m ( ZZ ^m V ) ) e. _V
29 28 pwex 
 |-  ~P ( ZZ ^m ( ZZ ^m V ) ) e. _V
30 29 rabex 
 |-  { 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 ) ) } e. _V
31 26 27 30 fvmpt 
 |-  ( 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 ) ) } )