Theorem lbsss 21071

Description: A basis is a set of vectors. (Contributed by Mario Carneiro, 24-Jun-2014.)

Hypotheses

Ref	Expression
lbsss.v	⊢ 𝑉 = (Base‘𝑊)
lbsss.j	⊢ 𝐽 = (LBasis‘𝑊)

Assertion

Ref	Expression
lbsss	⊢ (𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉)

Proof of Theorem lbsss

Dummy variables 𝑦 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfvdm 6865	. . . . 5 ⊢ (𝐵 ∈ (LBasis‘𝑊) → 𝑊 ∈ dom LBasis)
2		lbsss.j	. . . . 5 ⊢ 𝐽 = (LBasis‘𝑊)
3	1, 2	eleq2s 2859	. . . 4 ⊢ (𝐵 ∈ 𝐽 → 𝑊 ∈ dom LBasis)
4		lbsss.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑊)
5		eqid 2741	. . . . 5 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
6		eqid 2741	. . . . 5 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
7		eqid 2741	. . . . 5 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
8		eqid 2741	. . . . 5 ⊢ (LSpan‘𝑊) = (LSpan‘𝑊)
9		eqid 2741	. . . . 5 ⊢ (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
10	4, 5, 6, 7, 2, 8, 9	islbs 21070	. . . 4 ⊢ (𝑊 ∈ dom LBasis → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ ((LSpan‘𝑊)‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(𝐵 ∖ {𝑥})))))
11	3, 10	syl 17	. . 3 ⊢ (𝐵 ∈ 𝐽 → (𝐵 ∈ 𝐽 ↔ (𝐵 ⊆ 𝑉 ∧ ((LSpan‘𝑊)‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(𝐵 ∖ {𝑥})))))
12	11	ibi 269	. 2 ⊢ (𝐵 ∈ 𝐽 → (𝐵 ⊆ 𝑉 ∧ ((LSpan‘𝑊)‘𝐵) = 𝑉 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0g‘(Scalar‘𝑊))}) ¬ (𝑦( ·𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘(𝐵 ∖ {𝑥}))))
13	12	simp1d 1149	1 ⊢ (𝐵 ∈ 𝐽 → 𝐵 ⊆ 𝑉)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121  ∀wral 3055   ∖ cdif 3882   ⊆ wss 3885  {csn 4558  dom cdm 5621  ‘cfv 6489  (class class class)co 7360  Basecbs 17174  Scalarcsca 17218   ·_𝑠 cvsca 17219  0_gc0g 17397  LSpanclspn 20965  LBasisclbs 21068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6445  df-fun 6491  df-fv 6497  df-ov 7363  df-lbs 21069

This theorem is referenced by:  lbsel  21072  lbspss  21076  islbs2  21151  islbs3  21152  lmimlbs  21815  lbslsp  33464  lmimdim  33800  lvecdim0  33803  lssdimle  33804  lbsdiflsp0  33822  dimkerim  33823  fedgmullem1  33825  fedgmullem2  33826  fedgmul  33827  dimlssid  33828  extdg1id  33862  fldextrspunlsplem  33869  fldextrspunlsp  33870  fldextrspunlem1  33871