Metamath Proof Explorer

Theorem dih1

Description: The value of isomorphism H at the lattice unity is the set of all vectors. (Contributed by NM, 13-Mar-2014)

Ref Expression
Hypotheses dih1.m 
|- .1. = ( 1. ` K )
dih1.h 
|- H = ( LHyp ` K )
dih1.i 
|- I = ( ( DIsoH ` K ) ` W )
dih1.u 
|- U = ( ( DVecH ` K ) ` W )
dih1.v 
|- V = ( Base ` U )
Assertion dih1 
|- ( ( K e. HL /\ W e. H ) -> ( I ` .1. ) = V )

Proof

Step Hyp Ref Expression
1 dih1.m 
 |-  .1. = ( 1. ` K )
2 dih1.h 
 |-  H = ( LHyp ` K )
3 dih1.i 
 |-  I = ( ( DIsoH ` K ) ` W )
4 dih1.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dih1.v 
 |-  V = ( Base ` U )
6 2 3 dihvalrel 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` .1. ) )
7 relxp 
 |-  Rel ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) )
8 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
9 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
10 2 8 9 4 5 dvhvbase 
 |-  ( ( K e. HL /\ W e. H ) -> V = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
11 10 releqd 
 |-  ( ( K e. HL /\ W e. H ) -> ( Rel V <-> Rel ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) ) )
12 7 11 mpbiri 
 |-  ( ( K e. HL /\ W e. H ) -> Rel V )
13 id 
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
14 hlop 
 |-  ( K e. HL -> K e. OP )
15 14 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> K e. OP )
16 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( K e. HL /\ W e. H ) )
17 simprl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> f e. ( ( LTrn ` K ) ` W ) )
18 simprr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> s e. ( ( TEndo ` K ) ` W ) )
19 eqid 
 |-  ( le ` K ) = ( le ` K )
20 eqid 
 |-  ( oc ` K ) = ( oc ` K )
21 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
22 19 20 21 2 lhpocnel 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. ( Atoms ` K ) /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) )
23 22 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( ( ( oc ` K ) ` W ) e. ( Atoms ` K ) /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) )
24 eqid 
 |-  ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) = ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) )
25 19 21 2 8 24 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( oc ` K ) ` W ) e. ( Atoms ` K ) /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) /\ ( ( ( oc ` K ) ` W ) e. ( Atoms ` K ) /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) ) -> ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) e. ( ( LTrn ` K ) ` W ) )
26 16 23 23 25 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) e. ( ( LTrn ` K ) ` W ) )
27 2 8 9 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. ( ( TEndo ` K ) ` W ) /\ ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) e. ( ( LTrn ` K ) ` W ) ) -> ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) e. ( ( LTrn ` K ) ` W ) )
28 16 18 26 27 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) e. ( ( LTrn ` K ) ` W ) )
29 2 8 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) e. ( ( LTrn ` K ) ` W ) ) -> `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) e. ( ( LTrn ` K ) ` W ) )
30 28 29 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) e. ( ( LTrn ` K ) ` W ) )
31 2 8 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. ( ( LTrn ` K ) ` W ) /\ `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) e. ( ( LTrn ` K ) ` W ) ) -> ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) e. ( ( LTrn ` K ) ` W ) )
32 16 17 30 31 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) e. ( ( LTrn ` K ) ` W ) )
33 eqid 
 |-  ( Base ` K ) = ( Base ` K )
34 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
35 33 2 8 34 trlcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) e. ( ( LTrn ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) ) e. ( Base ` K ) )
36 32 35 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) ) e. ( Base ` K ) )
37 33 19 1 ople1 
 |-  ( ( K e. OP /\ ( ( ( trL ` K ) ` W ) ` ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) ) e. ( Base ` K ) ) -> ( ( ( trL ` K ) ` W ) ` ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) ) ( le ` K ) .1. )
38 15 36 37 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( ( ( trL ` K ) ` W ) ` ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) ) ( le ` K ) .1. )
39 38 ex 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) -> ( ( ( trL ` K ) ` W ) ` ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) ) ( le ` K ) .1. ) )
40 39 pm4.71d 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) <-> ( ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) /\ ( ( ( trL ` K ) ` W ) ` ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) ) ( le ` K ) .1. ) ) )
41 10 eleq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( <. f , s >. e. V <-> <. f , s >. e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) ) )
42 opelxp 
 |-  ( <. f , s >. e. ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) <-> ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) )
43 41 42 bitrdi 
 |-  ( ( K e. HL /\ W e. H ) -> ( <. f , s >. e. V <-> ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) )
44 14 adantr 
 |-  ( ( K e. HL /\ W e. H ) -> K e. OP )
