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. = ( 1r ` F )
lbsind2.z 
|- .0. = ( 0g ` F )
Assertion lbsind2 
|- ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> -. E 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. = ( 1r ` F )
5 lbsind2.z 
 |-  .0. = ( 0g ` F )
6 simp1l 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> W e. LMod )
7 simp2 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> B e. J )
8 simp3 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> E e. B )
9 eqid 
 |-  ( Base ` W ) = ( Base ` W )
10 9 1 lbsel 
 |-  ( ( B e. J /\ E e. B ) -> E e. ( Base ` W ) )
11 7 8 10 syl2anc 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> E e. ( Base ` W ) )
12 eqid 
 |-  ( .s ` W ) = ( .s ` W )
13 9 3 12 4 lmodvs1 
 |-  ( ( W e. LMod /\ E e. ( Base ` W ) ) -> ( .1. ( .s ` W ) E ) = E )
14 6 11 13 syl2anc 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> ( .1. ( .s ` W ) E ) = E )
15 3 lmodring 
 |-  ( W e. LMod -> F e. Ring )
16 eqid 
 |-  ( Base ` F ) = ( Base ` F )
17 16 4 ringidcl 
 |-  ( F e. Ring -> .1. e. ( Base ` F ) )
18 6 15 17 3syl 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> .1. e. ( Base ` F ) )
19 simp1r 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> .1. =/= .0. )
20 9 1 2 3 12 16 5 lbsind 
 |-  ( ( ( B e. J /\ E e. B ) /\ ( .1. e. ( Base ` F ) /\ .1. =/= .0. ) ) -> -. ( .1. ( .s ` W ) E ) e. ( N ` ( B \ { E } ) ) )
21 7 8 18 19 20 syl22anc 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> -. ( .1. ( .s ` W ) E ) e. ( N ` ( B \ { E } ) ) )
22 14 21 eqneltrrd 
 |-  ( ( ( W e. LMod /\ .1. =/= .0. ) /\ B e. J /\ E e. B ) -> -. E e. ( N ` ( B \ { E } ) ) )