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 ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ⊆ ( span ‘ { 𝐴 , 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 spansnsh ⊢ ( 𝐴 ∈ ℋ → ( span ‘ { 𝐴 } ) ∈ Sℋ )
2 spansnsh ⊢ ( 𝐵 ∈ ℋ → ( span ‘ { 𝐵 } ) ∈ Sℋ )
3 shscl ⊢ ( ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ ( span ‘ { 𝐵 } ) ∈ Sℋ ) → ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ∈ Sℋ )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ∈ Sℋ )
5 4 adantr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) → ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ∈ Sℋ )
6 1 2 anim12i ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ ( span ‘ { 𝐵 } ) ∈ Sℋ ) )
7 spansnid ⊢ ( 𝐴 ∈ ℋ → 𝐴 ∈ ( span ‘ { 𝐴 } ) )
8 spansnid ⊢ ( 𝐵 ∈ ℋ → 𝐵 ∈ ( span ‘ { 𝐵 } ) )
9 7 8 anim12i ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ∈ ( span ‘ { 𝐴 } ) ∧ 𝐵 ∈ ( span ‘ { 𝐵 } ) ) )
10 shsva ⊢ ( ( ( span ‘ { 𝐴 } ) ∈ Sℋ ∧ ( span ‘ { 𝐵 } ) ∈ Sℋ ) → ( ( 𝐴 ∈ ( span ‘ { 𝐴 } ) ∧ 𝐵 ∈ ( span ‘ { 𝐵 } ) ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) )
11 6 9 10 sylc ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) )
12 11 adantr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) → ( 𝐴 +ℎ 𝐵 ) ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) )
13 simpr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) → 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) )
14 elspansn3 ⊢ ( ( ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ∈ Sℋ ∧ ( 𝐴 +ℎ 𝐵 ) ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ∧ 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) → 𝑥 ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) )
15 5 12 13 14 syl3anc ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ) → 𝑥 ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) )
16 15 ex ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝑥 ∈ ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) → 𝑥 ∈ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) ) )
17 16 ssrdv ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ⊆ ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) )
18 df-pr ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
19 18 fveq2i ⊢ ( span ‘ { 𝐴 , 𝐵 } ) = ( span ‘ ( { 𝐴 } ∪ { 𝐵 } ) )
20 snssi ⊢ ( 𝐴 ∈ ℋ → { 𝐴 } ⊆ ℋ )
21 snssi ⊢ ( 𝐵 ∈ ℋ → { 𝐵 } ⊆ ℋ )
22 spanun ⊢ ( ( { 𝐴 } ⊆ ℋ ∧ { 𝐵 } ⊆ ℋ ) → ( span ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) )
23 20 21 22 syl2an ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( span ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) )
24 19 23 syl5req ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( span ‘ { 𝐴 } ) +ℋ ( span ‘ { 𝐵 } ) ) = ( span ‘ { 𝐴 , 𝐵 } ) )
25 17 24 sseqtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( span ‘ { ( 𝐴 +ℎ 𝐵 ) } ) ⊆ ( span ‘ { 𝐴 , 𝐵 } ) )