Metamath Proof Explorer

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]˙ ∀ x ∈ dom ⁡ f ∀ k ∈ Base s ∖ 0 s ¬ k ⋅ w f ⁡ x ∈ LSpan ⁡ w ⁡ f dom ⁡ f ∖ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 clindf class LIndF
1 vf setvar f
2 vw setvar w
3 1 cv setvar f
4 3 cdm class dom ⁡ f
5 cbs class Base
6 2 cv setvar w
7 6 5 cfv class Base w
8 4 7 3 wf wff f : dom ⁡ f ⟶ Base w
9 csca class Scalar
10 6 9 cfv class Scalar ⁡ w
11 vs setvar s
12 vx setvar x
13 vk setvar k
14 11 cv setvar s
15 14 5 cfv class Base s
16 c0g class 0 𝑔
17 14 16 cfv class 0 s
18 17 csn class 0 s
19 15 18 cdif class Base s ∖ 0 s
20 13 cv setvar k
21 cvsca class ⋅ 𝑠
22 6 21 cfv class ⋅ w
23 12 cv setvar x
24 23 3 cfv class f ⁡ x
25 20 24 22 co class k ⋅ w f ⁡ x
26 clspn class LSpan
27 6 26 cfv class LSpan ⁡ w
28 23 csn class x
29 4 28 cdif class dom ⁡ f ∖ x
30 3 29 cima class f dom ⁡ f ∖ x
31 30 27 cfv class LSpan ⁡ w ⁡ f dom ⁡ f ∖ x
32 25 31 wcel wff k ⋅ w f ⁡ x ∈ LSpan ⁡ w ⁡ f dom ⁡ f ∖ x
33 32 wn wff ¬ k ⋅ w f ⁡ x ∈ LSpan ⁡ w ⁡ f dom ⁡ f ∖ x
34 33 13 19 wral wff ∀ k ∈ Base s ∖ 0 s ¬ k ⋅ w f ⁡ x ∈ LSpan ⁡ w ⁡ f dom ⁡ f ∖ x
35 34 12 4 wral wff ∀ x ∈ dom ⁡ f ∀ k ∈ Base s ∖ 0 s ¬ k ⋅ w f ⁡ x ∈ LSpan ⁡ w ⁡ f dom ⁡ f ∖ x
36 35 11 10 wsbc wff [˙ Scalar ⁡ w / s]˙ ∀ x ∈ dom ⁡ f ∀ k ∈ Base s ∖ 0 s ¬ k ⋅ w f ⁡ x ∈ LSpan ⁡ w ⁡ f dom ⁡ f ∖ x
37 8 36 wa wff f : dom ⁡ f ⟶ Base w ∧ [˙ Scalar ⁡ w / s]˙ ∀ x ∈ dom ⁡ f ∀ k ∈ Base s ∖ 0 s ¬ k ⋅ w f ⁡ x ∈ LSpan ⁡ w ⁡ f dom ⁡ f ∖ x
38 37 1 2 copab class f w | f : dom ⁡ f ⟶ Base w ∧ [˙ Scalar ⁡ w / s]˙ ∀ x ∈ dom ⁡ f ∀ k ∈ Base s ∖ 0 s ¬ k ⋅ w f ⁡ x ∈ LSpan ⁡ w ⁡ f dom ⁡ f ∖ x
39 0 38 wceq wff LIndF = f w | f : dom ⁡ f ⟶ Base w ∧ [˙ Scalar ⁡ w / s]˙ ∀ x ∈ dom ⁡ f ∀ k ∈ Base s ∖ 0 s ¬ k ⋅ w f ⁡ x ∈ LSpan ⁡ w ⁡ f dom ⁡ f ∖ x