This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lbsextg

Description: For any linearly independent subset C of V , there is a basis containing the vectors in C . (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Hypotheses lbsex.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
lbsex.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lbsex.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lbsextg ( ( ( 𝑊 ∈ LVec ∧ 𝒫 𝑉 ∈ dom card ) ∧ 𝐶 ⊆ 𝑉 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) → ∃ 𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠 )

Proof

Step Hyp Ref Expression
1 lbsex.j ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
2 lbsex.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 lbsex.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 simp1l ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝒫 𝑉 ∈ dom card ) ∧ 𝐶 ⊆ 𝑉 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) → 𝑊 ∈ LVec )
5 simp2 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝒫 𝑉 ∈ dom card ) ∧ 𝐶 ⊆ 𝑉 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) → 𝐶 ⊆ 𝑉 )
6 simp3 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝒫 𝑉 ∈ dom card ) ∧ 𝐶 ⊆ 𝑉 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) → ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) )
7 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
8 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
9 8 difeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐶 ∖ { 𝑥 } ) = ( 𝐶 ∖ { 𝑦 } ) )
10 9 fveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝐶 ∖ { 𝑦 } ) ) )
11 7 10 eleq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ↔ 𝑦 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑦 } ) ) ) )
12 11 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ↔ ¬ 𝑦 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑦 } ) ) ) )
13 12 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ 𝐶 ¬ 𝑦 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑦 } ) ) )
14 6 13 sylib ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝒫 𝑉 ∈ dom card ) ∧ 𝐶 ⊆ 𝑉 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) → ∀ 𝑦 ∈ 𝐶 ¬ 𝑦 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑦 } ) ) )
15 8 difeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∖ { 𝑥 } ) = ( 𝑧 ∖ { 𝑦 } ) )
16 15 fveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝑧 ∖ { 𝑦 } ) ) )
17 7 16 eleq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ 𝑦 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑦 } ) ) ) )
18 17 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ ¬ 𝑦 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑦 } ) ) ) )
19 18 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑦 } ) ) )
20 19 anbi2i ⊢ ( ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) ↔ ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑦 } ) ) ) )
21 20 rabbii ⊢ { 𝑧 ∈ 𝒫 𝑉 ∣ ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) } = { 𝑧 ∈ 𝒫 𝑉 ∣ ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑦 } ) ) ) }
22 simp1r ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝒫 𝑉 ∈ dom card ) ∧ 𝐶 ⊆ 𝑉 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) → 𝒫 𝑉 ∈ dom card )
23 2 1 3 4 5 14 21 22 lbsextlem4 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝒫 𝑉 ∈ dom card ) ∧ 𝐶 ⊆ 𝑉 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) → ∃ 𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠 )