MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-algind Structured version   Unicode version

Definition df-algind 16429
Description: Define the predicate "the set  v is algebraically independent in the algebra  w". A collection of vectors is algebraically independent if no nontrivial polynomial with elements from the subset evaluates to zero. (Contributed by Mario Carneiro, 21-Mar-2015.)
Assertion
Ref Expression
df-algind  |- AlgInd  =  ( w  e.  _V , 
k  e.  ~P ( Base `  w )  |->  { v  e.  ~P ( Base `  w )  |  Fun  `' ( f  e.  ( Base `  (
v mPoly  ( ws  k ) ) )  |->  ( ( ( ( v evalSub  w
) `  k ) `  f ) `  (  _I  |`  v ) ) ) } )
Distinct variable group:    f, k, v, w

Detailed syntax breakdown of Definition df-algind
StepHypRef Expression
1 cai 16418 . 2  class AlgInd
2 vw . . 3  set  w
3 vk . . 3  set  k
4 cvv 2958 . . 3  class  _V
52cv 1652 . . . . 5  class  w
6 cbs 13471 . . . . 5  class  Base
75, 6cfv 5456 . . . 4  class  ( Base `  w )
87cpw 3801 . . 3  class  ~P ( Base `  w )
9 vf . . . . . . 7  set  f
10 vv . . . . . . . . . 10  set  v
1110cv 1652 . . . . . . . . 9  class  v
123cv 1652 . . . . . . . . . 10  class  k
13 cress 13472 . . . . . . . . . 10  classs
145, 12, 13co 6083 . . . . . . . . 9  class  ( ws  k )
15 cmpl 16410 . . . . . . . . 9  class mPoly
1611, 14, 15co 6083 . . . . . . . 8  class  ( v mPoly 
( ws  k ) )
1716, 6cfv 5456 . . . . . . 7  class  ( Base `  ( v mPoly  ( ws  k ) ) )
18 cid 4495 . . . . . . . . 9  class  _I
1918, 11cres 4882 . . . . . . . 8  class  (  _I  |`  v )
209cv 1652 . . . . . . . . 9  class  f
21 ces 16411 . . . . . . . . . . 11  class evalSub
2211, 5, 21co 6083 . . . . . . . . . 10  class  ( v evalSub  w )
2312, 22cfv 5456 . . . . . . . . 9  class  ( ( v evalSub  w ) `  k )
2420, 23cfv 5456 . . . . . . . 8  class  ( ( ( v evalSub  w ) `
 k ) `  f )
2519, 24cfv 5456 . . . . . . 7  class  ( ( ( ( v evalSub  w
) `  k ) `  f ) `  (  _I  |`  v ) )
269, 17, 25cmpt 4268 . . . . . 6  class  ( f  e.  ( Base `  (
v mPoly  ( ws  k ) ) )  |->  ( ( ( ( v evalSub  w
) `  k ) `  f ) `  (  _I  |`  v ) ) )
2726ccnv 4879 . . . . 5  class  `' ( f  e.  ( Base `  ( v mPoly  ( ws  k ) ) )  |->  ( ( ( ( v evalSub  w ) `  k
) `  f ) `  (  _I  |`  v
) ) )
2827wfun 5450 . . . 4  wff  Fun  `' ( f  e.  (
Base `  ( v mPoly  ( ws  k ) ) )  |->  ( ( ( ( v evalSub  w ) `
 k ) `  f ) `  (  _I  |`  v ) ) )
2928, 10, 8crab 2711 . . 3  class  { v  e.  ~P ( Base `  w )  |  Fun  `' ( f  e.  (
Base `  ( v mPoly  ( ws  k ) ) )  |->  ( ( ( ( v evalSub  w ) `
 k ) `  f ) `  (  _I  |`  v ) ) ) }
302, 3, 4, 8, 29cmpt2 6085 . 2  class  ( w  e.  _V ,  k  e.  ~P ( Base `  w )  |->  { v  e.  ~P ( Base `  w )  |  Fun  `' ( f  e.  (
Base `  ( v mPoly  ( ws  k ) ) )  |->  ( ( ( ( v evalSub  w ) `
 k ) `  f ) `  (  _I  |`  v ) ) ) } )
311, 30wceq 1653 1  wff AlgInd  =  ( w  e.  _V , 
k  e.  ~P ( Base `  w )  |->  { v  e.  ~P ( Base `  w )  |  Fun  `' ( f  e.  ( Base `  (
v mPoly  ( ws  k ) ) )  |->  ( ( ( ( v evalSub  w
) `  k ) `  f ) `  (  _I  |`  v ) ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator