Metamath Proof Explorer

Theorem hdmapevec2

Description: The inner product of the reference vector E with itself is nonzero. This shows the inner product condition in the proof of Theorem 3.6 of Holland95 p. 14 line 32, [ e , e ] =/= 0 is satisfied. TODO: remove redundant hypothesis hdmapevec.j. (Contributed by NM, 1-Jun-2015)

Ref Expression
Hypotheses hdmapevec.h 
|- H = ( LHyp ` K )
hdmapevec.e 
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmapevec.j 
|- J = ( ( HVMap ` K ) ` W )
hdmapevec.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapevec.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapevec2.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapevec2.r 
|- R = ( Scalar ` U )
hdmapevec2.i 
|- .1. = ( 1r ` R )
Assertion hdmapevec2 
|- ( ph -> ( ( S ` E ) ` E ) = .1. )

Proof

Step Hyp Ref Expression
1 hdmapevec.h 
 |-  H = ( LHyp ` K )
2 hdmapevec.e 
 |-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3 hdmapevec.j 
 |-  J = ( ( HVMap ` K ) ` W )
4 hdmapevec.s 
 |-  S = ( ( HDMap ` K ) ` W )
5 hdmapevec.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 hdmapevec2.u 
 |-  U = ( ( DVecH ` K ) ` W )
7 hdmapevec2.r 
 |-  R = ( Scalar ` U )
8 hdmapevec2.i 
 |-  .1. = ( 1r ` R )
9 1 2 3 4 5 hdmapevec 
 |-  ( ph -> ( S ` E ) = ( J ` E ) )
10 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
11 eqid 
 |-  ( Base ` U ) = ( Base ` U )
12 eqid 
 |-  ( +g ` U ) = ( +g ` U )
13 eqid 
 |-  ( .s ` U ) = ( .s ` U )
14 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
15 eqid 
 |-  ( Base ` R ) = ( Base ` R )
16 eqid 
 |-  ( Base ` K ) = ( Base ` K )
17 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
18 1 16 17 6 11 14 2 5 dvheveccl 
 |-  ( ph -> E e. ( ( Base ` U ) \ { ( 0g ` U ) } ) )
19 1 6 10 11 12 13 14 7 15 3 5 18 hvmapval 
 |-  ( ph -> ( J ` E ) = ( v e. ( Base ` U ) |-> ( iota_ k e. ( Base ` R ) E. w e. ( ( ( ocH ` K ) ` W ) ` { E } ) v = ( w ( +g ` U ) ( k ( .s ` U ) E ) ) ) ) )
20 9 19 eqtrd 
 |-  ( ph -> ( S ` E ) = ( v e. ( Base ` U ) |-> ( iota_ k e. ( Base ` R ) E. w e. ( ( ( ocH ` K ) ` W ) ` { E } ) v = ( w ( +g ` U ) ( k ( .s ` U ) E ) ) ) ) )
21 20 fveq1d 
 |-  ( ph -> ( ( S ` E ) ` E ) = ( ( v e. ( Base ` U ) |-> ( iota_ k e. ( Base ` R ) E. w e. ( ( ( ocH ` K ) ` W ) ` { E } ) v = ( w ( +g ` U ) ( k ( .s ` U ) E ) ) ) ) ` E ) )
22 eqid 
 |-  ( v e. ( Base ` U ) |-> ( iota_ k e. ( Base ` R ) E. w e. ( ( ( ocH ` K ) ` W ) ` { E } ) v = ( w ( +g ` U ) ( k ( .s ` U ) E ) ) ) ) = ( v e. ( Base ` U ) |-> ( iota_ k e. ( Base ` R ) E. w e. ( ( ( ocH ` K ) ` W ) ` { E } ) v = ( w ( +g ` U ) ( k ( .s ` U ) E ) ) ) )
23 1 10 6 11 12 13 14 7 15 8 5 18 22 dochfl1 
 |-  ( ph -> ( ( v e. ( Base ` U ) |-> ( iota_ k e. ( Base ` R ) E. w e. ( ( ( ocH ` K ) ` W ) ` { E } ) v = ( w ( +g ` U ) ( k ( .s ` U ) E ) ) ) ) ` E ) = .1. )
24 21 23 eqtrd 
 |-  ( ph -> ( ( S ` E ) ` E ) = .1. )