This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↾ 𝑣 ) ) ) } )