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 ) ∧ 𝐶 ⊆ 𝑉 ∧ ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) → ∃ 𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠 )