This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lbsind2

Description: A basis is linearly independent; that is, every element is not in the span of the remainder of the basis. (Contributed by Mario Carneiro, 25-Jun-2014) (Revised by Mario Carneiro, 12-Jan-2015)

Ref Expression
Hypotheses lbsind2.j ⊢ J = LBasis ⁡ W
lbsind2.n ⊢ N = LSpan ⁡ W
lbsind2.f ⊢ F = Scalar ⁡ W
lbsind2.o ⊢ 1 ˙ = 1 F
lbsind2.z ⊢ 0 ˙ = 0 F
Assertion lbsind2 ⊢ W ∈ LMod ∧ 1 ˙ ≠ 0 ˙ ∧ B ∈ J ∧ E ∈ B → ¬ E ∈ N ⁡ B ∖ E

Proof

Step Hyp Ref Expression
1 lbsind2.j ⊢ J = LBasis ⁡ W
2 lbsind2.n ⊢ N = LSpan ⁡ W
3 lbsind2.f ⊢ F = Scalar ⁡ W
4 lbsind2.o ⊢ 1 ˙ = 1 F
5 lbsind2.z ⊢ 0 ˙ = 0 F
6 simp1l ⊢ W ∈ LMod ∧ 1 ˙ ≠ 0 ˙ ∧ B ∈ J ∧ E ∈ B → W ∈ LMod
7 simp2 ⊢ W ∈ LMod ∧ 1 ˙ ≠ 0 ˙ ∧ B ∈ J ∧ E ∈ B → B ∈ J
8 simp3 ⊢ W ∈ LMod ∧ 1 ˙ ≠ 0 ˙ ∧ B ∈ J ∧ E ∈ B → E ∈ B
9 eqid ⊢ Base W = Base W
10 9 1 lbsel ⊢ B ∈ J ∧ E ∈ B → E ∈ Base W
11 7 8 10 syl2anc ⊢ W ∈ LMod ∧ 1 ˙ ≠ 0 ˙ ∧ B ∈ J ∧ E ∈ B → E ∈ Base W
12 eqid ⊢ ⋅ W = ⋅ W
13 9 3 12 4 lmodvs1 ⊢ W ∈ LMod ∧ E ∈ Base W → 1 ˙ ⋅ W E = E
14 6 11 13 syl2anc ⊢ W ∈ LMod ∧ 1 ˙ ≠ 0 ˙ ∧ B ∈ J ∧ E ∈ B → 1 ˙ ⋅ W E = E
15 3 lmodring ⊢ W ∈ LMod → F ∈ Ring
16 eqid ⊢ Base F = Base F
17 16 4 ringidcl ⊢ F ∈ Ring → 1 ˙ ∈ Base F
18 6 15 17 3syl ⊢ W ∈ LMod ∧ 1 ˙ ≠ 0 ˙ ∧ B ∈ J ∧ E ∈ B → 1 ˙ ∈ Base F
19 simp1r ⊢ W ∈ LMod ∧ 1 ˙ ≠ 0 ˙ ∧ B ∈ J ∧ E ∈ B → 1 ˙ ≠ 0 ˙
20 9 1 2 3 12 16 5 lbsind ⊢ B ∈ J ∧ E ∈ B ∧ 1 ˙ ∈ Base F ∧ 1 ˙ ≠ 0 ˙ → ¬ 1 ˙ ⋅ W E ∈ N ⁡ B ∖ E
21 7 8 18 19 20 syl22anc ⊢ W ∈ LMod ∧ 1 ˙ ≠ 0 ˙ ∧ B ∈ J ∧ E ∈ B → ¬ 1 ˙ ⋅ W E ∈ N ⁡ B ∖ E
22 14 21 eqneltrrd ⊢ W ∈ LMod ∧ 1 ˙ ≠ 0 ˙ ∧ B ∈ J ∧ E ∈ B → ¬ E ∈ N ⁡ B ∖ E