Definition df-lindf 19008

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 19028, 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 19040) and only one representation for each element of the range (islindf5 19041). (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

Step	Hyp	Ref	Expression
1		clindf 19006	. 2 class LIndF
2		vf	. . . . . . 7 setvar f
3	2	cv 1397	. . . . . 6 class f
4	3	cdm 4988	. . . . 5 class dom f
5		vw	. . . . . . 7 setvar w
6	5	cv 1397	. . . . . 6 class w
7		cbs 14716	. . . . . 6 class Base
8	6, 7	cfv 5570	. . . . 5 class ( Base ` w )
9	4, 8, 3	wf 5566	. . . 4 wff f : dom f --> ( Base ` w )
10		vk	. . . . . . . . . . 11 setvar k
11	10	cv 1397	. . . . . . . . . 10 class k
12		vx	. . . . . . . . . . . 12 setvar x
13	12	cv 1397	. . . . . . . . . . 11 class x
14	13, 3	cfv 5570	. . . . . . . . . 10 class ( f ` x )
15		cvsca 14788	. . . . . . . . . . 11 class .s
16	6, 15	cfv 5570	. . . . . . . . . 10 class ( .s ` w )
17	11, 14, 16	co 6270	. . . . . . . . 9 class ( k ( .s ` w ) ( f ` x ) )
18	13	csn 4016	. . . . . . . . . . . 12 class { x }
19	4, 18	cdif 3458	. . . . . . . . . . 11 class ( dom f \ { x } )
20	3, 19	cima 4991	. . . . . . . . . 10 class ( f " ( dom f \ { x } ) )
21		clspn 17812	. . . . . . . . . . 11 class LSpan
22	6, 21	cfv 5570	. . . . . . . . . 10 class ( LSpan ` w )
23	20, 22	cfv 5570	. . . . . . . . 9 class ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) )
24	17, 23	wcel 1823	. . . . . . . 8 wff ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) )
25	24	wn 3	. . . . . . 7 wff -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) )
26		vs	. . . . . . . . . 10 setvar s
27	26	cv 1397	. . . . . . . . 9 class s
28	27, 7	cfv 5570	. . . . . . . 8 class ( Base ` s )
29		c0g 14929	. . . . . . . . . 10 class 0g
30	27, 29	cfv 5570	. . . . . . . . 9 class ( 0g ` s )
31	30	csn 4016	. . . . . . . 8 class { ( 0g ` s ) }
32	28, 31	cdif 3458	. . . . . . 7 class ( ( Base ` s ) \ { ( 0g ` s ) } )
33	25, 10, 32	wral 2804	. . . . . 6 wff A. k e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( k ( .s ` w ) ( f ` x ) ) e. ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) )
34	33, 12, 4	wral 2804	. . . . 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 14787	. . . . . 6 class Scalar
36	6, 35	cfv 5570	. . . . 5 class (Scalar ` w )
37	34, 26, 36	wsbc 3324	. . . 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 } ) ) )
38	9, 37	wa 367	. . 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 } ) ) ) )
39	38, 2, 5	copab 4496	. 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 } ) ) ) ) }
40	1, 39	wceq 1398	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 } ) ) ) ) }

This definition is referenced by:  rellindf  19010  islindf  19014