# Metamath Proof Explorer

## Theorem hdmapinvlem2

Description: Line 28 in Baer p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015)

Ref Expression
Hypotheses hdmapinvlem1.h
|- H = ( LHyp ` K )
hdmapinvlem1.e
|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
hdmapinvlem1.o
|- O = ( ( ocH ` K ) ` W )
hdmapinvlem1.u
|- U = ( ( DVecH ` K ) ` W )
hdmapinvlem1.v
|- V = ( Base ` U )
hdmapinvlem1.r
|- R = ( Scalar ` U )
hdmapinvlem1.b
|- B = ( Base ` R )
hdmapinvlem1.t
|- .x. = ( .r ` R )
hdmapinvlem1.z
|- .0. = ( 0g ` R )
hdmapinvlem1.s
|- S = ( ( HDMap ` K ) ` W )
hdmapinvlem1.k
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapinvlem1.c
|- ( ph -> C e. ( O ` { E } ) )
Assertion hdmapinvlem2
|- ( ph -> ( ( S ` C ) ` E ) = .0. )

### Proof

Step Hyp Ref Expression
1 hdmapinvlem1.h
|-  H = ( LHyp ` K )
2 hdmapinvlem1.e
|-  E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3 hdmapinvlem1.o
|-  O = ( ( ocH ` K ) ` W )
4 hdmapinvlem1.u
|-  U = ( ( DVecH ` K ) ` W )
5 hdmapinvlem1.v
|-  V = ( Base ` U )
6 hdmapinvlem1.r
|-  R = ( Scalar ` U )
7 hdmapinvlem1.b
|-  B = ( Base ` R )
8 hdmapinvlem1.t
|-  .x. = ( .r ` R )
9 hdmapinvlem1.z
|-  .0. = ( 0g ` R )
10 hdmapinvlem1.s
|-  S = ( ( HDMap ` K ) ` W )
11 hdmapinvlem1.k
|-  ( ph -> ( K e. HL /\ W e. H ) )
12 hdmapinvlem1.c
|-  ( ph -> C e. ( O ` { E } ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 hdmapinvlem1
|-  ( ph -> ( ( S ` E ) ` C ) = .0. )
14 eqid
|-  ( Base ` K ) = ( Base ` K )
15 eqid
|-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
16 eqid
|-  ( 0g ` U ) = ( 0g ` U )
17 1 14 15 4 5 16 2 11 dvheveccl
|-  ( ph -> E e. ( V \ { ( 0g ` U ) } ) )