Definition df-algind 21325

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

Step	Hyp	Ref	Expression
1		cai 21321	. 2 class AlgInd
2		vw	. . 3 setvar 𝑤
3		vk	. . 3 setvar 𝑘
4		cvv 3432	. . 3 class V
5	2	cv 1538	. . . . 5 class 𝑤
6		cbs 16912	. . . . 5 class Base
7	5, 6	cfv 6433	. . . 4 class (Base‘𝑤)
8	7	cpw 4533	. . 3 class 𝒫 (Base‘𝑤)
9		vf	. . . . . . 7 setvar 𝑓
10		vv	. . . . . . . . . 10 setvar 𝑣
11	10	cv 1538	. . . . . . . . 9 class 𝑣
12	3	cv 1538	. . . . . . . . . 10 class 𝑘
13		cress 16941	. . . . . . . . . 10 class ↾s
14	5, 12, 13	co 7275	. . . . . . . . 9 class (𝑤 ↾s 𝑘)
15		cmpl 21109	. . . . . . . . 9 class mPoly
16	11, 14, 15	co 7275	. . . . . . . 8 class (𝑣 mPoly (𝑤 ↾s 𝑘))
17	16, 6	cfv 6433	. . . . . . 7 class (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘)))
18		cid 5488	. . . . . . . . 9 class I
19	18, 11	cres 5591	. . . . . . . 8 class ( I ↾ 𝑣)
20	9	cv 1538	. . . . . . . . 9 class 𝑓
21		ces 21280	. . . . . . . . . . 11 class evalSub
22	11, 5, 21	co 7275	. . . . . . . . . 10 class (𝑣 evalSub 𝑤)
23	12, 22	cfv 6433	. . . . . . . . 9 class ((𝑣 evalSub 𝑤)‘𝑘)
24	20, 23	cfv 6433	. . . . . . . 8 class (((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)
25	19, 24	cfv 6433	. . . . . . 7 class ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣))
26	9, 17, 25	cmpt 5157	. . . . . 6 class (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
27	26	ccnv 5588	. . . . 5 class ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
28	27	wfun 6427	. . . 4 wff Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
29	28, 10, 8	crab 3068	. . 3 class {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))}
30	2, 3, 4, 8, 29	cmpo 7277	. 2 class (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})
31	1, 30	wceq 1539	1 wff AlgInd = (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})

This definition is referenced by: (None)