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 syl5req 
 |-  ( ( 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 } ) )