Metamath Proof Explorer

Theorem islbs4

Description: A basis is an independent spanning set. This could have been used as alternative definition of a basis: LBasis = ( w e. _V |-> { b e. ~P ( Basew ) | ( ( ( LSpanw ) ` `b ) = ( Basew ) /\ b e. ( LIndSw ) ) } ) . (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses islbs4.b ⊢ B = Base W
islbs4.j ⊢ J = LBasis ⁡ W
islbs4.k ⊢ K = LSpan ⁡ W
Assertion islbs4 ⊢ X ∈ J ↔ X ∈ LIndS ⁡ W ∧ K ⁡ X = B

Proof

Step Hyp Ref Expression
1 islbs4.b ⊢ B = Base W
2 islbs4.j ⊢ J = LBasis ⁡ W
3 islbs4.k ⊢ K = LSpan ⁡ W
4 elfvex ⊢ X ∈ LBasis ⁡ W → W ∈ V
5 4 2 eleq2s ⊢ X ∈ J → W ∈ V
6 elfvex ⊢ X ∈ LIndS ⁡ W → W ∈ V
7 6 adantr ⊢ X ∈ LIndS ⁡ W ∧ K ⁡ X = B → W ∈ V
8 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
9 eqid ⊢ ⋅ W = ⋅ W
10 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
11 eqid ⊢ 0 Scalar ⁡ W = 0 Scalar ⁡ W
12 1 8 9 10 2 3 11 islbs ⊢ W ∈ V → X ∈ J ↔ X ⊆ B ∧ K ⁡ X = B ∧ ∀ x ∈ X ∀ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ k ⋅ W x ∈ K ⁡ X ∖ x
13 3anan32 ⊢ X ⊆ B ∧ K ⁡ X = B ∧ ∀ x ∈ X ∀ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ k ⋅ W x ∈ K ⁡ X ∖ x ↔ X ⊆ B ∧ ∀ x ∈ X ∀ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ k ⋅ W x ∈ K ⁡ X ∖ x ∧ K ⁡ X = B
14 1 9 3 8 10 11 islinds2 ⊢ W ∈ V → X ∈ LIndS ⁡ W ↔ X ⊆ B ∧ ∀ x ∈ X ∀ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ k ⋅ W x ∈ K ⁡ X ∖ x
15 14 anbi1d ⊢ W ∈ V → X ∈ LIndS ⁡ W ∧ K ⁡ X = B ↔ X ⊆ B ∧ ∀ x ∈ X ∀ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ k ⋅ W x ∈ K ⁡ X ∖ x ∧ K ⁡ X = B
16 13 15 bitr4id ⊢ W ∈ V → X ⊆ B ∧ K ⁡ X = B ∧ ∀ x ∈ X ∀ k ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ k ⋅ W x ∈ K ⁡ X ∖ x ↔ X ∈ LIndS ⁡ W ∧ K ⁡ X = B
17 12 16 bitrd ⊢ W ∈ V → X ∈ J ↔ X ∈ LIndS ⁡ W ∧ K ⁡ X = B
18 5 7 17 pm5.21nii ⊢ X ∈ J ↔ X ∈ LIndS ⁡ W ∧ K ⁡ X = B