Metamath Proof Explorer

Theorem hdmapip1

Description: Construct a proportional vector Y whose inner product with the original X equals one. (Contributed by NM, 13-Jun-2015)

Ref Expression
Hypotheses hdmapip1.h 
|- H = ( LHyp ` K )
hdmapip1.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapip1.v 
|- V = ( Base ` U )
hdmapip1.t 
|- .x. = ( .s ` U )
hdmapip1.o 
|- .0. = ( 0g ` U )
hdmapip1.r 
|- R = ( Scalar ` U )
hdmapip1.i 
|- .1. = ( 1r ` R )
hdmapip1.n 
|- N = ( invr ` R )
hdmapip1.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapip1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapip1.x 
|- ( ph -> X e. ( V \ { .0. } ) )
hdmapip1.y 
|- Y = ( ( N ` ( ( S ` X ) ` X ) ) .x. X )
Assertion hdmapip1 
|- ( ph -> ( ( S ` X ) ` Y ) = .1. )

Proof

Step Hyp Ref Expression
1 hdmapip1.h 
 |-  H = ( LHyp ` K )
2 hdmapip1.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmapip1.v 
 |-  V = ( Base ` U )
4 hdmapip1.t 
 |-  .x. = ( .s ` U )
5 hdmapip1.o 
 |-  .0. = ( 0g ` U )
6 hdmapip1.r 
 |-  R = ( Scalar ` U )
7 hdmapip1.i 
 |-  .1. = ( 1r ` R )
8 hdmapip1.n 
 |-  N = ( invr ` R )
9 hdmapip1.s 
 |-  S = ( ( HDMap ` K ) ` W )
10 hdmapip1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
11 hdmapip1.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
12 hdmapip1.y 
 |-  Y = ( ( N ` ( ( S ` X ) ` X ) ) .x. X )
13 12 fveq2i 
 |-  ( ( S ` X ) ` Y ) = ( ( S ` X ) ` ( ( N ` ( ( S ` X ) ` X ) ) .x. X ) )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 eqid 
 |-  ( .r ` R ) = ( .r ` R )
16 11 eldifad 
 |-  ( ph -> X e. V )
17 1 2 10 dvhlvec 
 |-  ( ph -> U e. LVec )
18 6 lvecdrng 
 |-  ( U e. LVec -> R e. DivRing )
19 17 18 syl 
 |-  ( ph -> R e. DivRing )
20 1 2 3 6 14 9 10 16 16 hdmapipcl 
 |-  ( ph -> ( ( S ` X ) ` X ) e. ( Base ` R ) )
21 eldifsni 
 |-  ( X e. ( V \ { .0. } ) -> X =/= .0. )
22 11 21 syl 
 |-  ( ph -> X =/= .0. )
23 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
24 1 2 3 5 6 23 9 10 16 hdmapip0 
 |-  ( ph -> ( ( ( S ` X ) ` X ) = ( 0g ` R ) <-> X = .0. ) )
25 24 necon3bid 
 |-  ( ph -> ( ( ( S ` X ) ` X ) =/= ( 0g ` R ) <-> X =/= .0. ) )
26 22 25 mpbird 
 |-  ( ph -> ( ( S ` X ) ` X ) =/= ( 0g ` R ) )
27 14 23 8 drnginvrcl 
 |-  ( ( R e. DivRing /\ ( ( S ` X ) ` X ) e. ( Base ` R ) /\ ( ( S ` X ) ` X ) =/= ( 0g ` R ) ) -> ( N ` ( ( S ` X ) ` X ) ) e. ( Base ` R ) )
28 19 20 26 27 syl3anc 
 |-  ( ph -> ( N ` ( ( S ` X ) ` X ) ) e. ( Base ` R ) )
29 1 2 3 4 6 14 15 9 10 16 16 28 hdmaplnm1 
 |-  ( ph -> ( ( S ` X ) ` ( ( N ` ( ( S ` X ) ` X ) ) .x. X ) ) = ( ( N ` ( ( S ` X ) ` X ) ) ( .r ` R ) ( ( S ` X ) ` X ) ) )
30 14 23 15 7 8 drnginvrl 
 |-  ( ( R e. DivRing /\ ( ( S ` X ) ` X ) e. ( Base ` R ) /\ ( ( S ` X ) ` X ) =/= ( 0g ` R ) ) -> ( ( N ` ( ( S ` X ) ` X ) ) ( .r ` R ) ( ( S ` X ) ` X ) ) = .1. )
31 19 20 26 30 syl3anc 
 |-  ( ph -> ( ( N ` ( ( S ` X ) ` X ) ) ( .r ` R ) ( ( S ` X ) ` X ) ) = .1. )
32 29 31 eqtrd 
 |-  ( ph -> ( ( S ` X ) ` ( ( N ` ( ( S ` X ) ` X ) ) .x. X ) ) = .1. )
33 13 32 syl5eq 
 |-  ( ph -> ( ( S ` X ) ` Y ) = .1. )