Metamath Proof Explorer

Theorem lbslsat

Description: A nonzero vector X is a basis of a line spanned by the singleton X . Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms and for example lsatlspsn . (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypotheses lbslsat.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lbslsat.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lbslsat.z ⊢ 0 = ( 0g ‘ 𝑊 )
lbslsat.y ⊢ 𝑌 = ( 𝑊 ↾s ( 𝑁 ‘ { 𝑋 } ) )
Assertion lbslsat ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → { 𝑋 } ∈ ( LBasis ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 lbslsat.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lbslsat.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lbslsat.z ⊢ 0 = ( 0g ‘ 𝑊 )
4 lbslsat.y ⊢ 𝑌 = ( 𝑊 ↾s ( 𝑁 ‘ { 𝑋 } ) )
5 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
6 snssi ⊢ ( 𝑋 ∈ 𝑉 → { 𝑋 } ⊆ 𝑉 )
7 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
8 1 7 2 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
9 5 6 8 syl2an ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
10 4 7 lsslvec ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → 𝑌 ∈ LVec )
11 9 10 syldan ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → 𝑌 ∈ LVec )
12 11 3adant3 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → 𝑌 ∈ LVec )
13 1 2 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ) → { 𝑋 } ⊆ ( 𝑁 ‘ { 𝑋 } ) )
14 5 6 13 syl2an ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → { 𝑋 } ⊆ ( 𝑁 ‘ { 𝑋 } ) )
15 1 2 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑉 )
16 5 6 15 syl2an ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑉 )
17 4 1 ressbas2 ⊢ ( ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑉 → ( 𝑁 ‘ { 𝑋 } ) = ( Base ‘ 𝑌 ) )
18 16 17 syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) = ( Base ‘ 𝑌 ) )
19 14 18 sseqtrd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → { 𝑋 } ⊆ ( Base ‘ 𝑌 ) )
20 19 3adant3 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → { 𝑋 } ⊆ ( Base ‘ 𝑌 ) )
21 5 adantr ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → 𝑊 ∈ LMod )
22 eqid ⊢ ( LSpan ‘ 𝑌 ) = ( LSpan ‘ 𝑌 )
23 4 2 22 7 lsslsp ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ { 𝑋 } ⊆ ( 𝑁 ‘ { 𝑋 } ) ) → ( ( LSpan ‘ 𝑌 ) ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑋 } ) )
24 21 9 14 23 syl3anc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑌 ) ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑋 } ) )
25 24 3adant3 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ( LSpan ‘ 𝑌 ) ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑋 } ) )
26 18 3adant3 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑋 } ) = ( Base ‘ 𝑌 ) )
27 25 26 eqtrd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ( LSpan ‘ 𝑌 ) ‘ { 𝑋 } ) = ( Base ‘ 𝑌 ) )
28 difid ⊢ ( { 𝑋 } ∖ { 𝑋 } ) = ∅
29 28 fveq2i ⊢ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) = ( ( LSpan ‘ 𝑌 ) ‘ ∅ )
30 29 a1i ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) = ( ( LSpan ‘ 𝑌 ) ‘ ∅ ) )
31 30 eleq2d ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ↔ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ∅ ) ) )
32 31 biimpa ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) → 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ∅ ) )
33 lveclmod ⊢ ( 𝑌 ∈ LVec → 𝑌 ∈ LMod )
34 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
35 34 22 lsp0 ⊢ ( 𝑌 ∈ LMod → ( ( LSpan ‘ 𝑌 ) ‘ ∅ ) = { ( 0g ‘ 𝑌 ) } )
36 11 33 35 3syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑌 ) ‘ ∅ ) = { ( 0g ‘ 𝑌 ) } )
37 36 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) → ( ( LSpan ‘ 𝑌 ) ‘ ∅ ) = { ( 0g ‘ 𝑌 ) } )
38 32 37 eleqtrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) → 𝑋 ∈ { ( 0g ‘ 𝑌 ) } )
39 elsni ⊢ ( 𝑋 ∈ { ( 0g ‘ 𝑌 ) } → 𝑋 = ( 0g ‘ 𝑌 ) )
40 38 39 syl ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) → 𝑋 = ( 0g ‘ 𝑌 ) )
41 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
42 grpmnd ⊢ ( 𝑊 ∈ Grp → 𝑊 ∈ Mnd )
43 21 41 42 3syl ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → 𝑊 ∈ Mnd )
44 3 1 2 0ellsp ⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ) → 0 ∈ ( 𝑁 ‘ { 𝑋 } ) )
45 5 6 44 syl2an ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → 0 ∈ ( 𝑁 ‘ { 𝑋 } ) )
46 4 1 3 ress0g ⊢ ( ( 𝑊 ∈ Mnd ∧ 0 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ 𝑉 ) → 0 = ( 0g ‘ 𝑌 ) )
47 43 45 16 46 syl3anc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → 0 = ( 0g ‘ 𝑌 ) )
48 47 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) → 0 = ( 0g ‘ 𝑌 ) )
49 40 48 eqtr4d ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) → 𝑋 = 0 )
50 49 ex ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) → 𝑋 = 0 ) )
51 50 necon3ad ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ≠ 0 → ¬ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) )
52 51 3impia ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ¬ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) )
53 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
54 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
55 54 difeq2d ⊢ ( 𝑥 = 𝑋 → ( { 𝑋 } ∖ { 𝑥 } ) = ( { 𝑋 } ∖ { 𝑋 } ) )
56 55 fveq2d ⊢ ( 𝑥 = 𝑋 → ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) = ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) )
57 53 56 eleq12d ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ↔ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) )
58 57 notbid ⊢ ( 𝑥 = 𝑋 → ( ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ↔ ¬ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) )
59 58 ralsng ⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑥 ∈ { 𝑋 } ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ↔ ¬ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) )
60 59 3ad2ant2 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( ∀ 𝑥 ∈ { 𝑋 } ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ↔ ¬ 𝑋 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑋 } ) ) ) )
61 52 60 mpbird ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ∀ 𝑥 ∈ { 𝑋 } ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) )
62 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
63 eqid ⊢ ( LBasis ‘ 𝑌 ) = ( LBasis ‘ 𝑌 )
64 62 63 22 islbs2 ⊢ ( 𝑌 ∈ LVec → ( { 𝑋 } ∈ ( LBasis ‘ 𝑌 ) ↔ ( { 𝑋 } ⊆ ( Base ‘ 𝑌 ) ∧ ( ( LSpan ‘ 𝑌 ) ‘ { 𝑋 } ) = ( Base ‘ 𝑌 ) ∧ ∀ 𝑥 ∈ { 𝑋 } ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ) ) )
65 64 biimpar ⊢ ( ( 𝑌 ∈ LVec ∧ ( { 𝑋 } ⊆ ( Base ‘ 𝑌 ) ∧ ( ( LSpan ‘ 𝑌 ) ‘ { 𝑋 } ) = ( Base ‘ 𝑌 ) ∧ ∀ 𝑥 ∈ { 𝑋 } ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑌 ) ‘ ( { 𝑋 } ∖ { 𝑥 } ) ) ) ) → { 𝑋 } ∈ ( LBasis ‘ 𝑌 ) )
66 12 20 27 61 65 syl13anc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → { 𝑋 } ∈ ( LBasis ‘ 𝑌 ) )