Metamath Proof Explorer

Theorem h1de2bi

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 19-Jul-2001) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses h1de2.1 
|- A e. ~H
h1de2.2 
|- B e. ~H
Assertion h1de2bi 
|- ( B =/= 0h -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) )

Proof

Step Hyp Ref Expression
1 h1de2.1 
 |-  A e. ~H
2 h1de2.2 
 |-  B e. ~H
3 his6 
 |-  ( B e. ~H -> ( ( B .ih B ) = 0 <-> B = 0h ) )
4 2 3 ax-mp 
 |-  ( ( B .ih B ) = 0 <-> B = 0h )
5 4 necon3bii 
 |-  ( ( B .ih B ) =/= 0 <-> B =/= 0h )
6 1 2 h1de2i 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> ( ( B .ih B ) .h A ) = ( ( A .ih B ) .h B ) )
7 6 adantl 
 |-  ( ( ( B .ih B ) =/= 0 /\ A e. ( _|_ ` ( _|_ ` { B } ) ) ) -> ( ( B .ih B ) .h A ) = ( ( A .ih B ) .h B ) )
8 7 oveq2d 
 |-  ( ( ( B .ih B ) =/= 0 /\ A e. ( _|_ ` ( _|_ ` { B } ) ) ) -> ( ( 1 / ( B .ih B ) ) .h ( ( B .ih B ) .h A ) ) = ( ( 1 / ( B .ih B ) ) .h ( ( A .ih B ) .h B ) ) )
9 2 2 hicli 
 |-  ( B .ih B ) e. CC
10 9 recclzi 
 |-  ( ( B .ih B ) =/= 0 -> ( 1 / ( B .ih B ) ) e. CC )
11 ax-hvmulass 
 |-  ( ( ( 1 / ( B .ih B ) ) e. CC /\ ( B .ih B ) e. CC /\ A e. ~H ) -> ( ( ( 1 / ( B .ih B ) ) x. ( B .ih B ) ) .h A ) = ( ( 1 / ( B .ih B ) ) .h ( ( B .ih B ) .h A ) ) )
12 9 1 11 mp3an23 
 |-  ( ( 1 / ( B .ih B ) ) e. CC -> ( ( ( 1 / ( B .ih B ) ) x. ( B .ih B ) ) .h A ) = ( ( 1 / ( B .ih B ) ) .h ( ( B .ih B ) .h A ) ) )
13 10 12 syl 
 |-  ( ( B .ih B ) =/= 0 -> ( ( ( 1 / ( B .ih B ) ) x. ( B .ih B ) ) .h A ) = ( ( 1 / ( B .ih B ) ) .h ( ( B .ih B ) .h A ) ) )
14 ax-1cn 
 |-  1 e. CC
15 14 9 divcan1zi 
 |-  ( ( B .ih B ) =/= 0 -> ( ( 1 / ( B .ih B ) ) x. ( B .ih B ) ) = 1 )
16 15 oveq1d 
 |-  ( ( B .ih B ) =/= 0 -> ( ( ( 1 / ( B .ih B ) ) x. ( B .ih B ) ) .h A ) = ( 1 .h A ) )
17 13 16 eqtr3d 
 |-  ( ( B .ih B ) =/= 0 -> ( ( 1 / ( B .ih B ) ) .h ( ( B .ih B ) .h A ) ) = ( 1 .h A ) )
18 ax-hvmulid 
 |-  ( A e. ~H -> ( 1 .h A ) = A )
19 1 18 ax-mp 
 |-  ( 1 .h A ) = A
20 17 19 eqtrdi 
 |-  ( ( B .ih B ) =/= 0 -> ( ( 1 / ( B .ih B ) ) .h ( ( B .ih B ) .h A ) ) = A )
21 20 adantr 
 |-  ( ( ( B .ih B ) =/= 0 /\ A e. ( _|_ ` ( _|_ ` { B } ) ) ) -> ( ( 1 / ( B .ih B ) ) .h ( ( B .ih B ) .h A ) ) = A )
22 8 21 eqtr3d 
 |-  ( ( ( B .ih B ) =/= 0 /\ A e. ( _|_ ` ( _|_ ` { B } ) ) ) -> ( ( 1 / ( B .ih B ) ) .h ( ( A .ih B ) .h B ) ) = A )
23 1 2 hicli 
 |-  ( A .ih B ) e. CC
24 ax-hvmulass 
 |-  ( ( ( 1 / ( B .ih B ) ) e. CC /\ ( A .ih B ) e. CC /\ B e. ~H ) -> ( ( ( 1 / ( B .ih B ) ) x. ( A .ih B ) ) .h B ) = ( ( 1 / ( B .ih B ) ) .h ( ( A .ih B ) .h B ) ) )
