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 ˙ = K
dihval.j ˙ = join K
dihval.m ˙ = meet K
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 ˙ = LSSum U
Assertion dihfval K V W H I = x B if x ˙ W D x ι u S | q A ¬ q ˙ W q ˙ x ˙ W = x u = C q ˙ D x ˙ W

Proof

Step Hyp Ref Expression
1 dihval.b B = Base K
2 dihval.l ˙ = K
3 dihval.j ˙ = join K
4 dihval.m ˙ = meet K
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 ˙ = LSSum U
13 1 2 3 4 5 6 dihffval K V DIsoH K = w H x B if x ˙ w DIsoB K w x ι u LSubSp DVecH K w | q A ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w
14 13 fveq1d K V DIsoH K W = w H x B if x ˙ w DIsoB K w x ι u LSubSp DVecH K w | q A ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w W
15 7 14 syl5eq K V I = w H x B if x ˙ w DIsoB K w x ι u LSubSp DVecH K w | q A ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w W
16 breq2 w = W x ˙ w x ˙ W
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 w = W q ˙ w q ˙ W
25 24 notbid w = W ¬ q ˙ w ¬ q ˙ W
26 oveq2 w = W x ˙ w = x ˙ W
27 26 oveq2d w = W q ˙ x ˙ w = q ˙ x ˙ W
28 27 eqeq1d w = W q ˙ x ˙ w = x q ˙ x ˙ W = x
29 25 28 anbi12d w = W ¬ q ˙ w q ˙ x ˙ w = x ¬ q ˙ W q ˙ x ˙ W = x
30 21 fveq2d w = W LSSum DVecH K w = LSSum U
31 30 12 eqtr4di w = W LSSum DVecH K w = ˙
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 w = W DIsoB K w x ˙ w = D x ˙ W
36 31 34 35 oveq123d w = W DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w = C q ˙ D x ˙ W
37 36 eqeq2d w = W u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w u = C q ˙ D x ˙ W
38 29 37 imbi12d w = W ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w ¬ q ˙ W q ˙ x ˙ W = x u = C q ˙ D x ˙ W
39 38 ralbidv w = W q A ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w q A ¬ q ˙ W q ˙ x ˙ W = x u = C q ˙ D x ˙ W
40 23 39 riotaeqbidv w = W ι u LSubSp DVecH K w | q A ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w = ι u S | q A ¬ q ˙ W q ˙ x ˙ W = x u = C q ˙ D x ˙ W
41 16 19 40 ifbieq12d w = W if x ˙ w DIsoB K w x ι u LSubSp DVecH K w | q A ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w = if x ˙ W D x ι u S | q A ¬ q ˙ W q ˙ x ˙ W = x u = C q ˙ D x ˙ W
42 41 mpteq2dv w = W x B if x ˙ w DIsoB K w x ι u LSubSp DVecH K w | q A ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w = x B if x ˙ W D x ι u S | q A ¬ q ˙ W q ˙ x ˙ W = x u = C q ˙ D x ˙ W
43 eqid w H x B if x ˙ w DIsoB K w x ι u LSubSp DVecH K w | q A ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w = w H x B if x ˙ w DIsoB K w x ι u LSubSp DVecH K w | q A ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w
44 42 43 1 mptfvmpt W H w H x B if x ˙ w DIsoB K w x ι u LSubSp DVecH K w | q A ¬ q ˙ w q ˙ x ˙ w = x u = DIsoC K w q LSSum DVecH K w DIsoB K w x ˙ w W = x B if x ˙ W D x ι u S | q A ¬ q ˙ W q ˙ x ˙ W = x u = C q ˙ D x ˙ W
45 15 44 sylan9eq K V W H I = x B if x ˙ W D x ι u S | q A ¬ q ˙ W q ˙ x ˙ W = x u = C q ˙ D x ˙ W