Metamath Proof Explorer


Theorem hdmapellkr

Description: Membership in the kernel (as shown by hdmaplkr ) of the vector to dual map. Line 17 in Holland95 p. 14. (Contributed by NM, 16-Jun-2015)

Ref Expression
Hypotheses hdmapellkr.h
|- H = ( LHyp ` K )
hdmapellkr.o
|- O = ( ( ocH ` K ) ` W )
hdmapellkr.u
|- U = ( ( DVecH ` K ) ` W )
hdmapellkr.v
|- V = ( Base ` U )
hdmapellkr.r
|- R = ( Scalar ` U )
hdmapellkr.z
|- .0. = ( 0g ` R )
hdmapellkr.s
|- S = ( ( HDMap ` K ) ` W )
hdmapellkr.k
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapellkr.x
|- ( ph -> X e. V )
hdmapellkr.y
|- ( ph -> Y e. V )
Assertion hdmapellkr
|- ( ph -> ( ( ( S ` X ) ` Y ) = .0. <-> Y e. ( O ` { X } ) ) )

Proof

Step Hyp Ref Expression
1 hdmapellkr.h
 |-  H = ( LHyp ` K )
2 hdmapellkr.o
 |-  O = ( ( ocH ` K ) ` W )
3 hdmapellkr.u
 |-  U = ( ( DVecH ` K ) ` W )
4 hdmapellkr.v
 |-  V = ( Base ` U )
5 hdmapellkr.r
 |-  R = ( Scalar ` U )
6 hdmapellkr.z
 |-  .0. = ( 0g ` R )
7 hdmapellkr.s
 |-  S = ( ( HDMap ` K ) ` W )
8 hdmapellkr.k
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 hdmapellkr.x
 |-  ( ph -> X e. V )
10 hdmapellkr.y
 |-  ( ph -> Y e. V )
11 eqid
 |-  ( LFnl ` U ) = ( LFnl ` U )
12 eqid
 |-  ( LKer ` U ) = ( LKer ` U )
13 1 3 8 dvhlmod
 |-  ( ph -> U e. LMod )
14 eqid
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
15 eqid
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
16 1 3 4 14 15 7 8 9 hdmapcl
 |-  ( ph -> ( S ` X ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
17 1 14 15 3 11 8 16 lcdvbaselfl
 |-  ( ph -> ( S ` X ) e. ( LFnl ` U ) )
18 4 5 6 11 12 13 17 10 ellkr2
 |-  ( ph -> ( Y e. ( ( LKer ` U ) ` ( S ` X ) ) <-> ( ( S ` X ) ` Y ) = .0. ) )
19 1 2 3 4 11 12 7 8 9 hdmaplkr
 |-  ( ph -> ( ( LKer ` U ) ` ( S ` X ) ) = ( O ` { X } ) )
20 19 eleq2d
 |-  ( ph -> ( Y e. ( ( LKer ` U ) ` ( S ` X ) ) <-> Y e. ( O ` { X } ) ) )
21 18 20 bitr3d
 |-  ( ph -> ( ( ( S ` X ) ` Y ) = .0. <-> Y e. ( O ` { X } ) ) )