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

Metamath Proof Explorer

Theorem spansncol

Description: The singletons of collinear vectors have the same span. (Contributed by NM, 6-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 mulcl 
 |-  ( ( y e. CC /\ B e. CC ) -> ( y x. B ) e. CC )
2 1 ancoms 
 |-  ( ( B e. CC /\ y e. CC ) -> ( y x. B ) e. CC )
3 2 adantll 
 |-  ( ( ( A e. ~H /\ B e. CC ) /\ y e. CC ) -> ( y x. B ) e. CC )
4 ax-hvmulass 
 |-  ( ( y e. CC /\ B e. CC /\ A e. ~H ) -> ( ( y x. B ) .h A ) = ( y .h ( B .h A ) ) )
5 4 3com13 
 |-  ( ( A e. ~H /\ B e. CC /\ y e. CC ) -> ( ( y x. B ) .h A ) = ( y .h ( B .h A ) ) )
6 5 3expa 
 |-  ( ( ( A e. ~H /\ B e. CC ) /\ y e. CC ) -> ( ( y x. B ) .h A ) = ( y .h ( B .h A ) ) )
7 6 eqeq2d 
 |-  ( ( ( A e. ~H /\ B e. CC ) /\ y e. CC ) -> ( x = ( ( y x. B ) .h A ) <-> x = ( y .h ( B .h A ) ) ) )
8 7 biimprd 
 |-  ( ( ( A e. ~H /\ B e. CC ) /\ y e. CC ) -> ( x = ( y .h ( B .h A ) ) -> x = ( ( y x. B ) .h A ) ) )
9 oveq1 
 |-  ( z = ( y x. B ) -> ( z .h A ) = ( ( y x. B ) .h A ) )
10 9 rspceeqv 
 |-  ( ( ( y x. B ) e. CC /\ x = ( ( y x. B ) .h A ) ) -> E. z e. CC x = ( z .h A ) )
11 3 8 10 syl6an 
 |-  ( ( ( A e. ~H /\ B e. CC ) /\ y e. CC ) -> ( x = ( y .h ( B .h A ) ) -> E. z e. CC x = ( z .h A ) ) )
12 11 rexlimdva 
 |-  ( ( A e. ~H /\ B e. CC ) -> ( E. y e. CC x = ( y .h ( B .h A ) ) -> E. z e. CC x = ( z .h A ) ) )
13 12 3adant3 
 |-  ( ( A e. ~H /\ B e. CC /\ B =/= 0 ) -> ( E. y e. CC x = ( y .h ( B .h A ) ) -> E. z e. CC x = ( z .h A ) ) )
14 divcl 
 |-  ( ( z e. CC /\ B e. CC /\ B =/= 0 ) -> ( z / B ) e. CC )
15 14 3expb 
 |-  ( ( z e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( z / B ) e. CC )
16 15 adantlr 
 |-  ( ( ( z e. CC /\ A e. ~H ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( z / B ) e. CC )
17 simprl 
 |-  ( ( ( z e. CC /\ A e. ~H ) /\ ( B e. CC /\ B =/= 0 ) ) -> B e. CC )
18 simplr 
 |-  ( ( ( z e. CC /\ A e. ~H ) /\ ( B e. CC /\ B =/= 0 ) ) -> A e. ~H )
19 ax-hvmulass 
 |-  ( ( ( z / B ) e. CC /\ B e. CC /\ A e. ~H ) -> ( ( ( z / B ) x. B ) .h A ) = ( ( z / B ) .h ( B .h A ) ) )
20 16 17 18 19 syl3anc 
 |-  ( ( ( z e. CC /\ A e. ~H ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( ( z / B ) x. B ) .h A ) = ( ( z / B ) .h ( B .h A ) ) )
21 divcan1 
 |-  ( ( z e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( z / B ) x. B ) = z )
22 21 3expb 
 |-  ( ( z e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( z / B ) x. B ) = z )
23 22 adantlr 
 |-  ( ( ( z e. CC /\ A e. ~H ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( z / B ) x. B ) = z )
24 23 oveq1d 
 |-  ( ( ( z e. CC /\ A e. ~H ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( ( z / B ) x. B ) .h A ) = ( z .h A ) )
25 20 24 eqtr3d 
 |-  ( ( ( z e. CC /\ A e. ~H ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( z / B ) .h ( B .h A ) ) = ( z .h A ) )
26 25 eqeq2d 
 |-  ( ( ( z e. CC /\ A e. ~H ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( x = ( ( z / B ) .h ( B .h A ) ) <-> x = ( z .h A ) ) )
27 26 biimprd 
 |-  ( ( ( z e. CC /\ A e. ~H ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( x = ( z .h A ) -> x = ( ( z / B ) .h ( B .h A ) ) ) )
28 oveq1 
 |-  ( y = ( z / B ) -> ( y .h ( B .h A ) ) = ( ( z / B ) .h ( B .h A ) ) )
29 28 rspceeqv 
 |-  ( ( ( z / B ) e. CC /\ x = ( ( z / B ) .h ( B .h A ) ) ) -> E. y e. CC x = ( y .h ( B .h A ) ) )
30 16 27 29 syl6an 
 |-  ( ( ( z e. CC /\ A e. ~H ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( x = ( z .h A ) -> E. y e. CC x = ( y .h ( B .h A ) ) ) )
31 30 exp43 
 |-  ( z e. CC -> ( A e. ~H -> ( B e. CC -> ( B =/= 0 -> ( x = ( z .h A ) -> E. y e. CC x = ( y .h ( B .h A ) ) ) ) ) ) )
32 31 com4l 
 |-  ( A e. ~H -> ( B e. CC -> ( B =/= 0 -> ( z e. CC -> ( x = ( z .h A ) -> E. y e. CC x = ( y .h ( B .h A ) ) ) ) ) ) )
33 32 3imp 
 |-  ( ( A e. ~H /\ B e. CC /\ B =/= 0 ) -> ( z e. CC -> ( x = ( z .h A ) -> E. y e. CC x = ( y .h ( B .h A ) ) ) ) )
34 33 rexlimdv 
 |-  ( ( A e. ~H /\ B e. CC /\ B =/= 0 ) -> ( E. z e. CC x = ( z .h A ) -> E. y e. CC x = ( y .h ( B .h A ) ) ) )
35 13 34 impbid 
 |-  ( ( A e. ~H /\ B e. CC /\ B =/= 0 ) -> ( E. y e. CC x = ( y .h ( B .h A ) ) <-> E. z e. CC x = ( z .h A ) ) )
36 hvmulcl 
 |-  ( ( B e. CC /\ A e. ~H ) -> ( B .h A ) e. ~H )
37 36 ancoms 
 |-  ( ( A e. ~H /\ B e. CC ) -> ( B .h A ) e. ~H )
38 elspansn 
 |-  ( ( B .h A ) e. ~H -> ( x e. ( span ` { ( B .h A ) } ) <-> E. y e. CC x = ( y .h ( B .h A ) ) ) )
39 37 38 syl 
 |-  ( ( A e. ~H /\ B e. CC ) -> ( x e. ( span ` { ( B .h A ) } ) <-> E. y e. CC x = ( y .h ( B .h A ) ) ) )
40 39 3adant3 
 |-  ( ( A e. ~H /\ B e. CC /\ B =/= 0 ) -> ( x e. ( span ` { ( B .h A ) } ) <-> E. y e. CC x = ( y .h ( B .h A ) ) ) )
41 elspansn 
 |-  ( A e. ~H -> ( x e. ( span ` { A } ) <-> E. z e. CC x = ( z .h A ) ) )
42 41 3ad2ant1 
 |-  ( ( A e. ~H /\ B e. CC /\ B =/= 0 ) -> ( x e. ( span ` { A } ) <-> E. z e. CC x = ( z .h A ) ) )
43 35 40 42 3bitr4d 
 |-  ( ( A e. ~H /\ B e. CC /\ B =/= 0 ) -> ( x e. ( span ` { ( B .h A ) } ) <-> x e. ( span ` { A } ) ) )
44 43 eqrdv 
 |-  ( ( A e. ~H /\ B e. CC /\ B =/= 0 ) -> ( span ` { ( B .h A ) } ) = ( span ` { A } ) )