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
dih1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dih1.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dih1.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dih1.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
Assertion dih1

Proof

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