Metamath Proof Explorer

Theorem elspansn4

Description: A span membership condition implying two vectors belong to the same subspace. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 elspansn3 
 |-  ( ( A e. SH /\ B e. A /\ C e. ( span ` { B } ) ) -> C e. A )
2 1 3exp 
 |-  ( A e. SH -> ( B e. A -> ( C e. ( span ` { B } ) -> C e. A ) ) )
3 2 com23 
 |-  ( A e. SH -> ( C e. ( span ` { B } ) -> ( B e. A -> C e. A ) ) )
4 3 imp 
 |-  ( ( A e. SH /\ C e. ( span ` { B } ) ) -> ( B e. A -> C e. A ) )
5 4 ad2ant2r 
 |-  ( ( ( A e. SH /\ B e. ~H ) /\ ( C e. ( span ` { B } ) /\ C =/= 0h ) ) -> ( B e. A -> C e. A ) )
6 spansnid 
 |-  ( B e. ~H -> B e. ( span ` { B } ) )
7 6 ad2antrr 
 |-  ( ( ( B e. ~H /\ C =/= 0h ) /\ C e. ( span ` { B } ) ) -> B e. ( span ` { B } ) )
8 spansneleq 
 |-  ( ( B e. ~H /\ C =/= 0h ) -> ( C e. ( span ` { B } ) -> ( span ` { C } ) = ( span ` { B } ) ) )
9 8 imp 
 |-  ( ( ( B e. ~H /\ C =/= 0h ) /\ C e. ( span ` { B } ) ) -> ( span ` { C } ) = ( span ` { B } ) )
10 7 9 eleqtrrd 
 |-  ( ( ( B e. ~H /\ C =/= 0h ) /\ C e. ( span ` { B } ) ) -> B e. ( span ` { C } ) )
11 elspansn3 
 |-  ( ( A e. SH /\ C e. A /\ B e. ( span ` { C } ) ) -> B e. A )
12 11 3expia 
 |-  ( ( A e. SH /\ C e. A ) -> ( B e. ( span ` { C } ) -> B e. A ) )
13 10 12 syl5 
 |-  ( ( A e. SH /\ C e. A ) -> ( ( ( B e. ~H /\ C =/= 0h ) /\ C e. ( span ` { B } ) ) -> B e. A ) )
14 13 exp4b 
 |-  ( A e. SH -> ( C e. A -> ( ( B e. ~H /\ C =/= 0h ) -> ( C e. ( span ` { B } ) -> B e. A ) ) ) )
15 14 com24 
 |-  ( A e. SH -> ( C e. ( span ` { B } ) -> ( ( B e. ~H /\ C =/= 0h ) -> ( C e. A -> B e. A ) ) ) )
16 15 exp4a 
 |-  ( A e. SH -> ( C e. ( span ` { B } ) -> ( B e. ~H -> ( C =/= 0h -> ( C e. A -> B e. A ) ) ) ) )
17 16 com23 
 |-  ( A e. SH -> ( B e. ~H -> ( C e. ( span ` { B } ) -> ( C =/= 0h -> ( C e. A -> B e. A ) ) ) ) )
18 17 imp43 
 |-  ( ( ( A e. SH /\ B e. ~H ) /\ ( C e. ( span ` { B } ) /\ C =/= 0h ) ) -> ( C e. A -> B e. A ) )
19 5 18 impbid 
 |-  ( ( ( A e. SH /\ B e. ~H ) /\ ( C e. ( span ` { B } ) /\ C =/= 0h ) ) -> ( B e. A <-> C e. A ) )