Definition df-lindf

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 , 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 ) and only one representation for each element of the range ( islindf5 ). (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Assertion	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 } ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clindf	|- LIndF
1		vf	|- f
2		vw	|- w
3	1	cv	|- f
4	3	cdm	|- dom f
5		cbs	|- Base
6	2	cv	|- w
7	6 5	cfv	|- ( Base ` w )
8	4 7 3	wf	|- f : dom f --> ( Base ` w )
9		csca	|- Scalar
10	6 9	cfv	|- ( Scalar ` w )
11		vs	|- s
12		vx	|- x
13		vk	|- k
14	11	cv	|- s
15	14 5	cfv	|- ( Base ` s )
16		c0g	|- 0g
17	14 16	cfv	|- ( 0g ` s )
18	17	csn	|- { ( 0g ` s ) }
19	15 18	cdif	|- ( ( Base ` s ) \ { ( 0g ` s ) } )
20	13	cv	|- k
21		cvsca	|- .s
22	6 21	cfv	|- ( .s ` w )
23	12	cv	|- x
24	23 3	cfv	|- ( f ` x )
25	20 24 22	co	|- ( k ( .s ` w ) ( f ` x ) )
26		clspn	|- LSpan
27	6 26	cfv	|- ( LSpan ` w )
28	23	csn	|- { x }
29	4 28	cdif	|- ( dom f \ { x } )
30	3 29	cima	|- ( f " ( dom f \ { x } ) )
31	30 27	cfv	|- ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) )
32	25 31	wcel	|- ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) )
33	32	wn	|- -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) )
34	33 13 19	wral	|- A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) )
35	34 12 4	wral	|- A. x e. dom f A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) )
36	35 11 10	wsbc	|- [. ( 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 } ) ) )
37	8 36	wa	|- ( 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 } ) ) ) )
38	37 1 2	copab	|- { <. 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 } ) ) ) ) }
39	0 38	wceq	|- 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 } ) ) ) ) }