Metamath Proof Explorer

Theorem h1de2i

Description: Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 17-Jul-2001) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 h1de2.1 
 |-  A e. ~H
2 h1de2.2 
 |-  B e. ~H
3 2 2 hicli 
 |-  ( B .ih B ) e. CC
4 3 1 hvmulcli 
 |-  ( ( B .ih B ) .h A ) e. ~H
5 1 2 hicli 
 |-  ( A .ih B ) e. CC
6 5 2 hvmulcli 
 |-  ( ( A .ih B ) .h B ) e. ~H
7 his2sub 
 |-  ( ( ( ( B .ih B ) .h A ) e. ~H /\ ( ( A .ih B ) .h B ) e. ~H /\ A e. ~H ) -> ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih A ) = ( ( ( ( B .ih B ) .h A ) .ih A ) - ( ( ( A .ih B ) .h B ) .ih A ) ) )
8 4 6 1 7 mp3an 
 |-  ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih A ) = ( ( ( ( B .ih B ) .h A ) .ih A ) - ( ( ( A .ih B ) .h B ) .ih A ) )
9 ax-his3 
 |-  ( ( ( B .ih B ) e. CC /\ A e. ~H /\ A e. ~H ) -> ( ( ( B .ih B ) .h A ) .ih A ) = ( ( B .ih B ) x. ( A .ih A ) ) )
10 3 1 1 9 mp3an 
 |-  ( ( ( B .ih B ) .h A ) .ih A ) = ( ( B .ih B ) x. ( A .ih A ) )
11 1 1 hicli 
 |-  ( A .ih A ) e. CC
12 3 11 mulcomi 
 |-  ( ( B .ih B ) x. ( A .ih A ) ) = ( ( A .ih A ) x. ( B .ih B ) )
13 10 12 eqtri 
 |-  ( ( ( B .ih B ) .h A ) .ih A ) = ( ( A .ih A ) x. ( B .ih B ) )
14 ax-his3 
 |-  ( ( ( A .ih B ) e. CC /\ B e. ~H /\ A e. ~H ) -> ( ( ( A .ih B ) .h B ) .ih A ) = ( ( A .ih B ) x. ( B .ih A ) ) )
15 5 2 1 14 mp3an 
 |-  ( ( ( A .ih B ) .h B ) .ih A ) = ( ( A .ih B ) x. ( B .ih A ) )
16 13 15 oveq12i 
 |-  ( ( ( ( B .ih B ) .h A ) .ih A ) - ( ( ( A .ih B ) .h B ) .ih A ) ) = ( ( ( A .ih A ) x. ( B .ih B ) ) - ( ( A .ih B ) x. ( B .ih A ) ) )
17 8 16 eqtr2i 
 |-  ( ( ( A .ih A ) x. ( B .ih B ) ) - ( ( A .ih B ) x. ( B .ih A ) ) ) = ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih A )
18 his2sub 
 |-  ( ( ( ( B .ih B ) .h A ) e. ~H /\ ( ( A .ih B ) .h B ) e. ~H /\ B e. ~H ) -> ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih B ) = ( ( ( ( B .ih B ) .h A ) .ih B ) - ( ( ( A .ih B ) .h B ) .ih B ) ) )
19 4 6 2 18 mp3an 
 |-  ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih B ) = ( ( ( ( B .ih B ) .h A ) .ih B ) - ( ( ( A .ih B ) .h B ) .ih B ) )
20 3 5 mulcomi 
 |-  ( ( B .ih B ) x. ( A .ih B ) ) = ( ( A .ih B ) x. ( B .ih B ) )
21 ax-his3 
 |-  ( ( ( B .ih B ) e. CC /\ A e. ~H /\ B e. ~H ) -> ( ( ( B .ih B ) .h A ) .ih B ) = ( ( B .ih B ) x. ( A .ih B ) ) )
22 3 1 2 21 mp3an 
 |-  ( ( ( B .ih B ) .h A ) .ih B ) = ( ( B .ih B ) x. ( A .ih B ) )
23 ax-his3 
 |-  ( ( ( A .ih B ) e. CC /\ B e. ~H /\ B e. ~H ) -> ( ( ( A .ih B ) .h B ) .ih B ) = ( ( A .ih B ) x. ( B .ih B ) ) )
24 5 2 2 23 mp3an 
 |-  ( ( ( A .ih B ) .h B ) .ih B ) = ( ( A .ih B ) x. ( B .ih B ) )
