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

Metamath Proof Explorer

Theorem lbssp

Description: The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses lbsss.v ⊢ V = Base W
lbsss.j ⊢ J = LBasis ⁡ W
lbssp.n ⊢ N = LSpan ⁡ W
Assertion lbssp ⊢ B ∈ J → N ⁡ B = V

Proof

Step Hyp Ref Expression
1 lbsss.v ⊢ V = Base W
2 lbsss.j ⊢ J = LBasis ⁡ W
3 lbssp.n ⊢ N = LSpan ⁡ W
4 elfvdm ⊢ B ∈ LBasis ⁡ W → W ∈ dom ⁡ LBasis
5 4 2 eleq2s ⊢ B ∈ J → W ∈ dom ⁡ LBasis
6 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
7 eqid ⊢ ⋅ W = ⋅ W
8 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
9 eqid ⊢ 0 Scalar ⁡ W = 0 Scalar ⁡ W
10 1 6 7 8 2 3 9 islbs ⊢ W ∈ dom ⁡ LBasis → B ∈ J ↔ B ⊆ V ∧ N ⁡ B = V ∧ ∀ x ∈ B ∀ y ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ y ⋅ W x ∈ N ⁡ B ∖ x
11 5 10 syl ⊢ B ∈ J → B ∈ J ↔ B ⊆ V ∧ N ⁡ B = V ∧ ∀ x ∈ B ∀ y ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ y ⋅ W x ∈ N ⁡ B ∖ x
12 11 ibi ⊢ B ∈ J → B ⊆ V ∧ N ⁡ B = V ∧ ∀ x ∈ B ∀ y ∈ Base Scalar ⁡ W ∖ 0 Scalar ⁡ W ¬ y ⋅ W x ∈ N ⁡ B ∖ x
13 12 simp2d ⊢ B ∈ J → N ⁡ B = V