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 e. ~H /\ B e. ~H ) -> ( span ` { ( A +h B ) } ) C_ ( span ` { A , B } ) )

Proof

Step Hyp Ref Expression
1 spansnsh
 |-  ( A e. ~H -> ( span ` { A } ) e. SH )
2 spansnsh
 |-  ( B e. ~H -> ( span ` { B } ) e. SH )
3 shscl
 |-  ( ( ( span ` { A } ) e. SH /\ ( span ` { B } ) e. SH ) -> ( ( span ` { A } ) +H ( span ` { B } ) ) e. SH )
4 1 2 3 syl2an
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( span ` { A } ) +H ( span ` { B } ) ) e. SH )
5 4 adantr
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ x e. ( span ` { ( A +h B ) } ) ) -> ( ( span ` { A } ) +H ( span ` { B } ) ) e. SH )
6 1 2 anim12i
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( span ` { A } ) e. SH /\ ( span ` { B } ) e. SH ) )
7 spansnid
 |-  ( A e. ~H -> A e. ( span ` { A } ) )
8 spansnid
 |-  ( B e. ~H -> B e. ( span ` { B } ) )
9 7 8 anim12i
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A e. ( span ` { A } ) /\ B e. ( span ` { B } ) ) )
10 shsva
 |-  ( ( ( span ` { A } ) e. SH /\ ( span ` { B } ) e. SH ) -> ( ( A e. ( span ` { A } ) /\ B e. ( span ` { B } ) ) -> ( A +h B ) e. ( ( span ` { A } ) +H ( span ` { B } ) ) ) )
11 6 9 10 sylc
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A +h B ) e. ( ( span ` { A } ) +H ( span ` { B } ) ) )
12 11 adantr
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ x e. ( span ` { ( A +h B ) } ) ) -> ( A +h B ) e. ( ( span ` { A } ) +H ( span ` { B } ) ) )
13 simpr
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ x e. ( span ` { ( A +h B ) } ) ) -> x e. ( span ` { ( A +h B ) } ) )
14 elspansn3
 |-  ( ( ( ( span ` { A } ) +H ( span ` { B } ) ) e. SH /\ ( A +h B ) e. ( ( span ` { A } ) +H ( span ` { B } ) ) /\ x e. ( span ` { ( A +h B ) } ) ) -> x e. ( ( span ` { A } ) +H ( span ` { B } ) ) )
15 5 12 13 14 syl3anc
 |-  ( ( ( A e. ~H /\ B e. ~H ) /\ x e. ( span ` { ( A +h B ) } ) ) -> x e. ( ( span ` { A } ) +H ( span ` { B } ) ) )
16 15 ex
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( x e. ( span ` { ( A +h B ) } ) -> x e. ( ( span ` { A } ) +H ( span ` { B } ) ) ) )
17 16 ssrdv
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( span ` { ( A +h B ) } ) C_ ( ( span ` { A } ) +H ( span ` { B } ) ) )
18 df-pr
 |-  { A , B } = ( { A } u. { B } )
19 18 fveq2i
 |-  ( span ` { A , B } ) = ( span ` ( { A } u. { B } ) )
20 snssi
 |-  ( A e. ~H -> { A } C_ ~H )
21 snssi
 |-  ( B e. ~H -> { B } C_ ~H )
22 spanun
 |-  ( ( { A } C_ ~H /\ { B } C_ ~H ) -> ( span ` ( { A } u. { B } ) ) = ( ( span ` { A } ) +H ( span ` { B } ) ) )
23 20 21 22 syl2an
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( span ` ( { A } u. { B } ) ) = ( ( span ` { A } ) +H ( span ` { B } ) ) )
24 19 23 eqtr2id
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( span ` { A } ) +H ( span ` { B } ) ) = ( span ` { A , B } ) )
25 17 24 sseqtrd
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( span ` { ( A +h B ) } ) C_ ( span ` { A , B } ) )