Metamath Proof Explorer

Theorem lkreqN

Description: Proportional functionals have equal kernels. (Contributed by NM, 28-Mar-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lkreq.s 
|- S = ( Scalar ` W )
lkreq.r 
|- R = ( Base ` S )
lkreq.o 
|- .0. = ( 0g ` S )
lkreq.f 
|- F = ( LFnl ` W )
lkreq.k 
|- K = ( LKer ` W )
lkreq.d 
|- D = ( LDual ` W )
lkreq.t 
|- .x. = ( .s ` D )
lkreq.w 
|- ( ph -> W e. LVec )
lkreq.a 
|- ( ph -> A e. ( R \ { .0. } ) )
lkreq.h 
|- ( ph -> H e. F )
lkreq.g 
|- ( ph -> G = ( A .x. H ) )
Assertion lkreqN 
|- ( ph -> ( K ` G ) = ( K ` H ) )

Proof

Step Hyp Ref Expression
1 lkreq.s 
 |-  S = ( Scalar ` W )
2 lkreq.r 
 |-  R = ( Base ` S )
3 lkreq.o 
 |-  .0. = ( 0g ` S )
4 lkreq.f 
 |-  F = ( LFnl ` W )
5 lkreq.k 
 |-  K = ( LKer ` W )
6 lkreq.d 
 |-  D = ( LDual ` W )
7 lkreq.t 
 |-  .x. = ( .s ` D )
8 lkreq.w 
 |-  ( ph -> W e. LVec )
9 lkreq.a 
 |-  ( ph -> A e. ( R \ { .0. } ) )
10 lkreq.h 
 |-  ( ph -> H e. F )
11 lkreq.g 
 |-  ( ph -> G = ( A .x. H ) )
12 11 eqeq1d 
 |-  ( ph -> ( G = ( 0g ` D ) <-> ( A .x. H ) = ( 0g ` D ) ) )
13 eqid 
 |-  ( Base ` D ) = ( Base ` D )
14 eqid 
 |-  ( Scalar ` D ) = ( Scalar ` D )
15 eqid 
 |-  ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` D ) )
16 eqid 
 |-  ( 0g ` ( Scalar ` D ) ) = ( 0g ` ( Scalar ` D ) )
17 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
18 6 8 lduallvec 
 |-  ( ph -> D e. LVec )
19 9 eldifad 
 |-  ( ph -> A e. R )
20 1 2 6 14 15 8 ldualsbase 
 |-  ( ph -> ( Base ` ( Scalar ` D ) ) = R )
21 19 20 eleqtrrd 
 |-  ( ph -> A e. ( Base ` ( Scalar ` D ) ) )
22 4 6 13 8 10 ldualelvbase 
 |-  ( ph -> H e. ( Base ` D ) )
23 13 7 14 15 16 17 18 21 22 lvecvs0or 
 |-  ( ph -> ( ( A .x. H ) = ( 0g ` D ) <-> ( A = ( 0g ` ( Scalar ` D ) ) \/ H = ( 0g ` D ) ) ) )
24 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
25 8 24 syl 
 |-  ( ph -> W e. LMod )
26 1 3 6 14 16 25 ldual0 
 |-  ( ph -> ( 0g ` ( Scalar ` D ) ) = .0. )
27 26 eqeq2d 
 |-  ( ph -> ( A = ( 0g ` ( Scalar ` D ) ) <-> A = .0. ) )
28 eldifsni 
 |-  ( A e. ( R \ { .0. } ) -> A =/= .0. )
29 9 28 syl 
 |-  ( ph -> A =/= .0. )
30 29 a1d 
 |-  ( ph -> ( H =/= ( 0g ` D ) -> A =/= .0. ) )
31 30 necon4d 
 |-  ( ph -> ( A = .0. -> H = ( 0g ` D ) ) )
32 27 31 sylbid 
 |-  ( ph -> ( A = ( 0g ` ( Scalar ` D ) ) -> H = ( 0g ` D ) ) )
33 idd 
 |-  ( ph -> ( H = ( 0g ` D ) -> H = ( 0g ` D ) ) )
34 32 33 jaod 
 |-  ( ph -> ( ( A = ( 0g ` ( Scalar ` D ) ) \/ H = ( 0g ` D ) ) -> H = ( 0g ` D ) ) )
35 23 34 sylbid 
 |-  ( ph -> ( ( A .x. H ) = ( 0g ` D ) -> H = ( 0g ` D ) ) )
36 12 35 sylbid 
 |-  ( ph -> ( G = ( 0g ` D ) -> H = ( 0g ` D ) ) )
37 nne 
 |-  ( -. H =/= ( 0g ` D ) <-> H = ( 0g ` D ) )
38 36 37 imbitrrdi 
 |-  ( ph -> ( G = ( 0g ` D ) -> -. H =/= ( 0g ` D ) ) )
39 38 con3d 
 |-  ( ph -> ( -. -. H =/= ( 0g ` D ) -> -. G = ( 0g ` D ) ) )
40 39 orrd 
 |-  ( ph -> ( -. H =/= ( 0g ` D ) \/ -. G = ( 0g ` D ) ) )
41 ianor 
 |-  ( -. ( H =/= ( 0g ` D ) /\ G = ( 0g ` D ) ) <-> ( -. H =/= ( 0g ` D ) \/ -. G = ( 0g ` D ) ) )
42 40 41 sylibr 
 |-  ( ph -> -. ( H =/= ( 0g ` D ) /\ G = ( 0g ` D ) ) )
43 4 1 2 6 7 25 19 10 ldualvscl 
 |-  ( ph -> ( A .x. H ) e. F )
44 11 43 eqeltrd 
 |-  ( ph -> G e. F )
45 4 5 6 17 8 10 44 lkrpssN 
 |-  ( ph -> ( ( K ` H ) C. ( K ` G ) <-> ( H =/= ( 0g ` D ) /\ G = ( 0g ` D ) ) ) )
46 df-pss 
 |-  ( ( K ` H ) C. ( K ` G ) <-> ( ( K ` H ) C_ ( K ` G ) /\ ( K ` H ) =/= ( K ` G ) ) )
47 45 46 bitr3di 
 |-  ( ph -> ( ( H =/= ( 0g ` D ) /\ G = ( 0g ` D ) ) <-> ( ( K ` H ) C_ ( K ` G ) /\ ( K ` H ) =/= ( K ` G ) ) ) )
48 1 2 4 5 6 7 8 10 19 lkrss 
 |-  ( ph -> ( K ` H ) C_ ( K ` ( A .x. H ) ) )
49 11 fveq2d 
 |-  ( ph -> ( K ` G ) = ( K ` ( A .x. H ) ) )
50 48 49 sseqtrrd 
 |-  ( ph -> ( K ` H ) C_ ( K ` G ) )
51 50 biantrurd 
 |-  ( ph -> ( ( K ` H ) =/= ( K ` G ) <-> ( ( K ` H ) C_ ( K ` G ) /\ ( K ` H ) =/= ( K ` G ) ) ) )
52 47 51 bitr4d 
 |-  ( ph -> ( ( H =/= ( 0g ` D ) /\ G = ( 0g ` D ) ) <-> ( K ` H ) =/= ( K ` G ) ) )
53 52 necon2bbid 
 |-  ( ph -> ( ( K ` H ) = ( K ` G ) <-> -. ( H =/= ( 0g ` D ) /\ G = ( 0g ` D ) ) ) )
54 42 53 mpbird 
 |-  ( ph -> ( K ` H ) = ( K ` G ) )
55 54 eqcomd 
 |-  ( ph -> ( K ` G ) = ( K ` H ) )