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