25 23 2 24 mp3an23 
 |-  ( ( 1 / ( B .ih B ) ) e. CC -> ( ( ( 1 / ( B .ih B ) ) x. ( A .ih B ) ) .h B ) = ( ( 1 / ( B .ih B ) ) .h ( ( A .ih B ) .h B ) ) )
26 10 25 syl 
 |-  ( ( B .ih B ) =/= 0 -> ( ( ( 1 / ( B .ih B ) ) x. ( A .ih B ) ) .h B ) = ( ( 1 / ( B .ih B ) ) .h ( ( A .ih B ) .h B ) ) )
27 mulcom 
 |-  ( ( ( 1 / ( B .ih B ) ) e. CC /\ ( A .ih B ) e. CC ) -> ( ( 1 / ( B .ih B ) ) x. ( A .ih B ) ) = ( ( A .ih B ) x. ( 1 / ( B .ih B ) ) ) )
28 10 23 27 sylancl 
 |-  ( ( B .ih B ) =/= 0 -> ( ( 1 / ( B .ih B ) ) x. ( A .ih B ) ) = ( ( A .ih B ) x. ( 1 / ( B .ih B ) ) ) )
29 23 9 divreczi 
 |-  ( ( B .ih B ) =/= 0 -> ( ( A .ih B ) / ( B .ih B ) ) = ( ( A .ih B ) x. ( 1 / ( B .ih B ) ) ) )
30 28 29 eqtr4d 
 |-  ( ( B .ih B ) =/= 0 -> ( ( 1 / ( B .ih B ) ) x. ( A .ih B ) ) = ( ( A .ih B ) / ( B .ih B ) ) )
31 30 oveq1d 
 |-  ( ( B .ih B ) =/= 0 -> ( ( ( 1 / ( B .ih B ) ) x. ( A .ih B ) ) .h B ) = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) )
32 26 31 eqtr3d 
 |-  ( ( B .ih B ) =/= 0 -> ( ( 1 / ( B .ih B ) ) .h ( ( A .ih B ) .h B ) ) = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) )
33 32 adantr 
 |-  ( ( ( B .ih B ) =/= 0 /\ A e. ( _|_ ` ( _|_ ` { B } ) ) ) -> ( ( 1 / ( B .ih B ) ) .h ( ( A .ih B ) .h B ) ) = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) )
34 22 33 eqtr3d 
 |-  ( ( ( B .ih B ) =/= 0 /\ A e. ( _|_ ` ( _|_ ` { B } ) ) ) -> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) )
35 34 ex 
 |-  ( ( B .ih B ) =/= 0 -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) )
36 23 9 divclzi 
 |-  ( ( B .ih B ) =/= 0 -> ( ( A .ih B ) / ( B .ih B ) ) e. CC )
37 2 elexi 
 |-  B e. _V
38 37 snss 
 |-  ( B e. ~H <-> { B } C_ ~H )
39 2 38 mpbi 
 |-  { B } C_ ~H
40 occl 
 |-  ( { B } C_ ~H -> ( _|_ ` { B } ) e. CH )
41 39 40 ax-mp 
 |-  ( _|_ ` { B } ) e. CH
42 41 choccli 
 |-  ( _|_ ` ( _|_ ` { B } ) ) e. CH
43 42 chshii 
 |-  ( _|_ ` ( _|_ ` { B } ) ) e. SH
44 h1did 
 |-  ( B e. ~H -> B e. ( _|_ ` ( _|_ ` { B } ) ) )
45 2 44 ax-mp 
 |-  B e. ( _|_ ` ( _|_ ` { B } ) )
46 shmulcl 
 |-  ( ( ( _|_ ` ( _|_ ` { B } ) ) e. SH /\ ( ( A .ih B ) / ( B .ih B ) ) e. CC /\ B e. ( _|_ ` ( _|_ ` { B } ) ) ) -> ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) e. ( _|_ ` ( _|_ ` { B } ) ) )
47 43 45 46 mp3an13 
 |-  ( ( ( A .ih B ) / ( B .ih B ) ) e. CC -> ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) e. ( _|_ ` ( _|_ ` { B } ) ) )
48 36 47 syl 
 |-  ( ( B .ih B ) =/= 0 -> ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) e. ( _|_ ` ( _|_ ` { B } ) ) )
49 eleq1 
 |-  ( A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) e. ( _|_ ` ( _|_ ` { B } ) ) ) )
50 48 49 syl5ibrcom 
 |-  ( ( B .ih B ) =/= 0 -> ( A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) -> A e. ( _|_ ` ( _|_ ` { B } ) ) ) )
51 35 50 impbid 
 |-  ( ( B .ih B ) =/= 0 -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) )
52 5 51 sylbir 
 |-  ( B =/= 0h -> ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> A = ( ( ( A .ih B ) / ( B .ih B ) ) .h B ) ) )