Metamath Proof Explorer

Theorem lindfind

Description: A linearly independent family is independent: no nonzero element multiple can be expressed as a linear combination of the others. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses lindfind.s ⊢ · ˙ = ⋅ W
lindfind.n ⊢ N = LSpan ⁡ W
lindfind.l ⊢ L = Scalar ⁡ W
lindfind.z ⊢ 0 ˙ = 0 L
lindfind.k ⊢ K = Base L
Assertion lindfind ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → ¬ A · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E

Proof

Step Hyp Ref Expression
1 lindfind.s ⊢ · ˙ = ⋅ W
2 lindfind.n ⊢ N = LSpan ⁡ W
3 lindfind.l ⊢ L = Scalar ⁡ W
4 lindfind.z ⊢ 0 ˙ = 0 L
5 lindfind.k ⊢ K = Base L
6 simplr ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → E ∈ dom ⁡ F
7 eldifsn ⊢ A ∈ K ∖ 0 ˙ ↔ A ∈ K ∧ A ≠ 0 ˙
8 7 bilanri ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → A ∈ K ∖ 0 ˙
9 simpll ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → F LIndF W
10 3 5 elbasfv ⊢ A ∈ K → W ∈ V
11 10 ad2antrl ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → W ∈ V
12 rellindf ⊢ Rel ⁡ LIndF
13 12 brrelex1i ⊢ F LIndF W → F ∈ V
14 13 ad2antrr ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → F ∈ V
15 eqid ⊢ Base W = Base W
16 15 1 2 3 5 4 islindf ⊢ W ∈ V ∧ F ∈ V → F LIndF W ↔ F : dom ⁡ F ⟶ Base W ∧ ∀ e ∈ dom ⁡ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ F ⁡ e ∈ N ⁡ F dom ⁡ F ∖ e
17 11 14 16 syl2anc ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → F LIndF W ↔ F : dom ⁡ F ⟶ Base W ∧ ∀ e ∈ dom ⁡ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ F ⁡ e ∈ N ⁡ F dom ⁡ F ∖ e
18 9 17 mpbid ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → F : dom ⁡ F ⟶ Base W ∧ ∀ e ∈ dom ⁡ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ F ⁡ e ∈ N ⁡ F dom ⁡ F ∖ e
19 18 simprd ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → ∀ e ∈ dom ⁡ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ F ⁡ e ∈ N ⁡ F dom ⁡ F ∖ e
20 fveq2 ⊢ e = E → F ⁡ e = F ⁡ E
21 20 oveq2d ⊢ e = E → a · ˙ F ⁡ e = a · ˙ F ⁡ E
22 sneq ⊢ e = E → e = E
23 22 difeq2d ⊢ e = E → dom ⁡ F ∖ e = dom ⁡ F ∖ E
24 23 imaeq2d ⊢ e = E → F dom ⁡ F ∖ e = F dom ⁡ F ∖ E
25 24 fveq2d ⊢ e = E → N ⁡ F dom ⁡ F ∖ e = N ⁡ F dom ⁡ F ∖ E
26 21 25 eleq12d ⊢ e = E → a · ˙ F ⁡ e ∈ N ⁡ F dom ⁡ F ∖ e ↔ a · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E
27 26 notbid ⊢ e = E → ¬ a · ˙ F ⁡ e ∈ N ⁡ F dom ⁡ F ∖ e ↔ ¬ a · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E
28 oveq1 ⊢ a = A → a · ˙ F ⁡ E = A · ˙ F ⁡ E
29 28 eleq1d ⊢ a = A → a · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E ↔ A · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E
30 29 notbid ⊢ a = A → ¬ a · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E ↔ ¬ A · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E
31 27 30 rspc2va ⊢ E ∈ dom ⁡ F ∧ A ∈ K ∖ 0 ˙ ∧ ∀ e ∈ dom ⁡ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ F ⁡ e ∈ N ⁡ F dom ⁡ F ∖ e → ¬ A · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E
32 6 8 19 31 syl21anc ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → ¬ A · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E