Definition df-algind 22497

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 22461	. 2 class AlgInd
2		vw	. . 3 setvar 𝑤
3		vk	. . 3 setvar 𝑘
4		cvv 3450	. . 3 class V
5	2	cv 1568	. . . . 5 class 𝑤
6		cbs 17392	. . . . 5 class Base
7	5, 6	cfv 6538	. . . 4 class (Base‘𝑤)
8	7	cpw 4556	. . 3 class 𝒫 (Base‘𝑤)
9		vf	. . . . . . 7 setvar 𝑓
10		vv	. . . . . . . . . 10 setvar 𝑣
11	10	cv 1568	. . . . . . . . 9 class 𝑣
12	3	cv 1568	. . . . . . . . . 10 class 𝑘
13		cress 17413	. . . . . . . . . 10 class ↾s
14	5, 12, 13	co 7420	. . . . . . . . 9 class (𝑤 ↾s 𝑘)
15		cmpl 22219	. . . . . . . . 9 class mPoly
16	11, 14, 15	co 7420	. . . . . . . 8 class (𝑣 mPoly (𝑤 ↾s 𝑘))
17	16, 6	cfv 6538	. . . . . . 7 class (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘)))
18		cid 5544	. . . . . . . . 9 class I
19	18, 11	cres 5652	. . . . . . . 8 class ( I ↾ 𝑣)
20	9	cv 1568	. . . . . . . . 9 class 𝑓
21		ces 22386	. . . . . . . . . . 11 class evalSub
22	11, 5, 21	co 7420	. . . . . . . . . 10 class (𝑣 evalSub 𝑤)
23	12, 22	cfv 6538	. . . . . . . . 9 class ((𝑣 evalSub 𝑤)‘𝑘)
24	20, 23	cfv 6538	. . . . . . . 8 class (((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)
25	19, 24	cfv 6538	. . . . . . 7 class ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣))
26	9, 17, 25	cmpt 5185	. . . . . 6 class (𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
27	26	ccnv 5649	. . . . 5 class ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
28	27	wfun 6532	. . . 4 wff Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))
29	28, 10, 8	crab 3412	. . 3 class {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))}
30	2, 3, 4, 8, 29	cmpo 7422	. 2 class (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})
31	1, 30	wceq 1569	1 wff AlgInd = (𝑤 ∈ V, 𝑘 ∈ 𝒫 (Base‘𝑤) ↦ {𝑣 ∈ 𝒫 (Base‘𝑤) ∣ Fun ◡(𝑓 ∈ (Base‘(𝑣 mPoly (𝑤 ↾s 𝑘))) ↦ ((((𝑣 evalSub 𝑤)‘𝑘)‘𝑓)‘( I ↾ 𝑣)))})

This definition is used by: (None)