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