Metamath Proof Explorer

Theorem hdmaplkr

Description: Kernel of the vector to dual map. Line 16 in Holland95 p. 14. TODO: eliminate F hypothesis. (Contributed by NM, 9-Jun-2015)

Ref Expression
Hypotheses hdmaplkr.h 
|- H = ( LHyp ` K )
hdmaplkr.o 
|- O = ( ( ocH ` K ) ` W )
hdmaplkr.u 
|- U = ( ( DVecH ` K ) ` W )
hdmaplkr.v 
|- V = ( Base ` U )
hdmaplkr.f 
|- F = ( LFnl ` U )
hdmaplkr.y 
|- Y = ( LKer ` U )
hdmaplkr.s 
|- S = ( ( HDMap ` K ) ` W )
hdmaplkr.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmaplkr.x 
|- ( ph -> X e. V )
Assertion hdmaplkr 
|- ( ph -> ( Y ` ( S ` X ) ) = ( O ` { X } ) )

Proof

Step Hyp Ref Expression
1 hdmaplkr.h 
 |-  H = ( LHyp ` K )
2 hdmaplkr.o 
 |-  O = ( ( ocH ` K ) ` W )
3 hdmaplkr.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 hdmaplkr.v 
 |-  V = ( Base ` U )
5 hdmaplkr.f 
 |-  F = ( LFnl ` U )
6 hdmaplkr.y 
 |-  Y = ( LKer ` U )
7 hdmaplkr.s 
 |-  S = ( ( HDMap ` K ) ` W )
8 hdmaplkr.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 hdmaplkr.x 
 |-  ( ph -> X e. V )
10 fveq2 
 |-  ( X = ( 0g ` U ) -> ( S ` X ) = ( S ` ( 0g ` U ) ) )
11 10 fveq2d 
 |-  ( X = ( 0g ` U ) -> ( Y ` ( S ` X ) ) = ( Y ` ( S ` ( 0g ` U ) ) ) )
12 sneq 
 |-  ( X = ( 0g ` U ) -> { X } = { ( 0g ` U ) } )
13 12 fveq2d 
 |-  ( X = ( 0g ` U ) -> ( O ` { X } ) = ( O ` { ( 0g ` U ) } ) )
14 11 13 sseq12d 
 |-  ( X = ( 0g ` U ) -> ( ( Y ` ( S ` X ) ) C_ ( O ` { X } ) <-> ( Y ` ( S ` ( 0g ` U ) ) ) C_ ( O ` { ( 0g ` U ) } ) ) )
15 eqid 
 |-  ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
16 1 15 8 lcdlmod 
 |-  ( ph -> ( ( LCDual ` K ) ` W ) e. LMod )
17 eqid 
 |-  ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
18 1 3 4 15 17 7 8 9 hdmapcl 
 |-  ( ph -> ( S ` X ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
19 eqid 
 |-  ( LSpan ` ( ( LCDual ` K ) ` W ) ) = ( LSpan ` ( ( LCDual ` K ) ` W ) )
20 17 19 lspsnid 
 |-  ( ( ( ( LCDual ` K ) ` W ) e. LMod /\ ( S ` X ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) ) -> ( S ` X ) e. ( ( LSpan ` ( ( LCDual ` K ) ` W ) ) ` { ( S ` X ) } ) )
21 16 18 20 syl2anc 
 |-  ( ph -> ( S ` X ) e. ( ( LSpan ` ( ( LCDual ` K ) ` W ) ) ` { ( S ` X ) } ) )
22 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
23 eqid 
 |-  ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
24 1 3 4 22 15 19 23 7 8 9 hdmap10 
 |-  ( ph -> ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { X } ) ) = ( ( LSpan ` ( ( LCDual ` K ) ` W ) ) ` { ( S ` X ) } ) )
25 eqid 
 |-  ( LFnl ` U ) = ( LFnl ` U )
26 1 2 23 3 4 22 25 6 8 9 mapdsn 
 |-  ( ph -> ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { X } ) ) = { f e. ( LFnl ` U ) | ( O ` { X } ) C_ ( Y ` f ) } )
27 24 26 eqtr3d 
 |-  ( ph -> ( ( LSpan ` ( ( LCDual ` K ) ` W ) ) ` { ( S ` X ) } ) = { f e. ( LFnl ` U ) | ( O ` { X } ) C_ ( Y ` f ) } )
28 21 27 eleqtrd 
 |-  ( ph -> ( S ` X ) e. { f e. ( LFnl ` U ) | ( O ` { X } ) C_ ( Y ` f ) } )
29 1 15 17 3 25 8 18 lcdvbaselfl 
 |-  ( ph -> ( S ` X ) e. ( LFnl ` U ) )
30 fveq2 
 |-  ( f = ( S ` X ) -> ( Y ` f ) = ( Y ` ( S ` X ) ) )
31 30 sseq2d 
 |-  ( f = ( S ` X ) -> ( ( O ` { X } ) C_ ( Y ` f ) <-> ( O ` { X } ) C_ ( Y ` ( S ` X ) ) ) )
