Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lindeps Structured version   Visualization version   Unicode version
Definition df-lindeps 42233
Description: Define the relation between a module and its linearly dependent subsets. (Contributed by AV, 26-Apr-2019.)
Assertion
Ref Expression
df-lindeps |- linDepS = { <. s , m >. | -. s linIndS m }
Distinct variable group:   m, s
Detailed syntax breakdown of Definition df-lindeps
StepHypRef Expression
1 clindeps 42230 . 2 class linDepS
2 vs . . . . . 6 setvar s
32cv 1482 . . . . 5 class s
4 vm . . . . . 6 setvar m
54cv 1482 . . . . 5 class m
6 clininds 42229 . . . . 5 class linIndS
73, 5, 6wbr 4653 . . . 4 wff s linIndS m
87wn 3 . . 3 wff -. s linIndS m
98, 2, 4copab 4712 . 2 class { <. s , m >. | -. s linIndS m }
101, 9wceq 1483 1 wff linDepS = { <. s , m >. | -. s linIndS m }
Colors of variables: wff setvar class
This definition is referenced by:  lindepsnlininds  42241
  Copyright terms: Public domain W3C validator