Metamath Proof Explorer


Theorem dibfval

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
dibval.t T = LTrn K W
dibval.o 0 ˙ = f T I B
dibval.j J = DIsoA K W
dibval.i I = DIsoB K W
Assertion dibfval K V W H I = x dom J J x × 0 ˙

Proof

Step Hyp Ref Expression
1 dibval.b B = Base K
2 dibval.h H = LHyp K
3 dibval.t T = LTrn K W
4 dibval.o 0 ˙ = f T I B
5 dibval.j J = DIsoA K W
6 dibval.i I = DIsoB K W
7 1 2 dibffval K V DIsoB K = w H x dom DIsoA K w DIsoA K w x × f LTrn K w I B
8 7 fveq1d K V DIsoB K W = w H x dom DIsoA K w DIsoA K w x × f LTrn K w I B W
9 6 8 syl5eq K V I = w H x dom DIsoA K w DIsoA K w x × f LTrn K w I B W
10 fveq2 w = W DIsoA K w = DIsoA K W
11 10 5 eqtr4di w = W DIsoA K w = J
12 11 dmeqd w = W dom DIsoA K w = dom J
13 11 fveq1d w = W DIsoA K w x = J x
14 fveq2 w = W LTrn K w = LTrn K W
15 14 3 eqtr4di w = W LTrn K w = T
16 eqidd w = W I B = I B
17 15 16 mpteq12dv w = W f LTrn K w I B = f T I B
18 17 4 eqtr4di w = W f LTrn K w I B = 0 ˙
19 18 sneqd w = W f LTrn K w I B = 0 ˙
20 13 19 xpeq12d w = W DIsoA K w x × f LTrn K w I B = J x × 0 ˙
21 12 20 mpteq12dv w = W x dom DIsoA K w DIsoA K w x × f LTrn K w I B = x dom J J x × 0 ˙
22 eqid w H x dom DIsoA K w DIsoA K w x × f LTrn K w I B = w H x dom DIsoA K w DIsoA K w x × f LTrn K w I B
23 5 fvexi J V
24 23 dmex dom J V
25 24 mptex x dom J J x × 0 ˙ V
26 21 22 25 fvmpt W H w H x dom DIsoA K w DIsoA K w x × f LTrn K w I B W = x dom J J x × 0 ˙
27 9 26 sylan9eq K V W H I = x dom J J x × 0 ˙