Metamath Proof Explorer

Definition df-lindeps

Description: Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019)

Ref Expression
Assertion df-lindeps 
|- linDepS = { <. s , m >. | -. s linIndS m }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clindeps 
 |-  linDepS
1 vs 
 |-  s
2 vm 
 |-  m
3 1 cv 
 |-  s
4 clininds 
 |-  linIndS
5 2 cv 
 |-  m
6 3 5 4 wbr 
 |-  s linIndS m
7 6 wn 
 |-  -. s linIndS m
8 7 1 2 copab 
 |-  { <. s , m >. | -. s linIndS m }
9 0 8 wceq 
 |-  linDepS = { <. s , m >. | -. s linIndS m }