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