Metamath Proof Explorer

Theorem lindssn

Description: Any singleton of a nonzero element is an independent set. (Contributed by Thierry Arnoux, 5-Aug-2023)

Ref Expression
Hypotheses lindssn.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
lindssn.2 ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion lindssn ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → { 𝑋 } ∈ ( LIndS ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 lindssn.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 lindssn.2 ⊢ 0 = ( 0g ‘ 𝑊 )
3 simp1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑊 ∈ LVec )
4 snssi ⊢ ( 𝑋 ∈ 𝐵 → { 𝑋 } ⊆ 𝐵 )
5 4 3ad2ant2 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → { 𝑋 } ⊆ 𝐵 )
6 simpr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
7 eldifsni ⊢ ( 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) → 𝑦 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
8 6 7 syl ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝑦 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
9 8 neneqd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ¬ 𝑦 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
10 simpl3 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝑋 ≠ 0 )
11 10 neneqd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ¬ 𝑋 = 0 )
12 ioran ⊢ ( ¬ ( 𝑦 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∨ 𝑋 = 0 ) ↔ ( ¬ 𝑦 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ¬ 𝑋 = 0 ) )
13 9 11 12 sylanbrc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ¬ ( 𝑦 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∨ 𝑋 = 0 ) )
14 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
15 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
16 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
17 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
18 3 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝑊 ∈ LVec )
19 6 eldifad ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
20 simpl2 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝑋 ∈ 𝐵 )
21 1 14 15 16 17 2 18 19 20 lvecvs0or ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 0 ↔ ( 𝑦 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∨ 𝑋 = 0 ) ) )
22 21 necon3abid ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ≠ 0 ↔ ¬ ( 𝑦 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∨ 𝑋 = 0 ) ) )
23 13 22 mpbird ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ≠ 0 )
24 nelsn ⊢ ( ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ≠ 0 → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ { 0 } )
25 23 24 syl ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ { 0 } )
26 difid ⊢ ( { 𝑋 } ∖ { 𝑋 } ) = ∅
27 26 a1i ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( { 𝑋 } ∖ { 𝑋 } ) = ∅ )
28 27 fveq2d ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) = ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) )
29 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
30 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
31 2 30 lsp0 ⊢ ( 𝑊 ∈ LMod → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } )
32 3 29 31 3syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } )
33 32 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ∅ ) = { 0 } )
34 28 33 eqtrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) = { 0 } )
35 25 34 neleqtrrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) )
36 35 ralrimiva ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) )
37 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) = ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
38 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
39 38 difeq2d ⊢ ( 𝑥 = 𝑋 → ( { 𝑋 } ∖ { 𝑥 } ) = ( { 𝑋 } ∖ { 𝑋 } ) )
40 39 fveq2d ⊢ ( 𝑥 = 𝑋 → ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) = ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) )
41 37 40 eleq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ↔ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) )
42 41 notbid ⊢ ( 𝑥 = 𝑋 → ( ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ↔ ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) )
43 42 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) )
44 43 ralsng ⊢ ( 𝑋 ∈ 𝐵 → ( ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) )
45 44 3ad2ant2 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) )
46 36 45 mpbird ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) )
47 1 14 30 15 16 17 islinds2 ⊢ ( 𝑊 ∈ LVec → ( { 𝑋 } ∈ ( LIndS ‘ 𝑊 ) ↔ ( { 𝑋 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ) ) )
48 47 biimpar ⊢ ( ( 𝑊 ∈ LVec ∧ ( { 𝑋 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ { 𝑋 } ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ) ) → { 𝑋 } ∈ ( LIndS ‘ 𝑊 ) )
49 3 5 46 48 syl12anc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → { 𝑋 } ∈ ( LIndS ‘ 𝑊 ) )