Metamath Proof Explorer

Theorem spanpr

Description: The span of a pair of vectors. (Contributed by NM, 9-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion spanpr ⊢A∈ℋ∧B∈ℋ→span⁡A+ℎB⊆span⁡AB

Proof

Step Hyp Ref Expression
1 spansnsh ⊢A∈ℋ→span⁡A∈Sℋ
2 spansnsh ⊢B∈ℋ→span⁡B∈Sℋ
3 shscl ⊢span⁡A∈Sℋ∧span⁡B∈Sℋ→span⁡A+ℋspan⁡B∈Sℋ
4 1 2 3 syl2an ⊢A∈ℋ∧B∈ℋ→span⁡A+ℋspan⁡B∈Sℋ
5 4 adantr ⊢A∈ℋ∧B∈ℋ∧x∈span⁡A+ℎB→span⁡A+ℋspan⁡B∈Sℋ
6 1 2 anim12i ⊢A∈ℋ∧B∈ℋ→span⁡A∈Sℋ∧span⁡B∈Sℋ
7 spansnid ⊢A∈ℋ→A∈span⁡A
8 spansnid ⊢B∈ℋ→B∈span⁡B
9 7 8 anim12i ⊢A∈ℋ∧B∈ℋ→A∈span⁡A∧B∈span⁡B
10 shsva ⊢span⁡A∈Sℋ∧span⁡B∈Sℋ→A∈span⁡A∧B∈span⁡B→A+ℎB∈span⁡A+ℋspan⁡B
11 6 9 10 sylc ⊢A∈ℋ∧B∈ℋ→A+ℎB∈span⁡A+ℋspan⁡B
12 11 adantr ⊢A∈ℋ∧B∈ℋ∧x∈span⁡A+ℎB→A+ℎB∈span⁡A+ℋspan⁡B
13 simpr ⊢A∈ℋ∧B∈ℋ∧x∈span⁡A+ℎB→x∈span⁡A+ℎB
14 elspansn3 ⊢span⁡A+ℋspan⁡B∈Sℋ∧A+ℎB∈span⁡A+ℋspan⁡B∧x∈span⁡A+ℎB→x∈span⁡A+ℋspan⁡B
15 5 12 13 14 syl3anc ⊢A∈ℋ∧B∈ℋ∧x∈span⁡A+ℎB→x∈span⁡A+ℋspan⁡B
16 15 ex ⊢A∈ℋ∧B∈ℋ→x∈span⁡A+ℎB→x∈span⁡A+ℋspan⁡B
17 16 ssrdv ⊢A∈ℋ∧B∈ℋ→span⁡A+ℎB⊆span⁡A+ℋspan⁡B
18 df-pr ⊢AB=A∪B
19 18 fveq2i ⊢span⁡AB=span⁡A∪B
20 snssi ⊢A∈ℋ→A⊆ℋ
21 snssi ⊢B∈ℋ→B⊆ℋ
22 spanun ⊢A⊆ℋ∧B⊆ℋ→span⁡A∪B=span⁡A+ℋspan⁡B
23 20 21 22 syl2an ⊢A∈ℋ∧B∈ℋ→span⁡A∪B=span⁡A+ℋspan⁡B
24 19 23 eqtr2id ⊢A∈ℋ∧B∈ℋ→span⁡A+ℋspan⁡B=span⁡AB
25 17 24 sseqtrd ⊢A∈ℋ∧B∈ℋ→span⁡A+ℎB⊆span⁡AB