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 ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) → { 𝑆 } linIndS 𝑀 )

Proof

Step Hyp Ref Expression
1 eldifsni ⊢ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) → 𝑠 ≠ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
2 1 adantl ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ) → 𝑠 ≠ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
3 simpl3 ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ) → 𝑆 ≠ ( 0g ‘ 𝑀 ) )
4 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
5 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
6 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
7 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
8 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) )
9 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
10 simpl1 ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ) → 𝑀 ∈ LVec )
11 eldifi ⊢ ( 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) → 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
12 11 adantl ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ) → 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
13 simpl2 ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ) → 𝑆 ∈ ( Base ‘ 𝑀 ) )
14 4 5 6 7 8 9 10 12 13 lvecvsn0 ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ) → ( ( 𝑠 ( ·𝑠 ‘ 𝑀 ) 𝑆 ) ≠ ( 0g ‘ 𝑀 ) ↔ ( 𝑠 ≠ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) ) )
15 2 3 14 mpbir2and ⊢ ( ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ) → ( 𝑠 ( ·𝑠 ‘ 𝑀 ) 𝑆 ) ≠ ( 0g ‘ 𝑀 ) )
16 15 ralrimiva ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ( 𝑠 ( ·𝑠 ‘ 𝑀 ) 𝑆 ) ≠ ( 0g ‘ 𝑀 ) )
17 lveclmod ⊢ ( 𝑀 ∈ LVec → 𝑀 ∈ LMod )
18 17 anim1i ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ) )
19 18 3adant3 ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) → ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ) )
20 4 6 7 8 9 5 snlindsntor ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ) → ( ∀ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ( 𝑠 ( ·𝑠 ‘ 𝑀 ) 𝑆 ) ≠ ( 0g ‘ 𝑀 ) ↔ { 𝑆 } linIndS 𝑀 ) )
21 19 20 syl ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) → ( ∀ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑀 ) ) } ) ( 𝑠 ( ·𝑠 ‘ 𝑀 ) 𝑆 ) ≠ ( 0g ‘ 𝑀 ) ↔ { 𝑆 } linIndS 𝑀 ) )
22 16 21 mpbid ⊢ ( ( 𝑀 ∈ LVec ∧ 𝑆 ∈ ( Base ‘ 𝑀 ) ∧ 𝑆 ≠ ( 0g ‘ 𝑀 ) ) → { 𝑆 } linIndS 𝑀 )