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 syl6ibr
 |-  ( 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 ) )