Definition df-algind 19544

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 ( w ↾s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) ) } )

Distinct variable group:   f, k, v, w

Detailed syntax breakdown of Definition df-algind

Step	Hyp	Ref	Expression
1		cai 19540	. 2 class AlgInd
2		vw	. . 3 setvar w
3		vk	. . 3 setvar k
4		cvv 3200	. . 3 class _V
5	2	cv 1482	. . . . 5 class w
6		cbs 15857	. . . . 5 class Base
7	5, 6	cfv 5888	. . . 4 class ( Base ` w )
8	7	cpw 4158	. . 3 class ~P ( Base ` w )
9		vf	. . . . . . 7 setvar f
10		vv	. . . . . . . . . 10 setvar v
11	10	cv 1482	. . . . . . . . 9 class v
12	3	cv 1482	. . . . . . . . . 10 class k
13		cress 15858	. . . . . . . . . 10 class ↾s
14	5, 12, 13	co 6650	. . . . . . . . 9 class ( w ↾s k )
15		cmpl 19353	. . . . . . . . 9 class mPoly
16	11, 14, 15	co 6650	. . . . . . . 8 class ( v mPoly ( w ↾s k ) )
17	16, 6	cfv 5888	. . . . . . 7 class ( Base ` ( v mPoly ( w ↾s k ) ) )
18		cid 5023	. . . . . . . . 9 class _I
19	18, 11	cres 5116	. . . . . . . 8 class ( _I |` v )
20	9	cv 1482	. . . . . . . . 9 class f
21		ces 19504	. . . . . . . . . . 11 class evalSub
22	11, 5, 21	co 6650	. . . . . . . . . 10 class ( v evalSub w )
23	12, 22	cfv 5888	. . . . . . . . 9 class ( ( v evalSub w ) ` k )
24	20, 23	cfv 5888	. . . . . . . 8 class ( ( ( v evalSub w ) ` k ) ` f )
25	19, 24	cfv 5888	. . . . . . 7 class ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) )
26	9, 17, 25	cmpt 4729	. . . . . 6 class ( f e. ( Base ` ( v mPoly ( w ↾s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) )
27	26	ccnv 5113	. . . . 5 class `' ( f e. ( Base ` ( v mPoly ( w ↾s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) )
28	27	wfun 5882	. . . 4 wff Fun `' ( f e. ( Base ` ( v mPoly ( w ↾s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) )
29	28, 10, 8	crab 2916	. . 3 class { v e. ~P ( Base ` w ) | Fun `' ( f e. ( Base ` ( v mPoly ( w ↾s k ) ) ) |-> ( ( ( ( v evalSub w ) ` k ) ` f ) ` ( _I |` v ) ) ) }
30	2, 3, 4, 8, 29	cmpt2 6652	. 2 class ( 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 ) ) ) } )
31	1, 30	wceq 1483	1 wff 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 ) ) ) } )

This definition is referenced by: (None)