Step |
Hyp |
Ref |
Expression |
1 |
|
dihlspsnat.a |
|- A = ( Atoms ` K ) |
2 |
|
dihlspsnat.h |
|- H = ( LHyp ` K ) |
3 |
|
dihlspsnat.u |
|- U = ( ( DVecH ` K ) ` W ) |
4 |
|
dihlspsnat.v |
|- V = ( Base ` U ) |
5 |
|
dihlspsnat.o |
|- .0. = ( 0g ` U ) |
6 |
|
dihlspsnat.n |
|- N = ( LSpan ` U ) |
7 |
|
dihlspsnat.i |
|- I = ( ( DIsoH ` K ) ` W ) |
8 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
9 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
10 |
8 2 7 3 9
|
dihf11 |
|- ( ( K e. HL /\ W e. H ) -> I : ( Base ` K ) -1-1-> ( LSubSp ` U ) ) |
11 |
10
|
3ad2ant1 |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> I : ( Base ` K ) -1-1-> ( LSubSp ` U ) ) |
12 |
|
f1f1orn |
|- ( I : ( Base ` K ) -1-1-> ( LSubSp ` U ) -> I : ( Base ` K ) -1-1-onto-> ran I ) |
13 |
11 12
|
syl |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> I : ( Base ` K ) -1-1-onto-> ran I ) |
14 |
2 3 4 6 7
|
dihlsprn |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran I ) |
15 |
14
|
3adant3 |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> ( N ` { X } ) e. ran I ) |
16 |
|
f1ocnvdm |
|- ( ( I : ( Base ` K ) -1-1-onto-> ran I /\ ( N ` { X } ) e. ran I ) -> ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) ) |
17 |
13 15 16
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) ) |
18 |
|
fveq2 |
|- ( ( `' I ` ( N ` { X } ) ) = ( 0. ` K ) -> ( I ` ( `' I ` ( N ` { X } ) ) ) = ( I ` ( 0. ` K ) ) ) |
19 |
2 7
|
dihcnvid2 |
|- ( ( ( K e. HL /\ W e. H ) /\ ( N ` { X } ) e. ran I ) -> ( I ` ( `' I ` ( N ` { X } ) ) ) = ( N ` { X } ) ) |
20 |
14 19
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( I ` ( `' I ` ( N ` { X } ) ) ) = ( N ` { X } ) ) |
21 |
|
eqid |
|- ( 0. ` K ) = ( 0. ` K ) |
22 |
21 2 7 3 5
|
dih0 |
|- ( ( K e. HL /\ W e. H ) -> ( I ` ( 0. ` K ) ) = { .0. } ) |
23 |
22
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( I ` ( 0. ` K ) ) = { .0. } ) |
24 |
20 23
|
eqeq12d |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( ( I ` ( `' I ` ( N ` { X } ) ) ) = ( I ` ( 0. ` K ) ) <-> ( N ` { X } ) = { .0. } ) ) |
25 |
|
id |
|- ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) ) |
26 |
2 3 25
|
dvhlmod |
|- ( ( K e. HL /\ W e. H ) -> U e. LMod ) |
27 |
4 5 6
|
lspsneq0 |
|- ( ( U e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) ) |
28 |
26 27
|
sylan |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) ) |
29 |
24 28
|
bitrd |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( ( I ` ( `' I ` ( N ` { X } ) ) ) = ( I ` ( 0. ` K ) ) <-> X = .0. ) ) |
30 |
18 29
|
syl5ib |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( ( `' I ` ( N ` { X } ) ) = ( 0. ` K ) -> X = .0. ) ) |
31 |
30
|
necon3d |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( X =/= .0. -> ( `' I ` ( N ` { X } ) ) =/= ( 0. ` K ) ) ) |
32 |
31
|
3impia |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> ( `' I ` ( N ` { X } ) ) =/= ( 0. ` K ) ) |
33 |
|
simpll1 |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) /\ ( I ` x ) C_ ( N ` { X } ) ) -> ( K e. HL /\ W e. H ) ) |
34 |
2 3 33
|
dvhlvec |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) /\ ( I ` x ) C_ ( N ` { X } ) ) -> U e. LVec ) |
35 |
|
simplr |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) /\ ( I ` x ) C_ ( N ` { X } ) ) -> x e. ( Base ` K ) ) |
36 |
8 2 7 3 9
|
dihlss |
|- ( ( ( K e. HL /\ W e. H ) /\ x e. ( Base ` K ) ) -> ( I ` x ) e. ( LSubSp ` U ) ) |
37 |
33 35 36
|
syl2anc |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) /\ ( I ` x ) C_ ( N ` { X } ) ) -> ( I ` x ) e. ( LSubSp ` U ) ) |
38 |
|
simpll2 |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) /\ ( I ` x ) C_ ( N ` { X } ) ) -> X e. V ) |
39 |
|
simpr |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) /\ ( I ` x ) C_ ( N ` { X } ) ) -> ( I ` x ) C_ ( N ` { X } ) ) |
40 |
4 5 9 6
|
lspsnat |
|- ( ( ( U e. LVec /\ ( I ` x ) e. ( LSubSp ` U ) /\ X e. V ) /\ ( I ` x ) C_ ( N ` { X } ) ) -> ( ( I ` x ) = ( N ` { X } ) \/ ( I ` x ) = { .0. } ) ) |
41 |
34 37 38 39 40
|
syl31anc |
|- ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) /\ ( I ` x ) C_ ( N ` { X } ) ) -> ( ( I ` x ) = ( N ` { X } ) \/ ( I ` x ) = { .0. } ) ) |
42 |
41
|
ex |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( I ` x ) C_ ( N ` { X } ) -> ( ( I ` x ) = ( N ` { X } ) \/ ( I ` x ) = { .0. } ) ) ) |
43 |
|
simp1 |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> ( K e. HL /\ W e. H ) ) |
44 |
43 15 19
|
syl2anc |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> ( I ` ( `' I ` ( N ` { X } ) ) ) = ( N ` { X } ) ) |
45 |
44
|
adantr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( I ` ( `' I ` ( N ` { X } ) ) ) = ( N ` { X } ) ) |
46 |
45
|
sseq2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( I ` x ) C_ ( I ` ( `' I ` ( N ` { X } ) ) ) <-> ( I ` x ) C_ ( N ` { X } ) ) ) |
47 |
|
simpl1 |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( K e. HL /\ W e. H ) ) |
48 |
|
simpr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> x e. ( Base ` K ) ) |
49 |
17
|
adantr |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) ) |
50 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
51 |
8 50 2 7
|
dihord |
|- ( ( ( K e. HL /\ W e. H ) /\ x e. ( Base ` K ) /\ ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) ) -> ( ( I ` x ) C_ ( I ` ( `' I ` ( N ` { X } ) ) ) <-> x ( le ` K ) ( `' I ` ( N ` { X } ) ) ) ) |
52 |
47 48 49 51
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( I ` x ) C_ ( I ` ( `' I ` ( N ` { X } ) ) ) <-> x ( le ` K ) ( `' I ` ( N ` { X } ) ) ) ) |
53 |
46 52
|
bitr3d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( I ` x ) C_ ( N ` { X } ) <-> x ( le ` K ) ( `' I ` ( N ` { X } ) ) ) ) |
54 |
45
|
eqeq2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( I ` x ) = ( I ` ( `' I ` ( N ` { X } ) ) ) <-> ( I ` x ) = ( N ` { X } ) ) ) |
55 |
8 2 7
|
dih11 |
|- ( ( ( K e. HL /\ W e. H ) /\ x e. ( Base ` K ) /\ ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) ) -> ( ( I ` x ) = ( I ` ( `' I ` ( N ` { X } ) ) ) <-> x = ( `' I ` ( N ` { X } ) ) ) ) |
56 |
47 48 49 55
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( I ` x ) = ( I ` ( `' I ` ( N ` { X } ) ) ) <-> x = ( `' I ` ( N ` { X } ) ) ) ) |
57 |
54 56
|
bitr3d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( I ` x ) = ( N ` { X } ) <-> x = ( `' I ` ( N ` { X } ) ) ) ) |
58 |
47 22
|
syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( I ` ( 0. ` K ) ) = { .0. } ) |
59 |
58
|
eqeq2d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( I ` x ) = ( I ` ( 0. ` K ) ) <-> ( I ` x ) = { .0. } ) ) |
60 |
|
simpl1l |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> K e. HL ) |
61 |
|
hlop |
|- ( K e. HL -> K e. OP ) |
62 |
8 21
|
op0cl |
|- ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) ) |
63 |
60 61 62
|
3syl |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( 0. ` K ) e. ( Base ` K ) ) |
64 |
8 2 7
|
dih11 |
|- ( ( ( K e. HL /\ W e. H ) /\ x e. ( Base ` K ) /\ ( 0. ` K ) e. ( Base ` K ) ) -> ( ( I ` x ) = ( I ` ( 0. ` K ) ) <-> x = ( 0. ` K ) ) ) |
65 |
47 48 63 64
|
syl3anc |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( I ` x ) = ( I ` ( 0. ` K ) ) <-> x = ( 0. ` K ) ) ) |
66 |
59 65
|
bitr3d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( I ` x ) = { .0. } <-> x = ( 0. ` K ) ) ) |
67 |
57 66
|
orbi12d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( ( ( I ` x ) = ( N ` { X } ) \/ ( I ` x ) = { .0. } ) <-> ( x = ( `' I ` ( N ` { X } ) ) \/ x = ( 0. ` K ) ) ) ) |
68 |
42 53 67
|
3imtr3d |
|- ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) /\ x e. ( Base ` K ) ) -> ( x ( le ` K ) ( `' I ` ( N ` { X } ) ) -> ( x = ( `' I ` ( N ` { X } ) ) \/ x = ( 0. ` K ) ) ) ) |
69 |
68
|
ralrimiva |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> A. x e. ( Base ` K ) ( x ( le ` K ) ( `' I ` ( N ` { X } ) ) -> ( x = ( `' I ` ( N ` { X } ) ) \/ x = ( 0. ` K ) ) ) ) |
70 |
|
simp1l |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> K e. HL ) |
71 |
|
hlatl |
|- ( K e. HL -> K e. AtLat ) |
72 |
8 50 21 1
|
isat3 |
|- ( K e. AtLat -> ( ( `' I ` ( N ` { X } ) ) e. A <-> ( ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) /\ ( `' I ` ( N ` { X } ) ) =/= ( 0. ` K ) /\ A. x e. ( Base ` K ) ( x ( le ` K ) ( `' I ` ( N ` { X } ) ) -> ( x = ( `' I ` ( N ` { X } ) ) \/ x = ( 0. ` K ) ) ) ) ) ) |
73 |
70 71 72
|
3syl |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> ( ( `' I ` ( N ` { X } ) ) e. A <-> ( ( `' I ` ( N ` { X } ) ) e. ( Base ` K ) /\ ( `' I ` ( N ` { X } ) ) =/= ( 0. ` K ) /\ A. x e. ( Base ` K ) ( x ( le ` K ) ( `' I ` ( N ` { X } ) ) -> ( x = ( `' I ` ( N ` { X } ) ) \/ x = ( 0. ` K ) ) ) ) ) ) |
74 |
17 32 69 73
|
mpbir3and |
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> ( `' I ` ( N ` { X } ) ) e. A ) |