Metamath Proof Explorer

Theorem dihf11lem

Description: Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihf11.b ⊢B=BaseK
dihf11.h ⊢H=LHyp⁡K
dihf11.i ⊢I=DIsoH⁡K⁡W
dihf11.u ⊢U=DVecH⁡K⁡W
dihf11.s ⊢S=LSubSp⁡U
Assertion dihf11lem ⊢K∈HL∧W∈H→I:B⟶S

Proof

Step Hyp Ref Expression
1 dihf11.b ⊢B=BaseK
2 dihf11.h ⊢H=LHyp⁡K
3 dihf11.i ⊢I=DIsoH⁡K⁡W
4 dihf11.u ⊢U=DVecH⁡K⁡W
5 dihf11.s ⊢S=LSubSp⁡U
6 fvex ⊢DIsoB⁡K⁡W⁡x∈V
7 riotaex ⊢ιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KW∈V
8 6 7 ifex ⊢ifx≤KWDIsoB⁡K⁡W⁡xιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KW∈V
9 8 rgenw ⊢∀x∈Bifx≤KWDIsoB⁡K⁡W⁡xιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KW∈V
10 9 a1i ⊢K∈HL∧W∈H→∀x∈Bifx≤KWDIsoB⁡K⁡W⁡xιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KW∈V
11 eqid ⊢x∈B⟼ifx≤KWDIsoB⁡K⁡W⁡xιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KW=x∈B⟼ifx≤KWDIsoB⁡K⁡W⁡xιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KW
12 11 mptfng ⊢∀x∈Bifx≤KWDIsoB⁡K⁡W⁡xιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KW∈V↔x∈B⟼ifx≤KWDIsoB⁡K⁡W⁡xιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KWFnB
13 10 12 sylib ⊢K∈HL∧W∈H→x∈B⟼ifx≤KWDIsoB⁡K⁡W⁡xιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KWFnB
14 eqid ⊢≤K=≤K
15 eqid ⊢join⁡K=join⁡K
16 eqid ⊢meet⁡K=meet⁡K
17 eqid ⊢Atoms⁡K=Atoms⁡K
18 eqid ⊢DIsoB⁡K⁡W=DIsoB⁡K⁡W
19 eqid ⊢DIsoC⁡K⁡W=DIsoC⁡K⁡W
20 eqid ⊢LSSum⁡U=LSSum⁡U
21 1 14 15 16 17 2 3 18 19 4 5 20 dihfval ⊢K∈HL∧W∈H→I=x∈B⟼ifx≤KWDIsoB⁡K⁡W⁡xιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KW
22 21 fneq1d ⊢K∈HL∧W∈H→IFnB↔x∈B⟼ifx≤KWDIsoB⁡K⁡W⁡xιu∈S|∀q∈Atoms⁡K¬q≤KW∧qjoin⁡Kxmeet⁡KW=x→u=DIsoC⁡K⁡W⁡qLSSum⁡UDIsoB⁡K⁡W⁡xmeet⁡KWFnB
23 13 22 mpbird ⊢K∈HL∧W∈H→IFnB
24 1 2 3 4 5 dihlss ⊢K∈HL∧W∈H∧y∈B→I⁡y∈S
25 24 ralrimiva ⊢K∈HL∧W∈H→∀y∈BI⁡y∈S
26 fnfvrnss ⊢IFnB∧∀y∈BI⁡y∈S→ran⁡I⊆S
27 23 25 26 syl2anc ⊢K∈HL∧W∈H→ran⁡I⊆S
28 df-f ⊢I:B⟶S↔IFnB∧ran⁡I⊆S
29 23 27 28 sylanbrc ⊢K∈HL∧W∈H→I:B⟶S