25 20 22 24 3eqtr4i 
 |-  ( ( ( B .ih B ) .h A ) .ih B ) = ( ( ( A .ih B ) .h B ) .ih B )
26 4 2 hicli 
 |-  ( ( ( B .ih B ) .h A ) .ih B ) e. CC
27 6 2 hicli 
 |-  ( ( ( A .ih B ) .h B ) .ih B ) e. CC
28 26 27 subeq0i 
 |-  ( ( ( ( ( B .ih B ) .h A ) .ih B ) - ( ( ( A .ih B ) .h B ) .ih B ) ) = 0 <-> ( ( ( B .ih B ) .h A ) .ih B ) = ( ( ( A .ih B ) .h B ) .ih B ) )
29 25 28 mpbir 
 |-  ( ( ( ( B .ih B ) .h A ) .ih B ) - ( ( ( A .ih B ) .h B ) .ih B ) ) = 0
30 19 29 eqtri 
 |-  ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih B ) = 0
31 2 h1dei 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> ( A e. ~H /\ A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) ) )
32 1 31 mpbiran 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) <-> A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) )
33 4 6 hvsubcli 
 |-  ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) e. ~H
34 oveq2 
 |-  ( x = ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) -> ( B .ih x ) = ( B .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) )
35 34 eqeq1d 
 |-  ( x = ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) -> ( ( B .ih x ) = 0 <-> ( B .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 ) )
36 oveq2 
 |-  ( x = ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) -> ( A .ih x ) = ( A .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) )
37 36 eqeq1d 
 |-  ( x = ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) -> ( ( A .ih x ) = 0 <-> ( A .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 ) )
38 35 37 imbi12d 
 |-  ( x = ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) -> ( ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) <-> ( ( B .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 -> ( A .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 ) ) )
39 38 rspcv 
 |-  ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) e. ~H -> ( A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) -> ( ( B .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 -> ( A .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 ) ) )
40 33 39 ax-mp 
 |-  ( A. x e. ~H ( ( B .ih x ) = 0 -> ( A .ih x ) = 0 ) -> ( ( B .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 -> ( A .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 ) )
41 32 40 sylbi 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> ( ( B .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 -> ( A .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 ) )
42 orthcom 
 |-  ( ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) e. ~H /\ B e. ~H ) -> ( ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih B ) = 0 <-> ( B .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 ) )
43 33 2 42 mp2an 
 |-  ( ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih B ) = 0 <-> ( B .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 )
44 orthcom 
 |-  ( ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) e. ~H /\ A e. ~H ) -> ( ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih A ) = 0 <-> ( A .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 ) )
45 33 1 44 mp2an 
 |-  ( ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih A ) = 0 <-> ( A .ih ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) ) = 0 )
46 41 43 45 3imtr4g 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> ( ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih B ) = 0 -> ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih A ) = 0 ) )
47 30 46 mpi 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> ( ( ( ( B .ih B ) .h A ) -h ( ( A .ih B ) .h B ) ) .ih A ) = 0 )
48 17 47 syl5eq 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> ( ( ( A .ih A ) x. ( B .ih B ) ) - ( ( A .ih B ) x. ( B .ih A ) ) ) = 0 )
49 11 3 mulcli 
 |-  ( ( A .ih A ) x. ( B .ih B ) ) e. CC
50 2 1 hicli 
 |-  ( B .ih A ) e. CC
51 5 50 mulcli 
 |-  ( ( A .ih B ) x. ( B .ih A ) ) e. CC
52 49 51 subeq0i 
 |-  ( ( ( ( A .ih A ) x. ( B .ih B ) ) - ( ( A .ih B ) x. ( B .ih A ) ) ) = 0 <-> ( ( A .ih A ) x. ( B .ih B ) ) = ( ( A .ih B ) x. ( B .ih A ) ) )
53 48 52 sylib 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> ( ( A .ih A ) x. ( B .ih B ) ) = ( ( A .ih B ) x. ( B .ih A ) ) )
54 53 eqcomd 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> ( ( A .ih B ) x. ( B .ih A ) ) = ( ( A .ih A ) x. ( B .ih B ) ) )
55 1 2 bcseqi 
 |-  ( ( ( A .ih B ) x. ( B .ih A ) ) = ( ( A .ih A ) x. ( B .ih B ) ) <-> ( ( B .ih B ) .h A ) = ( ( A .ih B ) .h B ) )
56 54 55 sylib 
 |-  ( A e. ( _|_ ` ( _|_ ` { B } ) ) -> ( ( B .ih B ) .h A ) = ( ( A .ih B ) .h B ) )