Theorem elspansn5

Description: A vector belonging to both a subspace and the span of the singleton of a vector not in it must be zero. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	elspansn5	|- ( A e. SH -> ( ( ( B e. ~H /\ -. B e. A ) /\ ( C e. ( span ` { B } ) /\ C e. A ) ) -> C = 0h ) )

Proof

Step	Hyp	Ref	Expression
1		elspansn4	|- ( ( ( A e. SH /\ B e. ~H ) /\ ( C e. ( span ` { B } ) /\ C =/= 0h ) ) -> ( B e. A <-> C e. A ) )
2	1	biimprd	|- ( ( ( A e. SH /\ B e. ~H ) /\ ( C e. ( span ` { B } ) /\ C =/= 0h ) ) -> ( C e. A -> B e. A ) )
3	2	exp32	|- ( ( A e. SH /\ B e. ~H ) -> ( C e. ( span ` { B } ) -> ( C =/= 0h -> ( C e. A -> B e. A ) ) ) )
4	3	com34	|- ( ( A e. SH /\ B e. ~H ) -> ( C e. ( span ` { B } ) -> ( C e. A -> ( C =/= 0h -> B e. A ) ) ) )
5	4	imp32	|- ( ( ( A e. SH /\ B e. ~H ) /\ ( C e. ( span ` { B } ) /\ C e. A ) ) -> ( C =/= 0h -> B e. A ) )
6	5	necon1bd	|- ( ( ( A e. SH /\ B e. ~H ) /\ ( C e. ( span ` { B } ) /\ C e. A ) ) -> ( -. B e. A -> C = 0h ) )
7	6	exp31	|- ( A e. SH -> ( B e. ~H -> ( ( C e. ( span ` { B } ) /\ C e. A ) -> ( -. B e. A -> C = 0h ) ) ) )
8	7	com34	|- ( A e. SH -> ( B e. ~H -> ( -. B e. A -> ( ( C e. ( span ` { B } ) /\ C e. A ) -> C = 0h ) ) ) )
9	8	imp4c	|- ( A e. SH -> ( ( ( B e. ~H /\ -. B e. A ) /\ ( C e. ( span ` { B } ) /\ C e. A ) ) -> C = 0h ) )