Metamath Proof Explorer

Theorem lindsind

Description: A linearly independent set 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 lindsind ⊢ F ∈ LIndS ⁡ W ∧ E ∈ F ∧ A ∈ K ∧ A ≠ 0 ˙ → ¬ A · ˙ E ∈ N ⁡ 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 ∈ LIndS ⁡ W ∧ E ∈ F ∧ A ∈ K ∧ A ≠ 0 ˙ → E ∈ F
7 eldifsn ⊢ A ∈ K ∖ 0 ˙ ↔ A ∈ K ∧ A ≠ 0 ˙
8 7 bilanri ⊢ F ∈ LIndS ⁡ W ∧ E ∈ F ∧ A ∈ K ∧ A ≠ 0 ˙ → A ∈ K ∖ 0 ˙
9 elfvdm ⊢ F ∈ LIndS ⁡ W → W ∈ dom ⁡ LIndS
10 eqid ⊢ Base W = Base W
11 10 1 2 3 5 4 islinds2 ⊢ W ∈ dom ⁡ LIndS → F ∈ LIndS ⁡ W ↔ F ⊆ Base W ∧ ∀ e ∈ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ e ∈ N ⁡ F ∖ e
12 9 11 syl ⊢ F ∈ LIndS ⁡ W → F ∈ LIndS ⁡ W ↔ F ⊆ Base W ∧ ∀ e ∈ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ e ∈ N ⁡ F ∖ e
13 12 ibi ⊢ F ∈ LIndS ⁡ W → F ⊆ Base W ∧ ∀ e ∈ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ e ∈ N ⁡ F ∖ e
14 13 simprd ⊢ F ∈ LIndS ⁡ W → ∀ e ∈ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ e ∈ N ⁡ F ∖ e
15 14 ad2antrr ⊢ F ∈ LIndS ⁡ W ∧ E ∈ F ∧ A ∈ K ∧ A ≠ 0 ˙ → ∀ e ∈ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ e ∈ N ⁡ F ∖ e
16 oveq2 ⊢ e = E → a · ˙ e = a · ˙ E
17 sneq ⊢ e = E → e = E
18 17 difeq2d ⊢ e = E → F ∖ e = F ∖ E
19 18 fveq2d ⊢ e = E → N ⁡ F ∖ e = N ⁡ F ∖ E
20 16 19 eleq12d ⊢ e = E → a · ˙ e ∈ N ⁡ F ∖ e ↔ a · ˙ E ∈ N ⁡ F ∖ E
21 20 notbid ⊢ e = E → ¬ a · ˙ e ∈ N ⁡ F ∖ e ↔ ¬ a · ˙ E ∈ N ⁡ F ∖ E
22 oveq1 ⊢ a = A → a · ˙ E = A · ˙ E
23 22 eleq1d ⊢ a = A → a · ˙ E ∈ N ⁡ F ∖ E ↔ A · ˙ E ∈ N ⁡ F ∖ E
24 23 notbid ⊢ a = A → ¬ a · ˙ E ∈ N ⁡ F ∖ E ↔ ¬ A · ˙ E ∈ N ⁡ F ∖ E
25 21 24 rspc2va ⊢ E ∈ F ∧ A ∈ K ∖ 0 ˙ ∧ ∀ e ∈ F ∀ a ∈ K ∖ 0 ˙ ¬ a · ˙ e ∈ N ⁡ F ∖ e → ¬ A · ˙ E ∈ N ⁡ F ∖ E
26 6 8 15 25 syl21anc ⊢ F ∈ LIndS ⁡ W ∧ E ∈ F ∧ A ∈ K ∧ A ≠ 0 ˙ → ¬ A · ˙ E ∈ N ⁡ F ∖ E