Metamath Proof Explorer

Definition df-algind

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)

Ref Expression
Assertion df-algind 
|- AlgInd = ( w e. _V , k e. ~P ( Base ` w ) |-> { v e. ~P ( Base ` w ) | Fun `' ( f e. ( Base ` ( v mPoly ( w |`s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cai 
 |-  AlgInd
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vk 
 |-  k
4 cbs 
 |-  Base
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( Base ` w )
7 6 cpw 
 |-  ~P ( Base ` w )
8 vv 
 |-  v
9 vf 
 |-  f
10 8 cv 
 |-  v
11 cmpl 
 |-  mPoly
12 cress 
 |-  |`s
13 3 cv 
 |-  k
14 5 13 12 co 
 |-  ( w |`s k )
15 10 14 11 co 
 |-  ( v mPoly ( w |`s k ) )
16 15 4 cfv 
 |-  ( Base ` ( v mPoly ( w |`s k ) ) )
17 ces 
 |-  evalSub
18 10 5 17 co 
 |-  ( v evalSub w )
19 13 18 cfv 
 |-  ( ( v evalSub w ) ` k )
20 9 cv 
 |-  f
21 20 19 cfv 
 |-  ( ( ( v evalSub w ) ` k ) ` f )
22 cid 
 |-  _I
23 22 10 cres 
 |-  ( _I |` v )
24 23 21 cfv 
 |-  ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) )
25 9 16 24 cmpt 
 |-  ( f e. ( Base ` ( v mPoly ( w |`s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) )
26 25 ccnv 
 |-  `' ( f e. ( Base ` ( v mPoly ( w |`s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) )
27 26 wfun 
 |-  Fun `' ( f e. ( Base ` ( v mPoly ( w |`s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) )
28 27 8 7 crab 
 |-  { v e. ~P ( Base ` w ) | Fun `' ( f e. ( Base ` ( v mPoly ( w |`s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) ) }
29 1 3 2 7 28 cmpo 
 |-  ( w e. _V , k e. ~P ( Base ` w ) |-> { v e. ~P ( Base ` w ) | Fun `' ( f e. ( Base ` ( v mPoly ( w |`s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) ) } )
30 0 29 wceq 
 |-  AlgInd = ( w e. _V , k e. ~P ( Base ` w ) |-> { v e. ~P ( Base ` w ) | Fun `' ( f e. ( Base ` ( v mPoly ( w |`s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) ) } )