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