Metamath Proof Explorer

Theorem dihffval

Description: The isomorphism H for a lattice K . Definition of isomorphism map in Crawley p. 122 line 3. (Contributed by NM, 28-Jan-2014)

Ref Expression
Hypotheses dihval.b ⊢B=BaseK
dihval.l ⊢≤˙=≤K
dihval.j ⊢∨˙=join⁡K
dihval.m ⊢∧˙=meet⁡K
dihval.a ⊢A=Atoms⁡K
dihval.h ⊢H=LHyp⁡K
Assertion dihffval ⊢K∈V→DIsoH⁡K=w∈H⟼x∈B⟼ifx≤˙wDIsoB⁡K⁡w⁡xιu∈LSubSp⁡DVecH⁡K⁡w|∀q∈A¬q≤˙w∧q∨˙x∧˙w=x→u=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w

Proof

Step Hyp Ref Expression
1 dihval.b ⊢B=BaseK
2 dihval.l ⊢≤˙=≤K
3 dihval.j ⊢∨˙=join⁡K
4 dihval.m ⊢∧˙=meet⁡K
5 dihval.a ⊢A=Atoms⁡K
6 dihval.h ⊢H=LHyp⁡K
7 elex ⊢K∈V→K∈V
8 fveq2 ⊢k=K→LHyp⁡k=LHyp⁡K
9 8 6 eqtr4di ⊢k=K→LHyp⁡k=H
10 fveq2 ⊢k=K→Basek=BaseK
11 10 1 eqtr4di ⊢k=K→Basek=B
12 fveq2 ⊢k=K→≤k=≤K
13 12 2 eqtr4di ⊢k=K→≤k=≤˙
14 13 breqd ⊢k=K→x≤kw↔x≤˙w
15 fveq2 ⊢k=K→DIsoB⁡k=DIsoB⁡K
16 15 fveq1d ⊢k=K→DIsoB⁡k⁡w=DIsoB⁡K⁡w
17 16 fveq1d ⊢k=K→DIsoB⁡k⁡w⁡x=DIsoB⁡K⁡w⁡x
18 fveq2 ⊢k=K→DVecH⁡k=DVecH⁡K
19 18 fveq1d ⊢k=K→DVecH⁡k⁡w=DVecH⁡K⁡w
20 19 fveq2d ⊢k=K→LSubSp⁡DVecH⁡k⁡w=LSubSp⁡DVecH⁡K⁡w
21 fveq2 ⊢k=K→Atoms⁡k=Atoms⁡K
22 21 5 eqtr4di ⊢k=K→Atoms⁡k=A
23 13 breqd ⊢k=K→q≤kw↔q≤˙w
24 23 notbid ⊢k=K→¬q≤kw↔¬q≤˙w
25 fveq2 ⊢k=K→join⁡k=join⁡K
26 25 3 eqtr4di ⊢k=K→join⁡k=∨˙
27 eqidd ⊢k=K→q=q
28 fveq2 ⊢k=K→meet⁡k=meet⁡K
29 28 4 eqtr4di ⊢k=K→meet⁡k=∧˙
30 29 oveqd ⊢k=K→xmeet⁡kw=x∧˙w
31 26 27 30 oveq123d ⊢k=K→qjoin⁡kxmeet⁡kw=q∨˙x∧˙w
32 31 eqeq1d ⊢k=K→qjoin⁡kxmeet⁡kw=x↔q∨˙x∧˙w=x
33 24 32 anbi12d ⊢k=K→¬q≤kw∧qjoin⁡kxmeet⁡kw=x↔¬q≤˙w∧q∨˙x∧˙w=x
34 19 fveq2d ⊢k=K→LSSum⁡DVecH⁡k⁡w=LSSum⁡DVecH⁡K⁡w
35 fveq2 ⊢k=K→DIsoC⁡k=DIsoC⁡K
36 35 fveq1d ⊢k=K→DIsoC⁡k⁡w=DIsoC⁡K⁡w
37 36 fveq1d ⊢k=K→DIsoC⁡k⁡w⁡q=DIsoC⁡K⁡w⁡q
38 16 30 fveq12d ⊢k=K→DIsoB⁡k⁡w⁡xmeet⁡kw=DIsoB⁡K⁡w⁡x∧˙w
39 34 37 38 oveq123d ⊢k=K→DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w
40 39 eqeq2d ⊢k=K→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw↔u=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w
41 33 40 imbi12d ⊢k=K→¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw↔¬q≤˙w∧q∨˙x∧˙w=x→u=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w
42 22 41 raleqbidv ⊢k=K→∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw↔∀q∈A¬q≤˙w∧q∨˙x∧˙w=x→u=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w
43 20 42 riotaeqbidv ⊢k=K→ιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw=ιu∈LSubSp⁡DVecH⁡K⁡w|∀q∈A¬q≤˙w∧q∨˙x∧˙w=x→u=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w
44 14 17 43 ifbieq12d ⊢k=K→ifx≤kwDIsoB⁡k⁡w⁡xιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw=ifx≤˙wDIsoB⁡K⁡w⁡xιu∈LSubSp⁡DVecH⁡K⁡w|∀q∈A¬q≤˙w∧q∨˙x∧˙w=x→u=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w
45 11 44 mpteq12dv ⊢k=K→x∈Basek⟼ifx≤kwDIsoB⁡k⁡w⁡xιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw=x∈B⟼ifx≤˙wDIsoB⁡K⁡w⁡xιu∈LSubSp⁡DVecH⁡K⁡w|∀q∈A¬q≤˙w∧q∨˙x∧˙w=x→u=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w
46 9 45 mpteq12dv ⊢k=K→w∈LHyp⁡k⟼x∈Basek⟼ifx≤kwDIsoB⁡k⁡w⁡xιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw=w∈H⟼x∈B⟼ifx≤˙wDIsoB⁡K⁡w⁡xιu∈LSubSp⁡DVecH⁡K⁡w|∀q∈A¬q≤˙w∧q∨˙x∧˙w=x→u=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w
47 df-dih ⊢DIsoH=k∈V⟼w∈LHyp⁡k⟼x∈Basek⟼ifx≤kwDIsoB⁡k⁡w⁡xιu∈LSubSp⁡DVecH⁡k⁡w|∀q∈Atoms⁡k¬q≤kw∧qjoin⁡kxmeet⁡kw=x→u=DIsoC⁡k⁡w⁡qLSSum⁡DVecH⁡k⁡wDIsoB⁡k⁡w⁡xmeet⁡kw
48 46 47 6 mptfvmpt ⊢K∈V→DIsoH⁡K=w∈H⟼x∈B⟼ifx≤˙wDIsoB⁡K⁡w⁡xιu∈LSubSp⁡DVecH⁡K⁡w|∀q∈A¬q≤˙w∧q∨˙x∧˙w=x→u=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w
49 7 48 syl ⊢K∈V→DIsoH⁡K=w∈H⟼x∈B⟼ifx≤˙wDIsoB⁡K⁡w⁡xιu∈LSubSp⁡DVecH⁡K⁡w|∀q∈A¬q≤˙w∧q∨˙x∧˙w=x→u=DIsoC⁡K⁡w⁡qLSSum⁡DVecH⁡K⁡wDIsoB⁡K⁡w⁡x∧˙w