Metamath Proof Explorer


Theorem sumspansn

Description: The sum of two vectors belong to the span of one of them iff the other vector also belongs. (Contributed by NM, 1-Nov-2005) (New usage is discouraged.)

Ref Expression
Assertion sumspansn
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) e. ( span ` { A } ) <-> B e. ( span ` { A } ) ) )

Proof

Step Hyp Ref Expression
1 spansnsh
 |-  ( A e. ~H -> ( span ` { A } ) e. SH )
2 1 adantr
 |-  ( ( A e. ~H /\ ( A +h B ) e. ( span ` { A } ) ) -> ( span ` { A } ) e. SH )
3 simpr
 |-  ( ( A e. ~H /\ ( A +h B ) e. ( span ` { A } ) ) -> ( A +h B ) e. ( span ` { A } ) )
4 spansnid
 |-  ( A e. ~H -> A e. ( span ` { A } ) )
5 4 adantr
 |-  ( ( A e. ~H /\ ( A +h B ) e. ( span ` { A } ) ) -> A e. ( span ` { A } ) )
6 shsubcl
 |-  ( ( ( span ` { A } ) e. SH /\ ( A +h B ) e. ( span ` { A } ) /\ A e. ( span ` { A } ) ) -> ( ( A +h B ) -h A ) e. ( span ` { A } ) )
7 2 3 5 6 syl3anc
 |-  ( ( A e. ~H /\ ( A +h B ) e. ( span ` { A } ) ) -> ( ( A +h B ) -h A ) e. ( span ` { A } ) )
8 7 ex
 |-  ( A e. ~H -> ( ( A +h B ) e. ( span ` { A } ) -> ( ( A +h B ) -h A ) e. ( span ` { A } ) ) )
9 8 adantr
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) e. ( span ` { A } ) -> ( ( A +h B ) -h A ) e. ( span ` { A } ) ) )
10 hvpncan2
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) -h A ) = B )
11 10 eleq1d
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( A +h B ) -h A ) e. ( span ` { A } ) <-> B e. ( span ` { A } ) ) )
12 9 11 sylibd
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) e. ( span ` { A } ) -> B e. ( span ` { A } ) ) )
13 shaddcl
 |-  ( ( ( span ` { A } ) e. SH /\ A e. ( span ` { A } ) /\ B e. ( span ` { A } ) ) -> ( A +h B ) e. ( span ` { A } ) )
14 13 3expia
 |-  ( ( ( span ` { A } ) e. SH /\ A e. ( span ` { A } ) ) -> ( B e. ( span ` { A } ) -> ( A +h B ) e. ( span ` { A } ) ) )
15 1 4 14 syl2anc
 |-  ( A e. ~H -> ( B e. ( span ` { A } ) -> ( A +h B ) e. ( span ` { A } ) ) )
16 15 adantr
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( B e. ( span ` { A } ) -> ( A +h B ) e. ( span ` { A } ) ) )
17 12 16 impbid
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( A +h B ) e. ( span ` { A } ) <-> B e. ( span ` { A } ) ) )