Metamath Proof Explorer

Theorem lindssnlvec

Description: A singleton not containing the zero element of a vector space is always linearly independent. (Contributed by AV, 16-Apr-2019) (Revised by AV, 28-Apr-2019)

Ref Expression
Assertion lindssnlvec 
|- ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) -> { S } linIndS M )

Proof

Step Hyp Ref Expression
1 eldifsni 
 |-  ( s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) -> s =/= ( 0g ` ( Scalar ` M ) ) )
2 1 adantl 
 |-  ( ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) /\ s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) ) -> s =/= ( 0g ` ( Scalar ` M ) ) )
3 simpl3 
 |-  ( ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) /\ s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) ) -> S =/= ( 0g ` M ) )
4 eqid 
 |-  ( Base ` M ) = ( Base ` M )
5 eqid 
 |-  ( .s ` M ) = ( .s ` M )
6 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
7 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
8 eqid 
 |-  ( 0g ` ( Scalar ` M ) ) = ( 0g ` ( Scalar ` M ) )
9 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
10 simpl1 
 |-  ( ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) /\ s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) ) -> M e. LVec )
11 eldifi 
 |-  ( s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) -> s e. ( Base ` ( Scalar ` M ) ) )
12 11 adantl 
 |-  ( ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) /\ s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) ) -> s e. ( Base ` ( Scalar ` M ) ) )
13 simpl2 
 |-  ( ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) /\ s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) ) -> S e. ( Base ` M ) )
14 4 5 6 7 8 9 10 12 13 lvecvsn0 
 |-  ( ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) /\ s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) ) -> ( ( s ( .s ` M ) S ) =/= ( 0g ` M ) <-> ( s =/= ( 0g ` ( Scalar ` M ) ) /\ S =/= ( 0g ` M ) ) ) )
15 2 3 14 mpbir2and 
 |-  ( ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) /\ s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) ) -> ( s ( .s ` M ) S ) =/= ( 0g ` M ) )
16 15 ralrimiva 
 |-  ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) -> A. s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) ( s ( .s ` M ) S ) =/= ( 0g ` M ) )
17 lveclmod 
 |-  ( M e. LVec -> M e. LMod )
18 17 anim1i 
 |-  ( ( M e. LVec /\ S e. ( Base ` M ) ) -> ( M e. LMod /\ S e. ( Base ` M ) ) )
19 18 3adant3 
 |-  ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) -> ( M e. LMod /\ S e. ( Base ` M ) ) )
20 4 6 7 8 9 5 snlindsntor 
 |-  ( ( M e. LMod /\ S e. ( Base ` M ) ) -> ( A. s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) ( s ( .s ` M ) S ) =/= ( 0g ` M ) <-> { S } linIndS M ) )
21 19 20 syl 
 |-  ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) -> ( A. s e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) ( s ( .s ` M ) S ) =/= ( 0g ` M ) <-> { S } linIndS M ) )
22 16 21 mpbid 
 |-  ( ( M e. LVec /\ S e. ( Base ` M ) /\ S =/= ( 0g ` M ) ) -> { S } linIndS M )