Metamath Proof Explorer


Theorem lbsextlem1

Description: Lemma for lbsext . The set S is the set of all linearly independent sets containing C ; we show here that it is nonempty. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lbsext.v 𝑉 = ( Base ‘ 𝑊 )
lbsext.j 𝐽 = ( LBasis ‘ 𝑊 )
lbsext.n 𝑁 = ( LSpan ‘ 𝑊 )
lbsext.w ( 𝜑𝑊 ∈ LVec )
lbsext.c ( 𝜑𝐶𝑉 )
lbsext.x ( 𝜑 → ∀ 𝑥𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) )
lbsext.s 𝑆 = { 𝑧 ∈ 𝒫 𝑉 ∣ ( 𝐶𝑧 ∧ ∀ 𝑥𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) }
Assertion lbsextlem1 ( 𝜑𝑆 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 lbsext.v 𝑉 = ( Base ‘ 𝑊 )
2 lbsext.j 𝐽 = ( LBasis ‘ 𝑊 )
3 lbsext.n 𝑁 = ( LSpan ‘ 𝑊 )
4 lbsext.w ( 𝜑𝑊 ∈ LVec )
5 lbsext.c ( 𝜑𝐶𝑉 )
6 lbsext.x ( 𝜑 → ∀ 𝑥𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) )
7 lbsext.s 𝑆 = { 𝑧 ∈ 𝒫 𝑉 ∣ ( 𝐶𝑧 ∧ ∀ 𝑥𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) }
8 1 fvexi 𝑉 ∈ V
9 8 elpw2 ( 𝐶 ∈ 𝒫 𝑉𝐶𝑉 )
10 5 9 sylibr ( 𝜑𝐶 ∈ 𝒫 𝑉 )
11 ssid 𝐶𝐶
12 6 11 jctil ( 𝜑 → ( 𝐶𝐶 ∧ ∀ 𝑥𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) )
13 sseq2 ( 𝑧 = 𝐶 → ( 𝐶𝑧𝐶𝐶 ) )
14 difeq1 ( 𝑧 = 𝐶 → ( 𝑧 ∖ { 𝑥 } ) = ( 𝐶 ∖ { 𝑥 } ) )
15 14 fveq2d ( 𝑧 = 𝐶 → ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) )
16 15 eleq2d ( 𝑧 = 𝐶 → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) )
17 16 notbid ( 𝑧 = 𝐶 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) )
18 17 raleqbi1dv ( 𝑧 = 𝐶 → ( ∀ 𝑥𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) )
19 13 18 anbi12d ( 𝑧 = 𝐶 → ( ( 𝐶𝑧 ∧ ∀ 𝑥𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) ↔ ( 𝐶𝐶 ∧ ∀ 𝑥𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) ) )
20 19 7 elrab2 ( 𝐶𝑆 ↔ ( 𝐶 ∈ 𝒫 𝑉 ∧ ( 𝐶𝐶 ∧ ∀ 𝑥𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) ) ) )
21 10 12 20 sylanbrc ( 𝜑𝐶𝑆 )
22 21 ne0d ( 𝜑𝑆 ≠ ∅ )