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 ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
lbsind2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lbsind2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lbsind2.o ⊢ 1 = ( 1r ‘ 𝐹 )
lbsind2.z ⊢ 0 = ( 0g ‘ 𝐹 )
Assertion lbsind2 ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → ¬ 𝐸 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝐸 } ) ) )

Proof

Step Hyp Ref Expression
1 lbsind2.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
2 lbsind2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lbsind2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lbsind2.o ⊢ 1 = ( 1r ‘ 𝐹 )
5 lbsind2.z ⊢ 0 = ( 0g ‘ 𝐹 )
6 simp1l ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 𝑊 ∈ LMod )
7 simp2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 𝐵 ∈ 𝐽 )
8 simp3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 𝐸 ∈ 𝐵 )
9 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
10 9 1 lbsel ⊢ ( ( 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 𝐸 ∈ ( Base ‘ 𝑊 ) )
11 7 8 10 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 𝐸 ∈ ( Base ‘ 𝑊 ) )
12 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
13 9 3 12 4 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐸 ∈ ( Base ‘ 𝑊 ) ) → ( 1 ( ·𝑠 ‘ 𝑊 ) 𝐸 ) = 𝐸 )
14 6 11 13 syl2anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → ( 1 ( ·𝑠 ‘ 𝑊 ) 𝐸 ) = 𝐸 )
15 3 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
16 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
17 16 4 ringidcl ⊢ ( 𝐹 ∈ Ring → 1 ∈ ( Base ‘ 𝐹 ) )
18 6 15 17 3syl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 1 ∈ ( Base ‘ 𝐹 ) )
19 simp1r ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → 1 ≠ 0 )
20 9 1 2 3 12 16 5 lbsind ⊢ ( ( ( 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) ∧ ( 1 ∈ ( Base ‘ 𝐹 ) ∧ 1 ≠ 0 ) ) → ¬ ( 1 ( ·𝑠 ‘ 𝑊 ) 𝐸 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝐸 } ) ) )
21 7 8 18 19 20 syl22anc ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → ¬ ( 1 ( ·𝑠 ‘ 𝑊 ) 𝐸 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝐸 } ) ) )
22 14 21 eqneltrrd ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐸 ∈ 𝐵 ) → ¬ 𝐸 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝐸 } ) ) )