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