Definition df-algind 21607

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 21603	. 2 class AlgInd
2		vw	. . 3 setvar 𝑤
3		vk	. . 3 setvar 𝑘
4		cvv 3473	. . 3 class V
5	2	cv 1540	. . . . 5 class 𝑤
6		cbs 17126	. . . . 5 class Base
7	5, 6	cfv 6532	. . . 4 class (Base‘𝑤)
8	7	cpw 4596	. . 3 class 𝒫 (Base‘𝑤)
9		vf	. . . . . . 7 setvar 𝑓
10		vv	. . . . . . . . . 10 setvar 𝑣
11	10	cv 1540	. . . . . . . . 9 class 𝑣
12	3	cv 1540	. . . . . . . . . 10 class 𝑘
13		cress 17155	. . . . . . . . . 10 class ↾s
14	5, 12, 13	co 7393	. . . . . . . . 9 class (𝑤 ↾s 𝑘)
15		cmpl 21390	. . . . . . . . 9 class mPoly
16	11, 14, 15	co 7393	. . . . . . . 8 class (𝑣 mPoly (𝑤 ↾s 𝑘))
17	16, 6	cfv 6532	. . . . . . 7 class (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘)))
18		cid 5566	. . . . . . . . 9 class I
19	18, 11	cres 5671	. . . . . . . 8 class ( I ↾ 𝑣)
20	9	cv 1540	. . . . . . . . 9 class 𝑓
21		ces 21562	. . . . . . . . . . 11 class evalSub
22	11, 5, 21	co 7393	. . . . . . . . . 10 class (𝑣 evalSub 𝑤)
23	12, 22	cfv 6532	. . . . . . . . 9 class ((𝑣 evalSub 𝑤)‘𝑘)
24	20, 23	cfv 6532	. . . . . . . 8 class (((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)
25	19, 24	cfv 6532	. . . . . . 7 class ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣))
26	9, 17, 25	cmpt 5224	. . . . . 6 class (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
27	26	ccnv 5668	. . . . 5 class ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
28	27	wfun 6526	. . . 4 wff Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
29	28, 10, 8	crab 3431	. . 3 class {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))}
30	2, 3, 4, 8, 29	cmpo 7395	. 2 class (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})
31	1, 30	wceq 1541	1 wff AlgInd = (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})

This definition is referenced by: (None)