Metamath Proof Explorer


Theorem dih1

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

Ref Expression
Hypotheses dih1.m 1˙=1.K
dih1.h H=LHypK
dih1.i I=DIsoHKW
dih1.u U=DVecHKW
dih1.v V=BaseU
Assertion dih1 KHLWHI1˙=V

Proof

Step Hyp Ref Expression
1 dih1.m 1˙=1.K
2 dih1.h H=LHypK
3 dih1.i I=DIsoHKW
4 dih1.u U=DVecHKW
5 dih1.v V=BaseU
6 2 3 dihvalrel KHLWHRelI1˙
7 relxp RelLTrnKW×TEndoKW
8 eqid LTrnKW=LTrnKW
9 eqid TEndoKW=TEndoKW
10 2 8 9 4 5 dvhvbase KHLWHV=LTrnKW×TEndoKW
11 10 releqd KHLWHRelVRelLTrnKW×TEndoKW
12 7 11 mpbiri KHLWHRelV
13 id KHLWHKHLWH
14 hlop KHLKOP
15 14 ad2antrr KHLWHfLTrnKWsTEndoKWKOP
16 simpl KHLWHfLTrnKWsTEndoKWKHLWH
17 simprl KHLWHfLTrnKWsTEndoKWfLTrnKW
18 simprr KHLWHfLTrnKWsTEndoKWsTEndoKW
19 eqid K=K
20 eqid ocK=ocK
21 eqid AtomsK=AtomsK
22 19 20 21 2 lhpocnel KHLWHocKWAtomsK¬ocKWKW
23 22 adantr KHLWHfLTrnKWsTEndoKWocKWAtomsK¬ocKWKW
24 eqid ιgLTrnKW|gocKW=ocKW=ιgLTrnKW|gocKW=ocKW
25 19 21 2 8 24 ltrniotacl KHLWHocKWAtomsK¬ocKWKWocKWAtomsK¬ocKWKWιgLTrnKW|gocKW=ocKWLTrnKW
26 16 23 23 25 syl3anc KHLWHfLTrnKWsTEndoKWιgLTrnKW|gocKW=ocKWLTrnKW
27 2 8 9 tendocl KHLWHsTEndoKWιgLTrnKW|gocKW=ocKWLTrnKWsιgLTrnKW|gocKW=ocKWLTrnKW
28 16 18 26 27 syl3anc KHLWHfLTrnKWsTEndoKWsιgLTrnKW|gocKW=ocKWLTrnKW
29 2 8 ltrncnv KHLWHsιgLTrnKW|gocKW=ocKWLTrnKWsιgLTrnKW|gocKW=ocKW-1LTrnKW
30 28 29 syldan KHLWHfLTrnKWsTEndoKWsιgLTrnKW|gocKW=ocKW-1LTrnKW
31 2 8 ltrnco KHLWHfLTrnKWsιgLTrnKW|gocKW=ocKW-1LTrnKWfsιgLTrnKW|gocKW=ocKW-1LTrnKW
32 16 17 30 31 syl3anc KHLWHfLTrnKWsTEndoKWfsιgLTrnKW|gocKW=ocKW-1LTrnKW
33 eqid BaseK=BaseK
34 eqid trLKW=trLKW
35 33 2 8 34 trlcl KHLWHfsιgLTrnKW|gocKW=ocKW-1LTrnKWtrLKWfsιgLTrnKW|gocKW=ocKW-1BaseK
36 32 35 syldan KHLWHfLTrnKWsTEndoKWtrLKWfsιgLTrnKW|gocKW=ocKW-1BaseK
37 33 19 1 ople1 KOPtrLKWfsιgLTrnKW|gocKW=ocKW-1BaseKtrLKWfsιgLTrnKW|gocKW=ocKW-1K1˙
38 15 36 37 syl2anc KHLWHfLTrnKWsTEndoKWtrLKWfsιgLTrnKW|gocKW=ocKW-1K1˙
39 38 ex KHLWHfLTrnKWsTEndoKWtrLKWfsιgLTrnKW|gocKW=ocKW-1K1˙
40 39 pm4.71d KHLWHfLTrnKWsTEndoKWfLTrnKWsTEndoKWtrLKWfsιgLTrnKW|gocKW=ocKW-1K1˙
41 10 eleq2d KHLWHfsVfsLTrnKW×TEndoKW
42 opelxp fsLTrnKW×TEndoKWfLTrnKWsTEndoKW
43 41 42 bitrdi KHLWHfsVfLTrnKWsTEndoKW
44 14 adantr KHLWHKOP
45 33 1 op1cl KOP1˙BaseK
46 44 45 syl KHLWH1˙BaseK
47 hlpos KHLKPoset
48 47 adantr KHLWHKPoset
49 33 2 lhpbase WHWBaseK
50 49 adantl KHLWHWBaseK
51 eqid K=K
52 1 51 2 lhp1cvr KHLWHWK1˙
53 33 19 51 cvrnle KPosetWBaseK1˙BaseKWK1˙¬1˙KW
54 48 50 46 52 53 syl31anc KHLWH¬1˙KW
55 hlol KHLKOL
56 eqid meetK=meetK
57 33 56 1 olm12 KOLWBaseK1˙meetKW=W
58 55 49 57 syl2an KHLWH1˙meetKW=W
59 58 oveq2d KHLWHocKWjoinK1˙meetKW=ocKWjoinKW
60 hllat KHLKLat
61 60 adantr KHLWHKLat
62 33 20 opoccl KOPWBaseKocKWBaseK
63 14 49 62 syl2an KHLWHocKWBaseK
64 eqid joinK=joinK
65 33 64 latjcom KLatocKWBaseKWBaseKocKWjoinKW=WjoinKocKW
66 61 63 50 65 syl3anc KHLWHocKWjoinKW=WjoinKocKW
67 33 20 64 1 opexmid KOPWBaseKWjoinKocKW=1˙
68 14 49 67 syl2an KHLWHWjoinKocKW=1˙
69 59 66 68 3eqtrd KHLWHocKWjoinK1˙meetKW=1˙
70 eqid ocKW=ocKW
71 vex fV
72 vex sV
73 33 19 64 56 21 2 70 8 34 9 3 24 71 72 dihopelvalc KHLWH1˙BaseK¬1˙KWocKWAtomsK¬ocKWKWocKWjoinK1˙meetKW=1˙fsI1˙fLTrnKWsTEndoKWtrLKWfsιgLTrnKW|gocKW=ocKW-1K1˙
74 13 46 54 22 69 73 syl122anc KHLWHfsI1˙fLTrnKWsTEndoKWtrLKWfsιgLTrnKW|gocKW=ocKW-1K1˙
75 40 43 74 3bitr4rd KHLWHfsI1˙fsV
76 75 eqrelrdv2 RelI1˙RelVKHLWHI1˙=V
77 6 12 13 76 syl21anc KHLWHI1˙=V