This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ellspsn 
 |-  ( ( 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 20 23 rexeqtrdv 
 |-  ( ph -> E. k e. ( Base ` ( Scalar ` W ) ) G = ( k ( .s ` D ) H ) )
25 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
26 6 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> W e. LVec )
27 simp2 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> k e. ( Base ` ( Scalar ` W ) ) )
28 simp3 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> G = ( k ( .s ` D ) H ) )
29 eldifsni 
 |-  ( G e. ( ( N ` { H } ) \ { .0. } ) -> G =/= .0. )
30 8 29 syl 
 |-  ( ph -> G =/= .0. )
31 30 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> G =/= .0. )
32 28 31 eqnetrrd 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( k ( .s ` D ) H ) =/= .0. )
33 eqid 
 |-  ( 0g ` ( Scalar ` D ) ) = ( 0g ` ( Scalar ` D ) )
34 21 25 3 15 33 11 ldual0 
 |-  ( ph -> ( 0g ` ( Scalar ` D ) ) = ( 0g ` ( Scalar ` W ) ) )
35 34 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( 0g ` ( Scalar ` D ) ) = ( 0g ` ( Scalar ` W ) ) )
36 35 eqeq2d 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( k = ( 0g ` ( Scalar ` D ) ) <-> k = ( 0g ` ( Scalar ` W ) ) ) )
37 orc 
 |-  ( k = ( 0g ` ( Scalar ` D ) ) -> ( k = ( 0g ` ( Scalar ` D ) ) \/ H = .0. ) )
38 36 37 biimtrrdi 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( k = ( 0g ` ( Scalar ` W ) ) -> ( k = ( 0g ` ( Scalar ` D ) ) \/ H = .0. ) ) )
39 3 6 lduallvec 
 |-  ( ph -> D e. LVec )
40 39 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> D e. LVec )
41 23 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` W ) ) )
42 27 41 eleqtrrd 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> k e. ( Base ` ( Scalar ` D ) ) )
43 14 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> H e. ( Base ` D ) )
44 13 17 15 16 33 4 40 42 43 lvecvs0or 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( ( k ( .s ` D ) H ) = .0. <-> ( k = ( 0g ` ( Scalar ` D ) ) \/ H = .0. ) ) )
45 38 44 sylibrd 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( k = ( 0g ` ( Scalar ` W ) ) -> ( k ( .s ` D ) H ) = .0. ) )
46 45 necon3d 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( ( k ( .s ` D ) H ) =/= .0. -> k =/= ( 0g ` ( Scalar ` W ) ) ) )
47 32 46 mpd 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> k =/= ( 0g ` ( Scalar ` W ) ) )
48 eldifsn 
 |-  ( k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) <-> ( k e. ( Base ` ( Scalar ` W ) ) /\ k =/= ( 0g ` ( Scalar ` W ) ) ) )
49 27 47 48 sylanbrc 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> k e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) )
50 7 3ad2ant1 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> H e. F )
51 21 22 25 1 2 3 17 26 49 50 28 lkreqN 
 |-  ( ( ph /\ k e. ( Base ` ( Scalar ` W ) ) /\ G = ( k ( .s ` D ) H ) ) -> ( L ` G ) = ( L ` H ) )
52 51 rexlimdv3a 
 |-  ( ph -> ( E. k e. ( Base ` ( Scalar ` W ) ) G = ( k ( .s ` D ) H ) -> ( L ` G ) = ( L ` H ) ) )
53 24 52 mpd 
 |-  ( ph -> ( L ` G ) = ( L ` H ) )