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 } ) ) )