Metamath Proof Explorer

Theorem lkrlspeqN

Description: Condition for colinear functionals to have equal kernels. (Contributed by NM, 20-Mar-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lkrlspeq.f 
|- F = ( LFnl ` W )
lkrlspeq.l 
|- L = ( LKer ` W )
lkrlspeq.d 
|- D = ( LDual ` W )
lkrlspeq.o 
|- .0. = ( 0g ` D )
lkrlspeq.j 
|- N = ( LSpan ` D )
lkrlspeq.w 
|- ( ph -> W e. LVec )
lkrlspeq.h 
|- ( ph -> H e. F )
lkrlspeq.g 
|- ( ph -> G e. ( ( N ` { H } ) \ { .0. } ) )
Assertion lkrlspeqN 
|- ( ph -> ( L ` G ) = ( L ` H ) )

Proof

Step Hyp Ref Expression
1 lkrlspeq.f 
 |-  F = ( LFnl ` W )
2 lkrlspeq.l 
 |-  L = ( LKer ` W )
3 lkrlspeq.d 
 |-  D = ( LDual ` W )
4 lkrlspeq.o 
 |-  .0. = ( 0g ` D )
5 lkrlspeq.j 
 |-  N = ( LSpan ` D )
6 lkrlspeq.w 
 |-  ( ph -> W e. LVec )
7 lkrlspeq.h 
 |-  ( ph -> H e. F )
8 lkrlspeq.g 
 |-  ( ph -> G e. ( ( N ` { H } ) \ { .0. } ) )
9 8 eldifad 
 |-  ( ph -> G e. ( N ` { H } ) )
10 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
11 6 10 syl 
 |-  ( ph -> W e. LMod )
12 3 11 lduallmod 
 |-  ( ph -> D e. LMod )
13 eqid 
 |-  ( Base ` D ) = ( Base ` D )
14 1 3 13 6 7 ldualelvbase 
 |-  ( ph -> H e. ( Base ` D ) )
15 eqid 
 |-  ( Scalar ` D ) = ( Scalar ` D )
16 eqid 
 |-  ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` D ) )
17 eqid 
 |-  ( .s ` D ) = ( .s ` D )
18 15 16 13 17 5 lspsnel 
 |-  ( ( D e. LMod /\ H e. ( Base ` D ) ) -> ( G e. ( N ` { H } ) <-> E. k e. ( Base ` ( Scalar ` D ) ) G = ( k ( .s ` D ) H ) ) )
19 12 14 18 syl2anc 
 |-  ( ph -> ( G e. ( N ` { H } ) <-> E. k e. ( Base ` ( Scalar ` D ) ) G = ( k ( .s ` D ) H ) ) )
20 9 19 mpbid 
 |-  ( ph -> E. k e. ( Base ` ( Scalar ` D ) ) G = ( k ( .s ` D ) H ) )
21 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
22 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
23 21 22 3 15 16 6 ldualsbase 
 |-  ( ph -> ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` W ) ) )
24 23 rexeqdv 
 |-  ( ph -> ( E. k e. ( Base ` ( Scalar ` D ) ) G = ( k ( .s ` D ) H ) <-> E. k e. ( Base ` ( Scalar ` W ) ) G = ( k ( .s ` D ) H ) ) )
25 20 24 mpbid 
 |-  ( ph -> E. k e. ( Base ` ( Scalar ` W ) ) G = ( k ( .s ` D ) H ) )
26 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
27 6 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> W e. LVec )
28 simp2 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> k e. ( Base ` ( Scalar ` W ) ) )
29 simp3 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> G = ( k ( .s ` D ) H ) )
30 eldifsni 
 |-  ( G e. ( ( N ` { H } ) \ { .0. } ) -> G =/= .0. )
31 8 30 syl 
 |-  ( ph -> G =/= .0. )
32 31 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> G =/= .0. )
33 29 32 eqnetrrd 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( k ( .s ` D ) H ) =/= .0. )
34 eqid 
 |-  ( 0g ` ( Scalar ` D ) ) = ( 0g ` ( Scalar ` D ) )
35 21 26 3 15 34 11 ldual0 
 |-  ( ph -> ( 0g ` ( Scalar ` D ) ) = ( 0g ` ( Scalar ` W ) ) )
36 35 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( 0g ` ( Scalar ` D ) ) = ( 0g ` ( Scalar ` W ) ) )
37 36 eqeq2d 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( k = ( 0g ` ( Scalar ` D ) ) <-> k = ( 0g ` ( Scalar ` W ) ) ) )
38 orc 
 |-  ( k = ( 0g ` ( Scalar ` D ) ) -> ( k = ( 0g ` ( Scalar ` D ) ) \/ H = .0. ) )
39 37 38 syl6bir 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( k = ( 0g ` ( Scalar ` W ) ) -> ( k = ( 0g ` ( Scalar ` D ) ) \/ H = .0. ) ) )
40 3 6 lduallvec 
 |-  ( ph -> D e. LVec )
41 40 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> D e. LVec )
42 23 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` W ) ) )
43 28 42 eleqtrrd 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> k e. ( Base ` ( Scalar ` D ) ) )
44 14 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> H e. ( Base ` D ) )
45 13 17 15 16 34 4 41 43 44 lvecvs0or 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( ( k ( .s ` D ) H ) = .0. <-> ( k = ( 0g ` ( Scalar ` D ) ) \/ H = .0. ) ) )
46 39 45 sylibrd 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( k = ( 0g ` ( Scalar ` W ) ) -> ( k ( .s ` D ) H ) = .0. ) )
47 46 necon3d 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( ( k ( .s ` D ) H ) =/= .0. -> k =/= ( 0g ` ( Scalar ` W ) ) ) )
48 33 47 mpd 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> k =/= ( 0g ` ( Scalar ` W ) ) )
49 eldifsn 
 |-  ( k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) <-> ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) )
50 28 48 49 sylanbrc 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) )
51 7 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> H e. F )
52 21 22 26 1 2 3 17 27 50 51 29 lkreqN 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( L ` G ) = ( L ` H ) )
53 52 rexlimdv3a 
 |-  ( ph -> ( E. k e. ( Base ` ( Scalar ` W ) ) G = ( k ( .s ` D ) H ) -> ( L ` G ) = ( L ` H ) ) )
54 25 53 mpd 
 |-  ( ph -> ( L ` G ) = ( L ` H ) )