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	$$⊢\mathrm{LIndF}=\left\{⟨f,w⟩|\left(f:\mathrm{dom}f⟶{\mathrm{Base}}_w\wedge \underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clindf	$$class\mathrm{LIndF}$$
1		vf	$$setvarf$$
2		vw	$$setvarw$$
3	1	cv	$$setvarf$$
4	3	cdm	$$class\mathrm{dom}f$$
5		cbs	$$class\mathrm{Base}$$
6	2	cv	$$setvarw$$
7	6 5	cfv	$$class{\mathrm{Base}}_w$$
8	4 7 3	wf	$$wfff:\mathrm{dom}f⟶{\mathrm{Base}}_w$$
9		csca	$$class\mathrm{Scalar}$$
10	6 9	cfv	$$class\mathrm{Scalar}\left(w\right)$$
11		vs	$$setvars$$
12		vx	$$setvarx$$
13		vk	$$setvark$$
14	11	cv	$$setvars$$
15	14 5	cfv	$$class{\mathrm{Base}}_s$$
16		c0g	$$class{0}_{𝑔}$$
17	14 16	cfv	$$class{0}_s$$
18	17	csn	$$class\left\{0_s\right\}$$
19	15 18	cdif	$$class\left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)$$
20	13	cv	$$setvark$$
21		cvsca	$$class{\cdot }_{𝑠}$$
22	6 21	cfv	$$class{\cdot }_w$$
23	12	cv	$$setvarx$$
24	23 3	cfv	$$classf\left(x\right)$$
25	20 24 22	co	$$class\left(k{\cdot }_{w}f\left(x\right)\right)$$
26		clspn	$$class\mathrm{LSpan}$$
27	6 26	cfv	$$class\mathrm{LSpan}\left(w\right)$$
28	23	csn	$$class\left\{x\right\}$$
29	4 28	cdif	$$class\left(\mathrm{dom}f\setminus \left\{x\right\}\right)$$
30	3 29	cima	$$classf\left[\mathrm{dom}f\setminus \left\{x\right\}\right]$$
31	30 27	cfv	$$class\mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)$$
32	25 31	wcel	$$wffk{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)$$
33	32	wn	$$wff\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)$$
34	33 13 19	wral	$$wff\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)$$
35	34 12 4	wral	$$wff\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)$$
36	35 11 10	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)$$
37	8 36	wa	$$wff\left(f:\mathrm{dom}f⟶{\mathrm{Base}}_w\wedge \underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\right)$$
38	37 1 2	copab	$$class\left\{⟨f,w⟩|\left(f:\mathrm{dom}f⟶{\mathrm{Base}}_w\wedge \underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\right)\right\}$$
39	0 38	wceq	$$wff\mathrm{LIndF}=\left\{⟨f,w⟩|\left(f:\mathrm{dom}f⟶{\mathrm{Base}}_w\wedge \underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\forall x\in \mathrm{dom}f\forall k\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg k{\cdot }_{w}f\left(x\right)\in \mathrm{LSpan}\left(w\right)\left(f\left[\mathrm{dom}f\setminus \left\{x\right\}\right]\right)\right)\right\}$$