Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lindf Unicode version

Definition df-lindf 26424
Description: An independent family is a family of vectors, no nonzero multiple of which can be expressed as a linear combination of other elements of the family. This is almost, but not quite, the same as a function into an independent set.

This is a defined concept because it matters in many cases whether independence is taken at a set or family level. For instance, a number is transcedental iff its nonzero powers are linearly independent. Is 1 transcedental? It has only one nonzero power.

We can almost define family independence as a family of unequal elements with independent range, as islindf3 26444, but taking that as primitive would lead to unpleasant corner case behavior with the zero ring.

This is equivalent to the common definition of having no nontrivial representations of zero (islindf4 26456) and only one representation for each element of the range (islindf5 26457). (Contributed by Stefan O'Rear, 24-Feb-2015.)

Assertion
Ref Expression
df-lindf  |- LIndF  =  { <. f ,  w >.  |  ( f : dom  f
--> ( Base `  w
)  /\  [. (Scalar `  w )  /  s ]. A. x  e.  dom  f A. k  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( k ( .s `  w
) ( f `  x ) )  e.  ( ( LSpan `  w
) `  ( f " ( dom  f  \  { x } ) ) ) ) }
Distinct variable group:    w, f, s, x, k

Detailed syntax breakdown of Definition df-lindf
StepHypRef Expression
1 clindf 26422 . 2  class LIndF
2 vf . . . . . . 7  set  f
32cv 1632 . . . . . 6  class  f
43cdm 4726 . . . . 5  class  dom  f
5 vw . . . . . . 7  set  w
65cv 1632 . . . . . 6  class  w
7 cbs 13195 . . . . . 6  class  Base
86, 7cfv 5292 . . . . 5  class  ( Base `  w )
94, 8, 3wf 5288 . . . 4  wff  f : dom  f --> ( Base `  w )
10 vk . . . . . . . . . . 11  set  k
1110cv 1632 . . . . . . . . . 10  class  k
12 vx . . . . . . . . . . . 12  set  x
1312cv 1632 . . . . . . . . . . 11  class  x
1413, 3cfv 5292 . . . . . . . . . 10  class  ( f `
 x )
15 cvsca 13259 . . . . . . . . . . 11  class  .s
166, 15cfv 5292 . . . . . . . . . 10  class  ( .s
`  w )
1711, 14, 16co 5900 . . . . . . . . 9  class  ( k ( .s `  w
) ( f `  x ) )
1813csn 3674 . . . . . . . . . . . 12  class  { x }
194, 18cdif 3183 . . . . . . . . . . 11  class  ( dom  f  \  { x } )
203, 19cima 4729 . . . . . . . . . 10  class  ( f
" ( dom  f  \  { x } ) )
21 clspn 15777 . . . . . . . . . . 11  class  LSpan
226, 21cfv 5292 . . . . . . . . . 10  class  ( LSpan `  w )
2320, 22cfv 5292 . . . . . . . . 9  class  ( (
LSpan `  w ) `  ( f " ( dom  f  \  { x } ) ) )
2417, 23wcel 1701 . . . . . . . 8  wff  ( k ( .s `  w
) ( f `  x ) )  e.  ( ( LSpan `  w
) `  ( f " ( dom  f  \  { x } ) ) )
2524wn 3 . . . . . . 7  wff  -.  (
k ( .s `  w ) ( f `
 x ) )  e.  ( ( LSpan `  w ) `  (
f " ( dom  f  \  { x } ) ) )
26 vs . . . . . . . . . 10  set  s
2726cv 1632 . . . . . . . . 9  class  s
2827, 7cfv 5292 . . . . . . . 8  class  ( Base `  s )
29 c0g 13449 . . . . . . . . . 10  class  0g
3027, 29cfv 5292 . . . . . . . . 9  class  ( 0g
`  s )
3130csn 3674 . . . . . . . 8  class  { ( 0g `  s ) }
3228, 31cdif 3183 . . . . . . 7  class  ( (
Base `  s )  \  { ( 0g `  s ) } )
3325, 10, 32wral 2577 . . . . . 6  wff  A. k  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( k ( .s `  w
) ( f `  x ) )  e.  ( ( LSpan `  w
) `  ( f " ( dom  f  \  { x } ) ) )
3433, 12, 4wral 2577 . . . . 5  wff  A. x  e.  dom  f A. k  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( k ( .s `  w
) ( f `  x ) )  e.  ( ( LSpan `  w
) `  ( f " ( dom  f  \  { x } ) ) )
35 csca 13258 . . . . . 6  class Scalar
366, 35cfv 5292 . . . . 5  class  (Scalar `  w )
3734, 26, 36wsbc 3025 . . . 4  wff  [. (Scalar `  w )  /  s ]. A. x  e.  dom  f A. k  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( k ( .s `  w
) ( f `  x ) )  e.  ( ( LSpan `  w
) `  ( f " ( dom  f  \  { x } ) ) )
389, 37wa 358 . . 3  wff  ( f : dom  f --> (
Base `  w )  /\  [. (Scalar `  w
)  /  s ]. A. x  e.  dom  f A. k  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( k ( .s `  w
) ( f `  x ) )  e.  ( ( LSpan `  w
) `  ( f " ( dom  f  \  { x } ) ) ) )
3938, 2, 5copab 4113 . 2  class  { <. f ,  w >.  |  ( f : dom  f --> ( Base `  w )  /\  [. (Scalar `  w
)  /  s ]. A. x  e.  dom  f A. k  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( k ( .s `  w
) ( f `  x ) )  e.  ( ( LSpan `  w
) `  ( f " ( dom  f  \  { x } ) ) ) ) }
401, 39wceq 1633 1  wff LIndF  =  { <. f ,  w >.  |  ( f : dom  f
--> ( Base `  w
)  /\  [. (Scalar `  w )  /  s ]. A. x  e.  dom  f A. k  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( k ( .s `  w
) ( f `  x ) )  e.  ( ( LSpan `  w
) `  ( f " ( dom  f  \  { x } ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  rellindf  26426  islindf  26430
  Copyright terms: Public domain W3C validator