45 33 1 op1cl 
 |-  ( K e. OP -> .1. e. ( Base ` K ) )
46 44 45 syl 
 |-  ( ( K e. HL /\ W e. H ) -> .1. e. ( Base ` K ) )
47 hlpos 
 |-  ( K e. HL -> K e. Poset )
48 47 adantr 
 |-  ( ( K e. HL /\ W e. H ) -> K e. Poset )
49 33 2 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
50 49 adantl 
 |-  ( ( K e. HL /\ W e. H ) -> W e. ( Base ` K ) )
51 eqid 
 |-  (
52 1 51 2 lhp1cvr 
 |-  ( ( K e. HL /\ W e. H ) -> W (
53 33 19 51 cvrnle 
 |-  ( ( ( K e. Poset /\ W e. ( Base ` K ) /\ .1. e. ( Base ` K ) ) /\ W (  -. .1. ( le ` K ) W )
54 48 50 46 52 53 syl31anc 
 |-  ( ( K e. HL /\ W e. H ) -> -. .1. ( le ` K ) W )
55 hlol 
 |-  ( K e. HL -> K e. OL )
56 eqid 
 |-  ( meet ` K ) = ( meet ` K )
57 33 56 1 olm12 
 |-  ( ( K e. OL /\ W e. ( Base ` K ) ) -> ( .1. ( meet ` K ) W ) = W )
58 55 49 57 syl2an 
 |-  ( ( K e. HL /\ W e. H ) -> ( .1. ( meet ` K ) W ) = W )
59 58 oveq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) ( join ` K ) ( .1. ( meet ` K ) W ) ) = ( ( ( oc ` K ) ` W ) ( join ` K ) W ) )
60 hllat 
 |-  ( K e. HL -> K e. Lat )
61 60 adantr 
 |-  ( ( K e. HL /\ W e. H ) -> K e. Lat )
62 33 20 opoccl 
 |-  ( ( K e. OP /\ W e. ( Base ` K ) ) -> ( ( oc ` K ) ` W ) e. ( Base ` K ) )
63 14 49 62 syl2an 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( oc ` K ) ` W ) e. ( Base ` K ) )
64 eqid 
 |-  ( join ` K ) = ( join ` K )
65 33 64 latjcom 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` W ) e. ( Base ` K ) /\ W e. ( Base ` K ) ) -> ( ( ( oc ` K ) ` W ) ( join ` K ) W ) = ( W ( join ` K ) ( ( oc ` K ) ` W ) ) )
66 61 63 50 65 syl3anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) ( join ` K ) W ) = ( W ( join ` K ) ( ( oc ` K ) ` W ) ) )
67 33 20 64 1 opexmid 
 |-  ( ( K e. OP /\ W e. ( Base ` K ) ) -> ( W ( join ` K ) ( ( oc ` K ) ` W ) ) = .1. )
68 14 49 67 syl2an 
 |-  ( ( K e. HL /\ W e. H ) -> ( W ( join ` K ) ( ( oc ` K ) ` W ) ) = .1. )
69 59 66 68 3eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) ( join ` K ) ( .1. ( meet ` K ) W ) ) = .1. )
70 eqid 
 |-  ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
71 vex 
 |-  f e. _V
72 vex 
 |-  s e. _V
73 33 19 64 56 21 2 70 8 34 9 3 24 71 72 dihopelvalc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( .1. e. ( Base ` K ) /\ -. .1. ( le ` K ) W ) /\ ( ( ( ( oc ` K ) ` W ) e. ( Atoms ` K ) /\ -. ( ( oc ` K ) ` W ) ( le ` K ) W ) /\ ( ( ( oc ` K ) ` W ) ( join ` K ) ( .1. ( meet ` K ) W ) ) = .1. ) ) -> ( <. f , s >. e. ( I ` .1. ) <-> ( ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) /\ ( ( ( trL ` K ) ` W ) ` ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) ) ( le ` K ) .1. ) ) )
74 13 46 54 22 69 73 syl122anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( <. f , s >. e. ( I ` .1. ) <-> ( ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) /\ ( ( ( trL ` K ) ` W ) ` ( f o. `' ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = ( ( oc ` K ) ` W ) ) ) ) ) ( le ` K ) .1. ) ) )
75 40 43 74 3bitr4rd 
 |-  ( ( K e. HL /\ W e. H ) -> ( <. f , s >. e. ( I ` .1. ) <-> <. f , s >. e. V ) )
76 75 eqrelrdv2 
 |-  ( ( ( Rel ( I ` .1. ) /\ Rel V ) /\ ( K e. HL /\ W e. H ) ) -> ( I ` .1. ) = V )
77 6 12 13 76 syl21anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` .1. ) = V )