# Metamath Proof Explorer

## Theorem dihfval

Description: 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 = Base K$
dihval.l
dihval.j
dihval.m
dihval.a $⊢ A = Atoms ⁡ K$
dihval.h $⊢ H = LHyp ⁡ K$
dihval.i $⊢ I = DIsoH ⁡ K ⁡ W$
dihval.d $⊢ D = DIsoB ⁡ K ⁡ W$
dihval.c $⊢ C = DIsoC ⁡ K ⁡ W$
dihval.u $⊢ U = DVecH ⁡ K ⁡ W$
dihval.s $⊢ S = LSubSp ⁡ U$
dihval.p
Assertion dihfval

### Proof

Step Hyp Ref Expression
1 dihval.b $⊢ B = Base K$
2 dihval.l
3 dihval.j
4 dihval.m
5 dihval.a $⊢ A = Atoms ⁡ K$
6 dihval.h $⊢ H = LHyp ⁡ K$
7 dihval.i $⊢ I = DIsoH ⁡ K ⁡ W$
8 dihval.d $⊢ D = DIsoB ⁡ K ⁡ W$
9 dihval.c $⊢ C = DIsoC ⁡ K ⁡ W$
10 dihval.u $⊢ U = DVecH ⁡ K ⁡ W$
11 dihval.s $⊢ S = LSubSp ⁡ U$
12 dihval.p
13 1 2 3 4 5 6 dihffval
14 13 fveq1d
15 7 14 syl5eq
16 breq2
17 fveq2 $⊢ w = W → DIsoB ⁡ K ⁡ w = DIsoB ⁡ K ⁡ W$
18 17 8 eqtr4di $⊢ w = W → DIsoB ⁡ K ⁡ w = D$
19 18 fveq1d $⊢ w = W → DIsoB ⁡ K ⁡ w ⁡ x = D ⁡ x$
20 fveq2 $⊢ w = W → DVecH ⁡ K ⁡ w = DVecH ⁡ K ⁡ W$
21 20 10 eqtr4di $⊢ w = W → DVecH ⁡ K ⁡ w = U$
22 21 fveq2d $⊢ w = W → LSubSp ⁡ DVecH ⁡ K ⁡ w = LSubSp ⁡ U$
23 22 11 eqtr4di $⊢ w = W → LSubSp ⁡ DVecH ⁡ K ⁡ w = S$
24 breq2
25 24 notbid
26 oveq2
27 26 oveq2d
28 27 eqeq1d
29 25 28 anbi12d
30 21 fveq2d $⊢ w = W → LSSum ⁡ DVecH ⁡ K ⁡ w = LSSum ⁡ U$
31 30 12 eqtr4di
32 fveq2 $⊢ w = W → DIsoC ⁡ K ⁡ w = DIsoC ⁡ K ⁡ W$
33 32 9 eqtr4di $⊢ w = W → DIsoC ⁡ K ⁡ w = C$
34 33 fveq1d $⊢ w = W → DIsoC ⁡ K ⁡ w ⁡ q = C ⁡ q$
35 18 26 fveq12d
36 31 34 35 oveq123d
37 36 eqeq2d
38 29 37 imbi12d
39 38 ralbidv
40 23 39 riotaeqbidv
41 16 19 40 ifbieq12d
42 41 mpteq2dv
43 eqid
44 42 43 1 mptfvmpt
45 15 44 sylan9eq