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

Definition df-algind 18535
 Description: Define the predicate "the set is algebraically independent in the algebra ". 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 mPoly s evalSub
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-algind
StepHypRef Expression
1 cai 18531 . 2 AlgInd
2 vw . . 3
3 vk . . 3
4 cvv 3061 . . 3
52cv 1406 . . . . 5
6 cbs 14843 . . . . 5
75, 6cfv 5571 . . . 4
87cpw 3957 . . 3
9 vf . . . . . . 7
10 vv . . . . . . . . . 10
1110cv 1406 . . . . . . . . 9
123cv 1406 . . . . . . . . . 10
13 cress 14844 . . . . . . . . . 10 s
145, 12, 13co 6280 . . . . . . . . 9 s
15 cmpl 18324 . . . . . . . . 9 mPoly
1611, 14, 15co 6280 . . . . . . . 8 mPoly s
1716, 6cfv 5571 . . . . . . 7 mPoly s
18 cid 4735 . . . . . . . . 9
1918, 11cres 4827 . . . . . . . 8
209cv 1406 . . . . . . . . 9
21 ces 18491 . . . . . . . . . . 11 evalSub
2211, 5, 21co 6280 . . . . . . . . . 10 evalSub
2312, 22cfv 5571 . . . . . . . . 9 evalSub
2420, 23cfv 5571 . . . . . . . 8 evalSub
2519, 24cfv 5571 . . . . . . 7 evalSub
269, 17, 25cmpt 4455 . . . . . 6 mPoly s evalSub
2726ccnv 4824 . . . . 5 mPoly s evalSub
2827wfun 5565 . . . 4 mPoly s evalSub
2928, 10, 8crab 2760 . . 3 mPoly s evalSub
302, 3, 4, 8, 29cmpt2 6282 . 2 mPoly s evalSub
311, 30wceq 1407 1 AlgInd mPoly s evalSub
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator