Metamath Proof Explorer

Theorem elspansn2

Description: Membership in the span of a singleton. All members are collinear with the generating vector. (Contributed by NM, 5-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 spansn 
 |-  ( B e. ~H -> ( span ` { B } ) = ( _|_ ` ( _|_ ` { B } ) ) )
2 1 eleq2d 
 |-  ( B e. ~H -> ( A e. ( span ` { B } ) <-> A e. ( _|_ ` ( _|_ ` { B } ) ) ) )
3 2 3ad2ant2 
 |-  ( ( A e. ~H /\ B e. ~H /\ B =/= 0h ) -> ( A e. ( span ` { B } ) <-> A e. ( _|_ ` ( _|_ ` { B } ) ) ) )
4 eleq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { B } ) ) ) )
5 id 
 |-  ( A = if ( A e. ~H , A , 0h ) -> A = if ( A e. ~H , A , 0h ) )
6 oveq1 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A .ih B ) = ( if ( A e. ~H , A , 0h ) .ih B ) )
7 6 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( A .ih B ) / ( B .ih B ) ) = ( ( if ( A e. ~H , A , 0h ) .ih B ) / ( B .ih B ) ) )
8 7 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) = ( ( ( if ( A e. ~H , A , 0h ) .ih B ) / ( B .ih B ) ) .h B ) )
9 5 8 eqeq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) <-> if ( A e. ~H , A , 0h ) = ( ( ( if ( A e. ~H , A , 0h ) .ih B ) / ( B .ih B ) ) .h B ) ) )
10 4 9 bibi12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) <-> ( if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. ~H , A , 0h ) = ( ( ( if ( A e. ~H , A , 0h ) .ih B ) / ( B .ih B ) ) .h B ) ) ) )
11 10 imbi2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( B =/= 0h -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) ) <-> ( B =/= 0h -> ( if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. ~H , A , 0h ) = ( ( ( if ( A e. ~H , A , 0h ) .ih B ) / ( B .ih B ) ) .h B ) ) ) ) )
12 neeq1 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( B =/= 0h <-> if ( B e. ~H , B , 0h ) =/= 0h ) )
13 sneq 
 |-  ( B = if ( B e. ~H , B , 0h ) -> { B } = { if ( B e. ~H , B , 0h ) } )
14 13 fveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( _|_ ` { B } ) = ( _|_ ` { if ( B e. ~H , B , 0h ) } ) )
15 14 fveq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( _|_ ` ( _|_ ` { B } ) ) = ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) )
16 15 eleq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) ) )
17 oveq2 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) .ih B ) = ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) )
18 oveq1 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( B .ih B ) = ( if ( B e. ~H , B , 0h ) .ih B ) )
19 oveq2 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( B e. ~H , B , 0h ) .ih B ) = ( if ( B e. ~H , B , 0h ) .ih if ( B e. ~H , B , 0h ) ) )
20 18 19 eqtrd 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( B .ih B ) = ( if ( B e. ~H , B , 0h ) .ih if ( B e. ~H , B , 0h ) ) )
21 17 20 oveq12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. ~H , A , 0h ) .ih B ) / ( B .ih B ) ) = ( ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) / ( if ( B e. ~H , B , 0h ) .ih if ( B e. ~H , B , 0h ) ) ) )
22 id 
 |-  ( B = if ( B e. ~H , B , 0h ) -> B = if ( B e. ~H , B , 0h ) )
23 21 22 oveq12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( ( if ( A e. ~H , A , 0h ) .ih B ) / ( B .ih B ) ) .h B ) = ( ( ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) / ( if ( B e. ~H , B , 0h ) .ih if ( B e. ~H , B , 0h ) ) ) .h if ( B e. ~H , B , 0h ) ) )
24 23 eqeq2d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( if ( A e. ~H , A , 0h ) = ( ( ( if ( A e. ~H , A , 0h ) .ih B ) / ( B .ih B ) ) .h B ) <-> if ( A e. ~H , A , 0h ) = ( ( ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) / ( if ( B e. ~H , B , 0h ) .ih if ( B e. ~H , B , 0h ) ) ) .h if ( B e. ~H , B , 0h ) ) ) )
25 16 24 bibi12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. ~H , A , 0h ) = ( ( ( if ( A e. ~H , A , 0h ) .ih B ) / ( B .ih B ) ) .h B ) ) <-> ( if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) <-> if ( A e. ~H , A , 0h ) = ( ( ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) / ( if ( B e. ~H , B , 0h ) .ih if ( B e. ~H , B , 0h ) ) ) .h if ( B e. ~H , B , 0h ) ) ) ) )
26 12 25 imbi12d 
 |-  ( B = if ( B e. ~H , B , 0h ) -> ( ( B =/= 0h -> ( if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { B } ) ) <-> if ( A e. ~H , A , 0h ) = ( ( ( if ( A e. ~H , A , 0h ) .ih B ) / ( B .ih B ) ) .h B ) ) ) <-> ( if ( B e. ~H , B , 0h ) =/= 0h -> ( if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) <-> if ( A e. ~H , A , 0h ) = ( ( ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) / ( if ( B e. ~H , B , 0h ) .ih if ( B e. ~H , B , 0h ) ) ) .h if ( B e. ~H , B , 0h ) ) ) ) ) )
27 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
28 ifhvhv0 
 |-  if ( B e. ~H , B , 0h ) e. ~H
29 27 28 h1de2bi 
 |-  ( if ( B e. ~H , B , 0h ) =/= 0h -> ( if ( A e. ~H , A , 0h ) e. ( _|_ ` ( _|_ ` { if ( B e. ~H , B , 0h ) } ) ) <-> if ( A e. ~H , A , 0h ) = ( ( ( if ( A e. ~H , A , 0h ) .ih if ( B e. ~H , B , 0h ) ) / ( if ( B e. ~H , B , 0h ) .ih if ( B e. ~H , B , 0h ) ) ) .h if ( B e. ~H , B , 0h ) ) ) )
30 11 26 29 dedth2h 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( B =/= 0h -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) ) )
31 30 3impia 
 |-  ( ( A e. ~H /\ B e. ~H /\ B =/= 0h ) -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) )
32 3 31 bitrd 
 |-  ( ( A e. ~H /\ B e. ~H /\ B =/= 0h ) -> ( A e. ( span ` { B } ) <-> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) )