Step |
Hyp |
Ref |
Expression |
1 |
|
lfl1dim.v |
|- V = ( Base ` W ) |
2 |
|
lfl1dim.d |
|- D = ( Scalar ` W ) |
3 |
|
lfl1dim.f |
|- F = ( LFnl ` W ) |
4 |
|
lfl1dim.l |
|- L = ( LKer ` W ) |
5 |
|
lfl1dim.k |
|- K = ( Base ` D ) |
6 |
|
lfl1dim.t |
|- .x. = ( .r ` D ) |
7 |
|
lfl1dim.w |
|- ( ph -> W e. LVec ) |
8 |
|
lfl1dim.g |
|- ( ph -> G e. F ) |
9 |
|
df-rab |
|- { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) } |
10 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
11 |
7 10
|
syl |
|- ( ph -> W e. LMod ) |
12 |
|
eqid |
|- ( 0g ` D ) = ( 0g ` D ) |
13 |
2 5 12
|
lmod0cl |
|- ( W e. LMod -> ( 0g ` D ) e. K ) |
14 |
11 13
|
syl |
|- ( ph -> ( 0g ` D ) e. K ) |
15 |
14
|
ad2antrr |
|- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( 0g ` D ) e. K ) |
16 |
|
simpr |
|- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> g = ( V X. { ( 0g ` D ) } ) ) |
17 |
11
|
ad2antrr |
|- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> W e. LMod ) |
18 |
8
|
ad2antrr |
|- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> G e. F ) |
19 |
1 2 3 5 6 12 17 18
|
lfl0sc |
|- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( G oF .x. ( V X. { ( 0g ` D ) } ) ) = ( V X. { ( 0g ` D ) } ) ) |
20 |
16 19
|
eqtr4d |
|- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> g = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) |
21 |
|
sneq |
|- ( k = ( 0g ` D ) -> { k } = { ( 0g ` D ) } ) |
22 |
21
|
xpeq2d |
|- ( k = ( 0g ` D ) -> ( V X. { k } ) = ( V X. { ( 0g ` D ) } ) ) |
23 |
22
|
oveq2d |
|- ( k = ( 0g ` D ) -> ( G oF .x. ( V X. { k } ) ) = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) |
24 |
23
|
rspceeqv |
|- ( ( ( 0g ` D ) e. K /\ g = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) |
25 |
15 20 24
|
syl2anc |
|- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) |
26 |
25
|
a1d |
|- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) |
27 |
14
|
ad3antrrr |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( 0g ` D ) e. K ) |
28 |
11
|
ad3antrrr |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> W e. LMod ) |
29 |
|
simpllr |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g e. F ) |
30 |
1 3 4 28 29
|
lkrssv |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( L ` g ) C_ V ) |
31 |
11
|
adantr |
|- ( ( ph /\ g e. F ) -> W e. LMod ) |
32 |
8
|
adantr |
|- ( ( ph /\ g e. F ) -> G e. F ) |
33 |
2 12 1 3 4
|
lkr0f |
|- ( ( W e. LMod /\ G e. F ) -> ( ( L ` G ) = V <-> G = ( V X. { ( 0g ` D ) } ) ) ) |
34 |
31 32 33
|
syl2anc |
|- ( ( ph /\ g e. F ) -> ( ( L ` G ) = V <-> G = ( V X. { ( 0g ` D ) } ) ) ) |
35 |
34
|
biimpar |
|- ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( L ` G ) = V ) |
36 |
35
|
sseq1d |
|- ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> V C_ ( L ` g ) ) ) |
37 |
36
|
biimpa |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> V C_ ( L ` g ) ) |
38 |
30 37
|
eqssd |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( L ` g ) = V ) |
39 |
2 12 1 3 4
|
lkr0f |
|- ( ( W e. LMod /\ g e. F ) -> ( ( L ` g ) = V <-> g = ( V X. { ( 0g ` D ) } ) ) ) |
40 |
28 29 39
|
syl2anc |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( ( L ` g ) = V <-> g = ( V X. { ( 0g ` D ) } ) ) ) |
41 |
38 40
|
mpbid |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g = ( V X. { ( 0g ` D ) } ) ) |
42 |
8
|
ad3antrrr |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> G e. F ) |
43 |
1 2 3 5 6 12 28 42
|
lfl0sc |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( G oF .x. ( V X. { ( 0g ` D ) } ) ) = ( V X. { ( 0g ` D ) } ) ) |
44 |
41 43
|
eqtr4d |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g = ( G oF .x. ( V X. { ( 0g ` D ) } ) ) ) |
45 |
27 44 24
|
syl2anc |
|- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) |
46 |
45
|
ex |
|- ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) |
47 |
|
eqid |
|- ( LSHyp ` W ) = ( LSHyp ` W ) |
48 |
7
|
ad2antrr |
|- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> W e. LVec ) |
49 |
8
|
ad2antrr |
|- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> G e. F ) |
50 |
|
simprr |
|- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> G =/= ( V X. { ( 0g ` D ) } ) ) |
51 |
1 2 12 47 3 4
|
lkrshp |
|- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> ( L ` G ) e. ( LSHyp ` W ) ) |
52 |
48 49 50 51
|
syl3anc |
|- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( L ` G ) e. ( LSHyp ` W ) ) |
53 |
|
simplr |
|- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> g e. F ) |
54 |
|
simprl |
|- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> g =/= ( V X. { ( 0g ` D ) } ) ) |
55 |
1 2 12 47 3 4
|
lkrshp |
|- ( ( W e. LVec /\ g e. F /\ g =/= ( V X. { ( 0g ` D ) } ) ) -> ( L ` g ) e. ( LSHyp ` W ) ) |
56 |
48 53 54 55
|
syl3anc |
|- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( L ` g ) e. ( LSHyp ` W ) ) |
57 |
47 48 52 56
|
lshpcmp |
|- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> ( L ` G ) = ( L ` g ) ) ) |
58 |
7
|
ad3antrrr |
|- ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> W e. LVec ) |
59 |
8
|
ad3antrrr |
|- ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> G e. F ) |
60 |
|
simpllr |
|- ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> g e. F ) |
61 |
|
simpr |
|- ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> ( L ` G ) = ( L ` g ) ) |
62 |
2 5 6 1 3 4
|
eqlkr2 |
|- ( ( W e. LVec /\ ( G e. F /\ g e. F ) /\ ( L ` G ) = ( L ` g ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) |
63 |
58 59 60 61 62
|
syl121anc |
|- ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) |
64 |
63
|
ex |
|- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( ( L ` G ) = ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) |
65 |
57 64
|
sylbid |
|- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) |
66 |
26 46 65
|
pm2.61da2ne |
|- ( ( ph /\ g e. F ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) |
67 |
7
|
ad2antrr |
|- ( ( ( ph /\ g e. F ) /\ k e. K ) -> W e. LVec ) |
68 |
8
|
ad2antrr |
|- ( ( ( ph /\ g e. F ) /\ k e. K ) -> G e. F ) |
69 |
|
simpr |
|- ( ( ( ph /\ g e. F ) /\ k e. K ) -> k e. K ) |
70 |
1 2 5 6 3 4 67 68 69
|
lkrscss |
|- ( ( ( ph /\ g e. F ) /\ k e. K ) -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) ) |
71 |
70
|
ex |
|- ( ( ph /\ g e. F ) -> ( k e. K -> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) ) ) |
72 |
|
fveq2 |
|- ( g = ( G oF .x. ( V X. { k } ) ) -> ( L ` g ) = ( L ` ( G oF .x. ( V X. { k } ) ) ) ) |
73 |
72
|
sseq2d |
|- ( g = ( G oF .x. ( V X. { k } ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) ) ) |
74 |
73
|
biimprcd |
|- ( ( L ` G ) C_ ( L ` ( G oF .x. ( V X. { k } ) ) ) -> ( g = ( G oF .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) ) |
75 |
71 74
|
syl6 |
|- ( ( ph /\ g e. F ) -> ( k e. K -> ( g = ( G oF .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) ) ) |
76 |
75
|
rexlimdv |
|- ( ( ph /\ g e. F ) -> ( E. k e. K g = ( G oF .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) ) |
77 |
66 76
|
impbid |
|- ( ( ph /\ g e. F ) -> ( ( L ` G ) C_ ( L ` g ) <-> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) |
78 |
77
|
pm5.32da |
|- ( ph -> ( ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) <-> ( g e. F /\ E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) ) |
79 |
11
|
adantr |
|- ( ( ph /\ k e. K ) -> W e. LMod ) |
80 |
8
|
adantr |
|- ( ( ph /\ k e. K ) -> G e. F ) |
81 |
|
simpr |
|- ( ( ph /\ k e. K ) -> k e. K ) |
82 |
1 2 5 6 3 79 80 81
|
lflvscl |
|- ( ( ph /\ k e. K ) -> ( G oF .x. ( V X. { k } ) ) e. F ) |
83 |
|
eleq1a |
|- ( ( G oF .x. ( V X. { k } ) ) e. F -> ( g = ( G oF .x. ( V X. { k } ) ) -> g e. F ) ) |
84 |
82 83
|
syl |
|- ( ( ph /\ k e. K ) -> ( g = ( G oF .x. ( V X. { k } ) ) -> g e. F ) ) |
85 |
84
|
pm4.71rd |
|- ( ( ph /\ k e. K ) -> ( g = ( G oF .x. ( V X. { k } ) ) <-> ( g e. F /\ g = ( G oF .x. ( V X. { k } ) ) ) ) ) |
86 |
85
|
rexbidva |
|- ( ph -> ( E. k e. K g = ( G oF .x. ( V X. { k } ) ) <-> E. k e. K ( g e. F /\ g = ( G oF .x. ( V X. { k } ) ) ) ) ) |
87 |
|
r19.42v |
|- ( E. k e. K ( g e. F /\ g = ( G oF .x. ( V X. { k } ) ) ) <-> ( g e. F /\ E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) |
88 |
86 87
|
bitr2di |
|- ( ph -> ( ( g e. F /\ E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) <-> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) |
89 |
78 88
|
bitrd |
|- ( ph -> ( ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) <-> E. k e. K g = ( G oF .x. ( V X. { k } ) ) ) ) |
90 |
89
|
abbidv |
|- ( ph -> { g | ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) } = { g | E. k e. K g = ( G oF .x. ( V X. { k } ) ) } ) |
91 |
9 90
|
syl5eq |
|- ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | E. k e. K g = ( G oF .x. ( V X. { k } ) ) } ) |