Metamath Proof Explorer

Theorem dihlspsnat

Description: The inverse isomorphism H of the span of a singleton is a Hilbert lattice atom. (Contributed by NM, 27-Apr-2014)

Ref Expression
Hypotheses dihlspsnat.a 
|- A = ( Atoms ` K )
dihlspsnat.h 
|- H = ( LHyp ` K )
dihlspsnat.u 
|- U = ( ( DVecH ` K ) ` W )
dihlspsnat.v 
|- V = ( Base ` U )
dihlspsnat.o 
|- .0. = ( 0g ` U )
dihlspsnat.n 
|- N = ( LSpan ` U )
dihlspsnat.i 
|- I = ( ( DIsoH ` K ) ` W )
Assertion dihlspsnat 
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> ( `' I ` ( N ` { X } ) ) e. A )

Proof

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 )