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

Definition df-algind 16108
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 16097 . 2  class AlgInd
2 vw . . 3  set  w
3 vk . . 3  set  k
4 cvv 2788 . . 3  class  _V
52cv 1622 . . . . 5  class  w
6 cbs 13148 . . . . 5  class  Base
75, 6cfv 5255 . . . 4  class  ( Base `  w )
87cpw 3625 . . 3  class  ~P ( Base `  w )
9 vf . . . . . . 7  set  f
10 vv . . . . . . . . . 10  set  v
1110cv 1622 . . . . . . . . 9  class  v
123cv 1622 . . . . . . . . . 10  class  k
13 cress 13149 . . . . . . . . . 10  classs
145, 12, 13co 5858 . . . . . . . . 9  class  ( ws  k )
15 cmpl 16089 . . . . . . . . 9  class mPoly
1611, 14, 15co 5858 . . . . . . . 8  class  ( v mPoly 
( ws  k ) )
1716, 6cfv 5255 . . . . . . 7  class  ( Base `  ( v mPoly  ( ws  k ) ) )
18 cid 4304 . . . . . . . . 9  class  _I
1918, 11cres 4691 . . . . . . . 8  class  (  _I  |`  v )
209cv 1622 . . . . . . . . 9  class  f
21 ces 16090 . . . . . . . . . . 11  class evalSub
2211, 5, 21co 5858 . . . . . . . . . 10  class  ( v evalSub  w )
2312, 22cfv 5255 . . . . . . . . 9  class  ( ( v evalSub  w ) `  k )
2420, 23cfv 5255 . . . . . . . 8  class  ( ( ( v evalSub  w ) `
 k ) `  f )
2519, 24cfv 5255 . . . . . . 7  class  ( ( ( ( v evalSub  w
) `  k ) `  f ) `  (  _I  |`  v ) )
269, 17, 25cmpt 4077 . . . . . 6  class  ( f  e.  ( Base `  (
v mPoly  ( ws  k ) ) )  |->  ( ( ( ( v evalSub  w
) `  k ) `  f ) `  (  _I  |`  v ) ) )
2726ccnv 4688 . . . . 5  class  `' ( f  e.  ( Base `  ( v mPoly  ( ws  k ) ) )  |->  ( ( ( ( v evalSub  w ) `  k
) `  f ) `  (  _I  |`  v
) ) )
2827wfun 5249 . . . 4  wff  Fun  `' ( f  e.  (
Base `  ( v mPoly  ( ws  k ) ) )  |->  ( ( ( ( v evalSub  w ) `
 k ) `  f ) `  (  _I  |`  v ) ) )
2928, 10, 8crab 2547 . . 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 5860 . 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 1623 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