This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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