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 𝑀 )