32 31 elrab3 
 |-  ( ( S ` X ) e. ( LFnl ` U ) -> ( ( S ` X ) e. { f e. ( LFnl ` U ) | ( O ` { X } ) C_ ( Y ` f ) } <-> ( O ` { X } ) C_ ( Y ` ( S ` X ) ) ) )
33 29 32 syl 
 |-  ( ph -> ( ( S ` X ) e. { f e. ( LFnl ` U ) | ( O ` { X } ) C_ ( Y ` f ) } <-> ( O ` { X } ) C_ ( Y ` ( S ` X ) ) ) )
34 28 33 mpbid 
 |-  ( ph -> ( O ` { X } ) C_ ( Y ` ( S ` X ) ) )
35 34 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( O ` { X } ) C_ ( Y ` ( S ` X ) ) )
36 eqid 
 |-  ( LSHyp ` U ) = ( LSHyp ` U )
37 1 3 8 dvhlvec 
 |-  ( ph -> U e. LVec )
38 37 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> U e. LVec )
39 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
40 8 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
41 9 anim1i 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( X e. V /\ X =/= ( 0g ` U ) ) )
42 eldifsn 
 |-  ( X e. ( V \ { ( 0g ` U ) } ) <-> ( X e. V /\ X =/= ( 0g ` U ) ) )
43 41 42 sylibr 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> X e. ( V \ { ( 0g ` U ) } ) )
44 1 2 3 4 39 36 40 43 dochsnshp 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( O ` { X } ) e. ( LSHyp ` U ) )
45 29 adantr 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( S ` X ) e. ( LFnl ` U ) )
46 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
47 eqid 
 |-  ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )
48 eqid 
 |-  ( 0g ` ( ( LCDual ` K ) ` W ) ) = ( 0g ` ( ( LCDual ` K ) ` W ) )
49 1 3 4 46 47 15 48 8 lcd0v 
 |-  ( ph -> ( 0g ` ( ( LCDual ` K ) ` W ) ) = ( V X. { ( 0g ` ( Scalar ` U ) ) } ) )
50 49 eqeq2d 
 |-  ( ph -> ( ( S ` X ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> ( S ` X ) = ( V X. { ( 0g ` ( Scalar ` U ) ) } ) ) )
51 1 3 4 39 15 48 7 8 9 hdmapeq0 
 |-  ( ph -> ( ( S ` X ) = ( 0g ` ( ( LCDual ` K ) ` W ) ) <-> X = ( 0g ` U ) ) )
52 50 51 bitr3d 
 |-  ( ph -> ( ( S ` X ) = ( V X. { ( 0g ` ( Scalar ` U ) ) } ) <-> X = ( 0g ` U ) ) )
53 52 necon3bid 
 |-  ( ph -> ( ( S ` X ) =/= ( V X. { ( 0g ` ( Scalar ` U ) ) } ) <-> X =/= ( 0g ` U ) ) )
54 53 biimpar 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( S ` X ) =/= ( V X. { ( 0g ` ( Scalar ` U ) ) } ) )
55 4 46 47 36 25 6 lkrshp 
 |-  ( ( U e. LVec /\ ( S ` X ) e. ( LFnl ` U ) /\ ( S ` X ) =/= ( V X. { ( 0g ` ( Scalar ` U ) ) } ) ) -> ( Y ` ( S ` X ) ) e. ( LSHyp ` U ) )
56 38 45 54 55 syl3anc 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( Y ` ( S ` X ) ) e. ( LSHyp ` U ) )
57 36 38 44 56 lshpcmp 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( ( O ` { X } ) C_ ( Y ` ( S ` X ) ) <-> ( O ` { X } ) = ( Y ` ( S ` X ) ) ) )
58 35 57 mpbid 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( O ` { X } ) = ( Y ` ( S ` X ) ) )
59 eqimss2 
 |-  ( ( O ` { X } ) = ( Y ` ( S ` X ) ) -> ( Y ` ( S ` X ) ) C_ ( O ` { X } ) )
60 58 59 syl 
 |-  ( ( ph /\ X =/= ( 0g ` U ) ) -> ( Y ` ( S ` X ) ) C_ ( O ` { X } ) )
61 1 3 8 dvhlmod 
 |-  ( ph -> U e. LMod )
62 4 39 lmod0vcl 
 |-  ( U e. LMod -> ( 0g ` U ) e. V )
63 61 62 syl 
 |-  ( ph -> ( 0g ` U ) e. V )
64 1 3 4 15 17 7 8 63 hdmapcl 
 |-  ( ph -> ( S ` ( 0g ` U ) ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
65 1 15 17 3 25 8 64 lcdvbaselfl 
 |-  ( ph -> ( S ` ( 0g ` U ) ) e. ( LFnl ` U ) )
66 4 25 6 61 65 lkrssv 
 |-  ( ph -> ( Y ` ( S ` ( 0g ` U ) ) ) C_ V )
67 1 3 2 4 39 doch0 
 |-  ( ( K e. HL /\ W e. H ) -> ( O ` { ( 0g ` U ) } ) = V )
68 8 67 syl 
 |-  ( ph -> ( O ` { ( 0g ` U ) } ) = V )
69 66 68 sseqtrrd 
 |-  ( ph -> ( Y ` ( S ` ( 0g ` U ) ) ) C_ ( O ` { ( 0g ` U ) } ) )
70 14 60 69 pm2.61ne 
 |-  ( ph -> ( Y ` ( S ` X ) ) C_ ( O ` { X } ) )
71 70 34 eqssd 
 |-  ( ph -> ( Y ` ( S ` X ) ) = ( O ` { X } ) )