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

Definition df-algind 19365
 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 = (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})
Distinct variable group:   𝑓,𝑘,𝑣,𝑤

Detailed syntax breakdown of Definition df-algind
StepHypRef Expression
1 cai 19361 . 2 class AlgInd
2 vw . . 3 setvar 𝑤
3 vk . . 3 setvar 𝑘
4 cvv 3173 . . 3 class V
52cv 1474 . . . . 5 class 𝑤
6 cbs 15695 . . . . 5 class Base
75, 6cfv 5804 . . . 4 class (Base‘𝑤)
87cpw 4108 . . 3 class 𝒫 (Base‘𝑤)
9 vf . . . . . . 7 setvar 𝑓
10 vv . . . . . . . . . 10 setvar 𝑣
1110cv 1474 . . . . . . . . 9 class 𝑣
123cv 1474 . . . . . . . . . 10 class 𝑘
13 cress 15696 . . . . . . . . . 10 class s
145, 12, 13co 6549 . . . . . . . . 9 class (𝑤s 𝑘)
15 cmpl 19174 . . . . . . . . 9 class mPoly
1611, 14, 15co 6549 . . . . . . . 8 class (𝑣 mPoly (𝑤s 𝑘))
1716, 6cfv 5804 . . . . . . 7 class (Base‘(𝑣 mPoly (𝑤s 𝑘)))
18 cid 4948 . . . . . . . . 9 class I
1918, 11cres 5040 . . . . . . . 8 class ( I ↾ 𝑣)
209cv 1474 . . . . . . . . 9 class 𝑓
21 ces 19325 . . . . . . . . . . 11 class evalSub
2211, 5, 21co 6549 . . . . . . . . . 10 class (𝑣 evalSub 𝑤)
2312, 22cfv 5804 . . . . . . . . 9 class ((𝑣 evalSub 𝑤)‘𝑘)
2420, 23cfv 5804 . . . . . . . 8 class (((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)
2519, 24cfv 5804 . . . . . . 7 class ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣))
269, 17, 25cmpt 4643 . . . . . 6 class (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
2726ccnv 5037 . . . . 5 class (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
2827wfun 5798 . . . 4 wff Fun (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
2928, 10, 8crab 2900 . . 3 class {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))}
302, 3, 4, 8, 29cmpt2 6551 . 2 class (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})
311, 30wceq 1475 1 wff AlgInd = (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator