Definition df-algind

Description: Define the predicate "the set v is algebraically independent in the algebra w ". 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)

	Ref	Expression
Assertion	df-algind	⊢ AlgInd = ( 𝑤 ∈ V , 𝑘 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ { 𝑣 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ Fun ◡ ( 𝑓 ∈ ( Base ‘ ( 𝑣 mPoly ( 𝑤 ↾s 𝑘 ) ) ) ↦ ( ( ( ( 𝑣 evalSub 𝑤 ) ‘ 𝑘 ) ‘ 𝑓 ) ‘ ( I ↾ 𝑣 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cai	⊢ AlgInd
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vk	⊢ 𝑘
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7	6	cpw	⊢ 𝒫 ( Base ‘ 𝑤 )
8		vv	⊢ 𝑣
9		vf	⊢ 𝑓
10	8	cv	⊢ 𝑣
11		cmpl	⊢ mPoly
12		cress	⊢ ↾s
13	3	cv	⊢ 𝑘
14	5 13 12	co	⊢ ( 𝑤 ↾s 𝑘 )
15	10 14 11	co	⊢ ( 𝑣 mPoly ( 𝑤 ↾s 𝑘 ) )
16	15 4	cfv	⊢ ( Base ‘ ( 𝑣 mPoly ( 𝑤 ↾s 𝑘 ) ) )
17		ces	⊢ evalSub
18	10 5 17	co	⊢ ( 𝑣 evalSub 𝑤 )
19	13 18	cfv	⊢ ( ( 𝑣 evalSub 𝑤 ) ‘ 𝑘 )
20	9	cv	⊢ 𝑓
21	20 19	cfv	⊢ ( ( ( 𝑣 evalSub 𝑤 ) ‘ 𝑘 ) ‘ 𝑓 )
22		cid	⊢ I
23	22 10	cres	⊢ ( I ↾ 𝑣 )
24	23 21	cfv	⊢ ( ( ( ( 𝑣 evalSub 𝑤 ) ‘ 𝑘 ) ‘ 𝑓 ) ‘ ( I ↾ 𝑣 ) )
25	9 16 24	cmpt	⊢ ( 𝑓 ∈ ( Base ‘ ( 𝑣 mPoly ( 𝑤 ↾s 𝑘 ) ) ) ↦ ( ( ( ( 𝑣 evalSub 𝑤 ) ‘ 𝑘 ) ‘ 𝑓 ) ‘ ( I ↾ 𝑣 ) ) )
26	25	ccnv	⊢ ◡ ( 𝑓 ∈ ( Base ‘ ( 𝑣 mPoly ( 𝑤 ↾s 𝑘 ) ) ) ↦ ( ( ( ( 𝑣 evalSub 𝑤 ) ‘ 𝑘 ) ‘ 𝑓 ) ‘ ( I ↾ 𝑣 ) ) )
27	26	wfun	⊢ Fun ◡ ( 𝑓 ∈ ( Base ‘ ( 𝑣 mPoly ( 𝑤 ↾s 𝑘 ) ) ) ↦ ( ( ( ( 𝑣 evalSub 𝑤 ) ‘ 𝑘 ) ‘ 𝑓 ) ‘ ( I ↾ 𝑣 ) ) )
28	27 8 7	crab	⊢ { 𝑣 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ Fun ◡ ( 𝑓 ∈ ( Base ‘ ( 𝑣 mPoly ( 𝑤 ↾s 𝑘 ) ) ) ↦ ( ( ( ( 𝑣 evalSub 𝑤 ) ‘ 𝑘 ) ‘ 𝑓 ) ‘ ( I ↾ 𝑣 ) ) ) }
29	1 3 2 7 28	cmpo	⊢ ( 𝑤 ∈ V , 𝑘 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ { 𝑣 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ Fun ◡ ( 𝑓 ∈ ( Base ‘ ( 𝑣 mPoly ( 𝑤 ↾s 𝑘 ) ) ) ↦ ( ( ( ( 𝑣 evalSub 𝑤 ) ‘ 𝑘 ) ‘ 𝑓 ) ‘ ( I ↾ 𝑣 ) ) ) } )
30	0 29	wceq	⊢ AlgInd = ( 𝑤 ∈ V , 𝑘 ∈ 𝒫 ( Base ‘ 𝑤 ) ↦ { 𝑣 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ Fun ◡ ( 𝑓 ∈ ( Base ‘ ( 𝑣 mPoly ( 𝑤 ↾s 𝑘 ) ) ) ↦ ( ( ( ( 𝑣 evalSub 𝑤 ) ‘ 𝑘 ) ‘ 𝑓 ) ‘ ( I ↾ 𝑣 ) ) ) } )