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∈V,k∈𝒫Basew⟼v∈𝒫Basew|Fun⁡f∈BasevmPolyw↾𝑠k⟼vevalSubw⁡k⁡f⁡I↾v-1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cai classAlgInd
1 vw setvarw
2 cvv classV
3 vk setvark
4 cbs classBase
5 1 cv setvarw
6 5 4 cfv classBasew
7 6 cpw class𝒫Basew
8 vv setvarv
9 vf setvarf
10 8 cv setvarv
11 cmpl classmPoly
12 cress class↾𝑠
13 3 cv setvark
14 5 13 12 co classw↾𝑠k
15 10 14 11 co classvmPolyw↾𝑠k
16 15 4 cfv classBasevmPolyw↾𝑠k
17 ces classevalSub
18 10 5 17 co classvevalSubw
19 13 18 cfv classvevalSubw⁡k
20 9 cv setvarf
21 20 19 cfv classvevalSubw⁡k⁡f
22 cid classI
23 22 10 cres classI↾v
24 23 21 cfv classvevalSubw⁡k⁡f⁡I↾v
25 9 16 24 cmpt classf∈BasevmPolyw↾𝑠k⟼vevalSubw⁡k⁡f⁡I↾v
26 25 ccnv classf∈BasevmPolyw↾𝑠k⟼vevalSubw⁡k⁡f⁡I↾v-1
27 26 wfun wffFun⁡f∈BasevmPolyw↾𝑠k⟼vevalSubw⁡k⁡f⁡I↾v-1
28 27 8 7 crab classv∈𝒫Basew|Fun⁡f∈BasevmPolyw↾𝑠k⟼vevalSubw⁡k⁡f⁡I↾v-1
29 1 3 2 7 28 cmpo classw∈V,k∈𝒫Basew⟼v∈𝒫Basew|Fun⁡f∈BasevmPolyw↾𝑠k⟼vevalSubw⁡k⁡f⁡I↾v-1
30 0 29 wceq wffAlgInd=w∈V,k∈𝒫Basew⟼v∈𝒫Basew|Fun⁡f∈BasevmPolyw↾𝑠k⟼vevalSubw⁡k⁡f⁡I↾v-1