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

Definition df-algind 20785
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 20781 . 2 class AlgInd
2 vw . . 3 setvar 𝑤
3 vk . . 3 setvar 𝑘
4 cvv 3469 . . 3 class V
52cv 1537 . . . . 5 class 𝑤
6 cbs 16474 . . . . 5 class Base
75, 6cfv 6334 . . . 4 class (Base‘𝑤)
87cpw 4511 . . 3 class 𝒫 (Base‘𝑤)
9 vf . . . . . . 7 setvar 𝑓
10 vv . . . . . . . . . 10 setvar 𝑣
1110cv 1537 . . . . . . . . 9 class 𝑣
123cv 1537 . . . . . . . . . 10 class 𝑘
13 cress 16475 . . . . . . . . . 10 class s
145, 12, 13co 7140 . . . . . . . . 9 class (𝑤s 𝑘)
15 cmpl 20589 . . . . . . . . 9 class mPoly
1611, 14, 15co 7140 . . . . . . . 8 class (𝑣 mPoly (𝑤s 𝑘))
1716, 6cfv 6334 . . . . . . 7 class (Base‘(𝑣 mPoly (𝑤s 𝑘)))
18 cid 5436 . . . . . . . . 9 class I
1918, 11cres 5534 . . . . . . . 8 class ( I ↾ 𝑣)
209cv 1537 . . . . . . . . 9 class 𝑓
21 ces 20741 . . . . . . . . . . 11 class evalSub
2211, 5, 21co 7140 . . . . . . . . . 10 class (𝑣 evalSub 𝑤)
2312, 22cfv 6334 . . . . . . . . 9 class ((𝑣 evalSub 𝑤)‘𝑘)
2420, 23cfv 6334 . . . . . . . 8 class (((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)
2519, 24cfv 6334 . . . . . . 7 class ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣))
269, 17, 25cmpt 5122 . . . . . 6 class (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
2726ccnv 5531 . . . . 5 class (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
2827wfun 6328 . . . 4 wff Fun (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
2928, 10, 8crab 3134 . . 3 class {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))}
302, 3, 4, 8, 29cmpo 7142 . 2 class (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})
311, 30wceq 1538 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