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 ∈ 𝒫 Base w ⟼ v ∈ 𝒫 Base w | Fun ⁡ f ∈ Base v mPoly w ↾ 𝑠 k ⟼ v evalSub w ⁡ k ⁡ f ⁡ I ↾ v -1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cai class AlgInd
1 vw setvar w
2 cvv class V
3 vk setvar k
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 6 cpw class 𝒫 Base w
8 vv setvar v
9 vf setvar f
10 8 cv setvar v
11 cmpl class mPoly
12 cress class ↾ 𝑠
13 3 cv setvar k
14 5 13 12 co class w ↾ 𝑠 k
15 10 14 11 co class v mPoly w ↾ 𝑠 k
16 15 4 cfv class Base v mPoly w ↾ 𝑠 k
17 ces class evalSub
18 10 5 17 co class v evalSub w
19 13 18 cfv class v evalSub w ⁡ k
20 9 cv setvar f
21 20 19 cfv class v evalSub w ⁡ k ⁡ f
22 cid class I
23 22 10 cres class I ↾ v
24 23 21 cfv class v evalSub w ⁡ k ⁡ f ⁡ I ↾ v
25 9 16 24 cmpt class f ∈ Base v mPoly w ↾ 𝑠 k ⟼ v evalSub w ⁡ k ⁡ f ⁡ I ↾ v
26 25 ccnv class f ∈ Base v mPoly w ↾ 𝑠 k ⟼ v evalSub w ⁡ k ⁡ f ⁡ I ↾ v -1
27 26 wfun wff Fun ⁡ f ∈ Base v mPoly w ↾ 𝑠 k ⟼ v evalSub w ⁡ k ⁡ f ⁡ I ↾ v -1
28 27 8 7 crab class v ∈ 𝒫 Base w | Fun ⁡ f ∈ Base v mPoly w ↾ 𝑠 k ⟼ v evalSub w ⁡ k ⁡ f ⁡ I ↾ v -1
29 1 3 2 7 28 cmpo class w ∈ V , k ∈ 𝒫 Base w ⟼ v ∈ 𝒫 Base w | Fun ⁡ f ∈ Base v mPoly w ↾ 𝑠 k ⟼ v evalSub w ⁡ k ⁡ f ⁡ I ↾ v -1
30 0 29 wceq wff AlgInd = w ∈ V , k ∈ 𝒫 Base w ⟼ v ∈ 𝒫 Base w | Fun ⁡ f ∈ Base v mPoly w ↾ 𝑠 k ⟼ v evalSub w ⁡ k ⁡ f ⁡ I ↾ v -1