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 biimpri ⊢ A ∈ K ∧ A ≠ 0 ˙ → A ∈ K ∖ 0 ˙
9 8 adantl ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → A ∈ K ∖ 0 ˙
10 simpll ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → F LIndF W
11 3 5 elbasfv ⊢ A ∈ K → W ∈ V
12 11 ad2antrl ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → W ∈ V
13 rellindf ⊢ Rel ⁡ LIndF
14 13 brrelex1i ⊢ F LIndF W → F ∈ V
15 14 ad2antrr ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → F ∈ V
16 eqid ⊢ Base W = Base W
17 16 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
18 12 15 17 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
19 10 18 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
20 19 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
21 fveq2 ⊢ e = E → F ⁡ e = F ⁡ E
22 21 oveq2d ⊢ e = E → a · ˙ F ⁡ e = a · ˙ F ⁡ E
23 sneq ⊢ e = E → e = E
24 23 difeq2d ⊢ e = E → dom ⁡ F ∖ e = dom ⁡ F ∖ E
25 24 imaeq2d ⊢ e = E → F dom ⁡ F ∖ e = F dom ⁡ F ∖ E
26 25 fveq2d ⊢ e = E → N ⁡ F dom ⁡ F ∖ e = N ⁡ F dom ⁡ F ∖ E
27 22 26 eleq12d ⊢ e = E → a · ˙ F ⁡ e ∈ N ⁡ F dom ⁡ F ∖ e ↔ a · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E
28 27 notbid ⊢ e = E → ¬ a · ˙ F ⁡ e ∈ N ⁡ F dom ⁡ F ∖ e ↔ ¬ a · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E
29 oveq1 ⊢ a = A → a · ˙ F ⁡ E = A · ˙ F ⁡ E
30 29 eleq1d ⊢ a = A → a · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E ↔ A · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E
31 30 notbid ⊢ a = A → ¬ a · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E ↔ ¬ A · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E
32 28 31 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
33 6 9 20 32 syl21anc ⊢ F LIndF W ∧ E ∈ dom ⁡ F ∧ A ∈ K ∧ A ≠ 0 ˙ → ¬ A · ˙ F ⁡ E ∈ N ⁡ F dom ⁡ F ∖ E