Metamath Proof Explorer

Theorem dicfval

Description: The partial isomorphism C for a lattice K . (Contributed by NM, 15-Dec-2013)

Ref Expression
Hypotheses dicval.l ⊢≤˙=≤K
dicval.a ⊢A=Atoms⁡K
dicval.h ⊢H=LHyp⁡K
dicval.p ⊢P=oc⁡K⁡W
dicval.t ⊢T=LTrn⁡K⁡W
dicval.e ⊢E=TEndo⁡K⁡W
dicval.i ⊢I=DIsoC⁡K⁡W
Assertion dicfval ⊢K∈V∧W∈H→I=q∈r∈A|¬r≤˙W⟼fs|f=s⁡ιg∈T|g⁡P=q∧s∈E

Proof

Step Hyp Ref Expression
1 dicval.l ⊢≤˙=≤K
2 dicval.a ⊢A=Atoms⁡K
3 dicval.h ⊢H=LHyp⁡K
4 dicval.p ⊢P=oc⁡K⁡W
5 dicval.t ⊢T=LTrn⁡K⁡W
6 dicval.e ⊢E=TEndo⁡K⁡W
7 dicval.i ⊢I=DIsoC⁡K⁡W
8 1 2 3 dicffval ⊢K∈V→DIsoC⁡K=w∈H⟼q∈r∈A|¬r≤˙w⟼fs|f=s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q∧s∈TEndo⁡K⁡w
9 8 fveq1d ⊢K∈V→DIsoC⁡K⁡W=w∈H⟼q∈r∈A|¬r≤˙w⟼fs|f=s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q∧s∈TEndo⁡K⁡w⁡W
10 7 9 eqtrid ⊢K∈V→I=w∈H⟼q∈r∈A|¬r≤˙w⟼fs|f=s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q∧s∈TEndo⁡K⁡w⁡W
11 breq2 ⊢w=W→r≤˙w↔r≤˙W
12 11 notbid ⊢w=W→¬r≤˙w↔¬r≤˙W
13 12 rabbidv ⊢w=W→r∈A|¬r≤˙w=r∈A|¬r≤˙W
14 fveq2 ⊢w=W→LTrn⁡K⁡w=LTrn⁡K⁡W
15 14 5 eqtr4di ⊢w=W→LTrn⁡K⁡w=T
16 fveq2 ⊢w=W→oc⁡K⁡w=oc⁡K⁡W
17 16 4 eqtr4di ⊢w=W→oc⁡K⁡w=P
18 17 fveqeq2d ⊢w=W→g⁡oc⁡K⁡w=q↔g⁡P=q
19 15 18 riotaeqbidv ⊢w=W→ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q=ιg∈T|g⁡P=q
20 19 fveq2d ⊢w=W→s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q=s⁡ιg∈T|g⁡P=q
21 20 eqeq2d ⊢w=W→f=s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q↔f=s⁡ιg∈T|g⁡P=q
22 fveq2 ⊢w=W→TEndo⁡K⁡w=TEndo⁡K⁡W
23 22 6 eqtr4di ⊢w=W→TEndo⁡K⁡w=E
24 23 eleq2d ⊢w=W→s∈TEndo⁡K⁡w↔s∈E
25 21 24 anbi12d ⊢w=W→f=s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q∧s∈TEndo⁡K⁡w↔f=s⁡ιg∈T|g⁡P=q∧s∈E
26 25 opabbidv ⊢w=W→fs|f=s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q∧s∈TEndo⁡K⁡w=fs|f=s⁡ιg∈T|g⁡P=q∧s∈E
27 13 26 mpteq12dv ⊢w=W→q∈r∈A|¬r≤˙w⟼fs|f=s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q∧s∈TEndo⁡K⁡w=q∈r∈A|¬r≤˙W⟼fs|f=s⁡ιg∈T|g⁡P=q∧s∈E
28 eqid ⊢w∈H⟼q∈r∈A|¬r≤˙w⟼fs|f=s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q∧s∈TEndo⁡K⁡w=w∈H⟼q∈r∈A|¬r≤˙w⟼fs|f=s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q∧s∈TEndo⁡K⁡w
29 2 fvexi ⊢A∈V
30 29 mptrabex ⊢q∈r∈A|¬r≤˙W⟼fs|f=s⁡ιg∈T|g⁡P=q∧s∈E∈V
31 27 28 30 fvmpt ⊢W∈H→w∈H⟼q∈r∈A|¬r≤˙w⟼fs|f=s⁡ιg∈LTrn⁡K⁡w|g⁡oc⁡K⁡w=q∧s∈TEndo⁡K⁡w⁡W=q∈r∈A|¬r≤˙W⟼fs|f=s⁡ιg∈T|g⁡P=q∧s∈E
32 10 31 sylan9eq ⊢K∈V∧W∈H→I=q∈r∈A|¬r≤˙W⟼fs|f=s⁡ιg∈T|g⁡P=q∧s∈E