Metamath Proof Explorer


Theorem dibffval

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

Ref Expression
Hypotheses dibval.b B = Base K
dibval.h H = LHyp K
Assertion dibffval K V DIsoB K = w H x dom DIsoA K w DIsoA K w x × f LTrn K w I B

Proof

Step Hyp Ref Expression
1 dibval.b B = Base K
2 dibval.h H = LHyp K
3 elex K V K V
4 fveq2 k = K LHyp k = LHyp K
5 4 2 eqtr4di k = K LHyp k = H
6 fveq2 k = K DIsoA k = DIsoA K
7 6 fveq1d k = K DIsoA k w = DIsoA K w
8 7 dmeqd k = K dom DIsoA k w = dom DIsoA K w
9 7 fveq1d k = K DIsoA k w x = DIsoA K w x
10 fveq2 k = K LTrn k = LTrn K
11 10 fveq1d k = K LTrn k w = LTrn K w
12 fveq2 k = K Base k = Base K
13 12 1 eqtr4di k = K Base k = B
14 13 reseq2d k = K I Base k = I B
15 11 14 mpteq12dv k = K f LTrn k w I Base k = f LTrn K w I B
16 15 sneqd k = K f LTrn k w I Base k = f LTrn K w I B
17 9 16 xpeq12d k = K DIsoA k w x × f LTrn k w I Base k = DIsoA K w x × f LTrn K w I B
18 8 17 mpteq12dv k = K x dom DIsoA k w DIsoA k w x × f LTrn k w I Base k = x dom DIsoA K w DIsoA K w x × f LTrn K w I B
19 5 18 mpteq12dv k = K w LHyp k x dom DIsoA k w DIsoA k w x × f LTrn k w I Base k = w H x dom DIsoA K w DIsoA K w x × f LTrn K w I B
20 df-dib DIsoB = k V w LHyp k x dom DIsoA k w DIsoA k w x × f LTrn k w I Base k
21 19 20 2 mptfvmpt K V DIsoB K = w H x dom DIsoA K w DIsoA K w x × f LTrn K w I B
22 3 21 syl K V DIsoB K = w H x dom DIsoA K w DIsoA K w x × f LTrn K w I B