Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mzpcl Unicode version

Definition df-mzpcl 26801
Description: Define the polynomially closed function rings over an arbitrary index set  v. The set  (mzPolyCld `  v
) contains all sets of functions from  ( ZZ  ^m  v
) to  ZZ which include all constants and projections and are closed under addition and multiplication. This is a "temporary" set used to define the polynomial function ring itself  (mzPoly `  v
); see df-mzp 26802. (Contributed by Stefan O'Rear, 4-Oct-2014.)
Assertion
Ref Expression
df-mzpcl  |- mzPolyCld  =  ( v  e.  _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  o F  +  g )  e.  p  /\  ( f  o F  x.  g )  e.  p ) ) } )
Distinct variable group:    f, g, i, j, p, v, x

Detailed syntax breakdown of Definition df-mzpcl
StepHypRef Expression
1 cmzpcl 26799 . 2  class mzPolyCld
2 vv . . 3  set  v
3 cvv 2788 . . 3  class  _V
4 cz 10024 . . . . . . . . . 10  class  ZZ
52cv 1622 . . . . . . . . . 10  class  v
6 cmap 6772 . . . . . . . . . 10  class  ^m
74, 5, 6co 5858 . . . . . . . . 9  class  ( ZZ 
^m  v )
8 vi . . . . . . . . . . 11  set  i
98cv 1622 . . . . . . . . . 10  class  i
109csn 3640 . . . . . . . . 9  class  { i }
117, 10cxp 4687 . . . . . . . 8  class  ( ( ZZ  ^m  v )  X.  { i } )
12 vp . . . . . . . . 9  set  p
1312cv 1622 . . . . . . . 8  class  p
1411, 13wcel 1684 . . . . . . 7  wff  ( ( ZZ  ^m  v )  X.  { i } )  e.  p
1514, 8, 4wral 2543 . . . . . 6  wff  A. i  e.  ZZ  ( ( ZZ 
^m  v )  X. 
{ i } )  e.  p
16 vx . . . . . . . . 9  set  x
17 vj . . . . . . . . . . 11  set  j
1817cv 1622 . . . . . . . . . 10  class  j
1916cv 1622 . . . . . . . . . 10  class  x
2018, 19cfv 5255 . . . . . . . . 9  class  ( x `
 j )
2116, 7, 20cmpt 4077 . . . . . . . 8  class  ( x  e.  ( ZZ  ^m  v )  |->  ( x `
 j ) )
2221, 13wcel 1684 . . . . . . 7  wff  ( x  e.  ( ZZ  ^m  v )  |->  ( x `
 j ) )  e.  p
2322, 17, 5wral 2543 . . . . . 6  wff  A. j  e.  v  ( x  e.  ( ZZ  ^m  v
)  |->  ( x `  j ) )  e.  p
2415, 23wa 358 . . . . 5  wff  ( 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 vf . . . . . . . . . . 11  set  f
2625cv 1622 . . . . . . . . . 10  class  f
27 vg . . . . . . . . . . 11  set  g
2827cv 1622 . . . . . . . . . 10  class  g
29 caddc 8740 . . . . . . . . . . 11  class  +
3029cof 6076 . . . . . . . . . 10  class  o F  +
3126, 28, 30co 5858 . . . . . . . . 9  class  ( f  o F  +  g )
3231, 13wcel 1684 . . . . . . . 8  wff  ( f  o F  +  g )  e.  p
33 cmul 8742 . . . . . . . . . . 11  class  x.
3433cof 6076 . . . . . . . . . 10  class  o F  x.
3526, 28, 34co 5858 . . . . . . . . 9  class  ( f  o F  x.  g
)
3635, 13wcel 1684 . . . . . . . 8  wff  ( f  o F  x.  g
)  e.  p
3732, 36wa 358 . . . . . . 7  wff  ( ( f  o F  +  g )  e.  p  /\  ( f  o F  x.  g )  e.  p )
3837, 27, 13wral 2543 . . . . . 6  wff  A. g  e.  p  ( (
f  o F  +  g )  e.  p  /\  ( f  o F  x.  g )  e.  p )
3938, 25, 13wral 2543 . . . . 5  wff  A. f  e.  p  A. g  e.  p  ( (
f  o F  +  g )  e.  p  /\  ( f  o F  x.  g )  e.  p )
4024, 39wa 358 . . . 4  wff  ( ( 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  o F  +  g )  e.  p  /\  ( f  o F  x.  g
)  e.  p ) )
414, 7, 6co 5858 . . . . 5  class  ( ZZ 
^m  ( ZZ  ^m  v ) )
4241cpw 3625 . . . 4  class  ~P ( ZZ  ^m  ( ZZ  ^m  v ) )
4340, 12, 42crab 2547 . . 3  class  { 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  o F  +  g )  e.  p  /\  ( f  o F  x.  g )  e.  p ) ) }
442, 3, 43cmpt 4077 . 2  class  ( v  e.  _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  o F  +  g )  e.  p  /\  ( f  o F  x.  g )  e.  p ) ) } )
451, 44wceq 1623 1  wff mzPolyCld  =  ( v  e.  _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  o F  +  g )  e.  p  /\  ( f  o F  x.  g )  e.  p ) ) } )
Colors of variables: wff set class
This definition is referenced by:  mzpclval  26803
  Copyright terms: Public domain W3C validator