Definition df-lindf 18648

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 18668, 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 18680) and only one representation for each element of the range (islindf5 18681). (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 18646	. 2 class LIndF
2		vf	. . . . . . 7 setvar f
3	2	cv 1378	. . . . . 6 class f
4	3	cdm 4999	. . . . 5 class dom f
5		vw	. . . . . . 7 setvar w
6	5	cv 1378	. . . . . 6 class w
7		cbs 14493	. . . . . 6 class Base
8	6, 7	cfv 5588	. . . . 5 class ( Base ` w )
9	4, 8, 3	wf 5584	. . . 4 wff f : dom f --> ( Base ` w )
10		vk	. . . . . . . . . . 11 setvar k
11	10	cv 1378	. . . . . . . . . 10 class k
12		vx	. . . . . . . . . . . 12 setvar x
13	12	cv 1378	. . . . . . . . . . 11 class x
14	13, 3	cfv 5588	. . . . . . . . . 10 class ( f ` x )
15		cvsca 14562	. . . . . . . . . . 11 class .s
16	6, 15	cfv 5588	. . . . . . . . . 10 class ( .s ` w )
17	11, 14, 16	co 6285	. . . . . . . . 9 class ( k ( .s ` w ) ( f ` x ) )
18	13	csn 4027	. . . . . . . . . . . 12 class { x }
19	4, 18	cdif 3473	. . . . . . . . . . 11 class ( dom f \ { x } )
20	3, 19	cima 5002	. . . . . . . . . 10 class ( f " ( dom f \ { x } ) )
21		clspn 17429	. . . . . . . . . . 11 class LSpan
22	6, 21	cfv 5588	. . . . . . . . . 10 class ( LSpan ` w )
23	20, 22	cfv 5588	. . . . . . . . 9 class ( ( LSpan ` w ) ` ( f " ( dom f \ { x } ) ) )
24	17, 23	wcel 1767	. . . . . . . 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 1378	. . . . . . . . 9 class s
28	27, 7	cfv 5588	. . . . . . . 8 class ( Base ` s )
29		c0g 14698	. . . . . . . . . 10 class 0g
30	27, 29	cfv 5588	. . . . . . . . 9 class ( 0g ` s )
31	30	csn 4027	. . . . . . . 8 class { ( 0g ` s ) }
32	28, 31	cdif 3473	. . . . . . 7 class ( ( Base ` s ) \ { ( 0g ` s ) } )
33	25, 10, 32	wral 2814	. . . . . 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 2814	. . . . 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 14561	. . . . . 6 class Scalar
36	6, 35	cfv 5588	. . . . 5 class (Scalar ` w )
37	34, 26, 36	wsbc 3331	. . . 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 369	. . 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 4504	. 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 1379	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  18650  islindf  18654