Metamath Proof Explorer

Theorem lbspss

Description: No proper subset of a basis spans the space. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lbsind2.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
lbsind2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lbsind2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lbsind2.o ⊢ 1 = ( 1r ‘ 𝐹 )
lbsind2.z ⊢ 0 = ( 0g ‘ 𝐹 )
lbspss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion lbspss ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) → ( 𝑁 ‘ 𝐶 ) ≠ 𝑉 )

Proof

Step Hyp Ref Expression
1 lbsind2.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
2 lbsind2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
3 lbsind2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lbsind2.o ⊢ 1 = ( 1r ‘ 𝐹 )
5 lbsind2.z ⊢ 0 = ( 0g ‘ 𝐹 )
6 lbspss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
7 pssnel ⊢ ( 𝐶 ⊊ 𝐵 → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) )
8 7 3ad2ant3 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) )
9 simpl2 ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → 𝐵 ∈ 𝐽 )
10 6 1 lbsss ⊢ ( 𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉 )
11 9 10 syl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → 𝐵 ⊆ 𝑉 )
12 simprl ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → 𝑥 ∈ 𝐵 )
13 11 12 sseldd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → 𝑥 ∈ 𝑉 )
14 simpl1l ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → 𝑊 ∈ LMod )
15 11 ssdifssd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝑉 )
16 simpl3 ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → 𝐶 ⊊ 𝐵 )
17 16 pssssd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → 𝐶 ⊆ 𝐵 )
18 17 sseld ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ( 𝑦 ∈ 𝐶 → 𝑦 ∈ 𝐵 ) )
19 simprr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ¬ 𝑥 ∈ 𝐶 )
20 eleq1w ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶 ) )
21 20 notbid ⊢ ( 𝑦 = 𝑥 → ( ¬ 𝑦 ∈ 𝐶 ↔ ¬ 𝑥 ∈ 𝐶 ) )
22 19 21 syl5ibrcom ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ( 𝑦 = 𝑥 → ¬ 𝑦 ∈ 𝐶 ) )
23 22 necon2ad ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ( 𝑦 ∈ 𝐶 → 𝑦 ≠ 𝑥 ) )
24 18 23 jcad ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ( 𝑦 ∈ 𝐶 → ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 𝑥 ) ) )
25 eldifsn ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 𝑥 ) )
26 24 25 syl6ibr ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ( 𝑦 ∈ 𝐶 → 𝑦 ∈ ( 𝐵 ∖ { 𝑥 } ) ) )
27 26 ssrdv ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → 𝐶 ⊆ ( 𝐵 ∖ { 𝑥 } ) )
28 6 2 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐵 ∖ { 𝑥 } ) ⊆ 𝑉 ∧ 𝐶 ⊆ ( 𝐵 ∖ { 𝑥 } ) ) → ( 𝑁 ‘ 𝐶 ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
29 14 15 27 28 syl3anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ( 𝑁 ‘ 𝐶 ) ⊆ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
30 simpl1r ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → 1 ≠ 0 )
31 1 2 3 4 5 lbsind2 ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
32 14 30 9 12 31 syl211anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
33 29 32 ssneldd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ¬ 𝑥 ∈ ( 𝑁 ‘ 𝐶 ) )
34 nelne1 ⊢ ( ( 𝑥 ∈ 𝑉 ∧ ¬ 𝑥 ∈ ( 𝑁 ‘ 𝐶 ) ) → 𝑉 ≠ ( 𝑁 ‘ 𝐶 ) )
35 13 33 34 syl2anc ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → 𝑉 ≠ ( 𝑁 ‘ 𝐶 ) )
36 35 necomd ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶 ) ) → ( 𝑁 ‘ 𝐶 ) ≠ 𝑉 )
37 8 36 exlimddv ⊢ ( ( ( 𝑊 ∈ LMod ∧ 1 ≠ 0 ) ∧ 𝐵 ∈ 𝐽 ∧ 𝐶 ⊊ 𝐵 ) → ( 𝑁 ‘ 𝐶 ) ≠ 𝑉 )