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 eqtr2id ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( span ‘ { 𝐴 } ) + ( span ‘ { 𝐵 } ) ) = ( span ‘ { 𝐴 , 𝐵 } ) )
25 17 24 sseqtrd ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( span ‘ { ( 𝐴 + 𝐵 ) } ) ⊆ ( span ‘ { 𝐴 , 𝐵 } ) )