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

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 ⊢ V = Base W
lbsext.j ⊢ J = LBasis ⁡ W
lbsext.n ⊢ N = LSpan ⁡ W
lbsext.w ⊢ φ → W ∈ LVec
lbsext.c ⊢ φ → C ⊆ V
lbsext.x ⊢ φ → ∀ x ∈ C ¬ x ∈ N ⁡ C ∖ x
lbsext.s ⊢ S = z ∈ 𝒫 V | C ⊆ z ∧ ∀ x ∈ z ¬ x ∈ N ⁡ z ∖ x
Assertion lbsextlem1 ⊢ φ → S ≠ ∅

Proof

Step Hyp Ref Expression
1 lbsext.v ⊢ V = Base W
2 lbsext.j ⊢ J = LBasis ⁡ W
3 lbsext.n ⊢ N = LSpan ⁡ W
4 lbsext.w ⊢ φ → W ∈ LVec
5 lbsext.c ⊢ φ → C ⊆ V
6 lbsext.x ⊢ φ → ∀ x ∈ C ¬ x ∈ N ⁡ C ∖ x
7 lbsext.s ⊢ S = z ∈ 𝒫 V | C ⊆ z ∧ ∀ x ∈ z ¬ x ∈ N ⁡ z ∖ x
8 1 fvexi ⊢ V ∈ V
9 8 elpw2 ⊢ C ∈ 𝒫 V ↔ C ⊆ V
10 5 9 sylibr ⊢ φ → C ∈ 𝒫 V
11 ssid ⊢ C ⊆ C
12 6 11 jctil ⊢ φ → C ⊆ C ∧ ∀ x ∈ C ¬ x ∈ N ⁡ C ∖ x
13 sseq2 ⊢ z = C → C ⊆ z ↔ C ⊆ C
14 difeq1 ⊢ z = C → z ∖ x = C ∖ x
15 14 fveq2d ⊢ z = C → N ⁡ z ∖ x = N ⁡ C ∖ x
16 15 eleq2d ⊢ z = C → x ∈ N ⁡ z ∖ x ↔ x ∈ N ⁡ C ∖ x
17 16 notbid ⊢ z = C → ¬ x ∈ N ⁡ z ∖ x ↔ ¬ x ∈ N ⁡ C ∖ x
18 17 raleqbi1dv ⊢ z = C → ∀ x ∈ z ¬ x ∈ N ⁡ z ∖ x ↔ ∀ x ∈ C ¬ x ∈ N ⁡ C ∖ x
19 13 18 anbi12d ⊢ z = C → C ⊆ z ∧ ∀ x ∈ z ¬ x ∈ N ⁡ z ∖ x ↔ C ⊆ C ∧ ∀ x ∈ C ¬ x ∈ N ⁡ C ∖ x
20 19 7 elrab2 ⊢ C ∈ S ↔ C ∈ 𝒫 V ∧ C ⊆ C ∧ ∀ x ∈ C ¬ x ∈ N ⁡ C ∖ x
21 10 12 20 sylanbrc ⊢ φ → C ∈ S
22 21 ne0d ⊢ φ → S ≠ ∅