Metamath Proof Explorer

Theorem asplss

Description: The algebraic span of a set of vectors is a vector subspace. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypotheses aspval.a ⊢ A = AlgSpan ⁡ W
aspval.v ⊢ V = Base W
aspval.l ⊢ L = LSubSp ⁡ W
Assertion asplss ⊢ W ∈ AssAlg ∧ S ⊆ V → A ⁡ S ∈ L

Proof

Step Hyp Ref Expression
1 aspval.a ⊢ A = AlgSpan ⁡ W
2 aspval.v ⊢ V = Base W
3 aspval.l ⊢ L = LSubSp ⁡ W
4 1 2 3 aspval ⊢ W ∈ AssAlg ∧ S ⊆ V → A ⁡ S = ⋂ t ∈ SubRing ⁡ W ∩ L | S ⊆ t
5 assalmod ⊢ W ∈ AssAlg → W ∈ LMod
6 5 adantr ⊢ W ∈ AssAlg ∧ S ⊆ V → W ∈ LMod
7 ssrab2 ⊢ t ∈ SubRing ⁡ W ∩ L | S ⊆ t ⊆ SubRing ⁡ W ∩ L
8 inss2 ⊢ SubRing ⁡ W ∩ L ⊆ L
9 7 8 sstri ⊢ t ∈ SubRing ⁡ W ∩ L | S ⊆ t ⊆ L
10 9 a1i ⊢ W ∈ AssAlg ∧ S ⊆ V → t ∈ SubRing ⁡ W ∩ L | S ⊆ t ⊆ L
11 fvex ⊢ A ⁡ S ∈ V
12 4 11 eqeltrrdi ⊢ W ∈ AssAlg ∧ S ⊆ V → ⋂ t ∈ SubRing ⁡ W ∩ L | S ⊆ t ∈ V
13 intex ⊢ t ∈ SubRing ⁡ W ∩ L | S ⊆ t ≠ ∅ ↔ ⋂ t ∈ SubRing ⁡ W ∩ L | S ⊆ t ∈ V
14 12 13 sylibr ⊢ W ∈ AssAlg ∧ S ⊆ V → t ∈ SubRing ⁡ W ∩ L | S ⊆ t ≠ ∅
15 3 lssintcl ⊢ W ∈ LMod ∧ t ∈ SubRing ⁡ W ∩ L | S ⊆ t ⊆ L ∧ t ∈ SubRing ⁡ W ∩ L | S ⊆ t ≠ ∅ → ⋂ t ∈ SubRing ⁡ W ∩ L | S ⊆ t ∈ L
16 6 10 14 15 syl3anc ⊢ W ∈ AssAlg ∧ S ⊆ V → ⋂ t ∈ SubRing ⁡ W ∩ L | S ⊆ t ∈ L
17 4 16 eqeltrd ⊢ W ∈ AssAlg ∧ S ⊆ V → A ⁡ S ∈ L