Metamath Proof Explorer

Theorem dihffval

Description: The 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 
|- .<_ = ( le ` K )
dihval.j 
|- .\/ = ( join ` K )
dihval.m 
|- ./\ = ( meet ` K )
dihval.a 
|- A = ( Atoms ` K )
dihval.h 
|- H = ( LHyp ` K )
Assertion dihffval 
|- ( K e. V -> ( DIsoH ` K ) = ( w e. H |-> ( x e. B |-> if ( x .<_ w , ( ( ( DIsoB ` K ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) A. q e. A ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dihval.b 
 |-  B = ( Base ` K )
2 dihval.l 
 |-  .<_ = ( le ` K )
3 dihval.j 
 |-  .\/ = ( join ` K )
4 dihval.m 
 |-  ./\ = ( meet ` K )
5 dihval.a 
 |-  A = ( Atoms ` K )
6 dihval.h 
 |-  H = ( LHyp ` K )
7 elex 
 |-  ( K e. V -> K e. _V )
8 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
9 8 6 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
10 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
11 10 1 eqtr4di 
 |-  ( k = K -> ( Base ` k ) = B )
12 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
13 12 2 eqtr4di 
 |-  ( k = K -> ( le ` k ) = .<_ )
14 13 breqd 
 |-  ( k = K -> ( x ( le ` k ) w <-> x .<_ w ) )
15 fveq2 
 |-  ( k = K -> ( DIsoB ` k ) = ( DIsoB ` K ) )
16 15 fveq1d 
 |-  ( k = K -> ( ( DIsoB ` k ) ` w ) = ( ( DIsoB ` K ) ` w ) )
17 16 fveq1d 
 |-  ( k = K -> ( ( ( DIsoB ` k ) ` w ) ` x ) = ( ( ( DIsoB ` K ) ` w ) ` x ) )
18 fveq2 
 |-  ( k = K -> ( DVecH ` k ) = ( DVecH ` K ) )
19 18 fveq1d 
 |-  ( k = K -> ( ( DVecH ` k ) ` w ) = ( ( DVecH ` K ) ` w ) )
20 19 fveq2d 
 |-  ( k = K -> ( LSubSp ` ( ( DVecH ` k ) ` w ) ) = ( LSubSp ` ( ( DVecH ` K ) ` w ) ) )
21 fveq2 
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
22 21 5 eqtr4di 
 |-  ( k = K -> ( Atoms ` k ) = A )
23 13 breqd 
 |-  ( k = K -> ( q ( le ` k ) w <-> q .<_ w ) )
24 23 notbid 
 |-  ( k = K -> ( -. q ( le ` k ) w <-> -. q .<_ w ) )
25 fveq2 
 |-  ( k = K -> ( join ` k ) = ( join ` K ) )
26 25 3 eqtr4di 
 |-  ( k = K -> ( join ` k ) = .\/ )
27 eqidd 
 |-  ( k = K -> q = q )
28 fveq2 
 |-  ( k = K -> ( meet ` k ) = ( meet ` K ) )
29 28 4 eqtr4di 
 |-  ( k = K -> ( meet ` k ) = ./\ )
30 29 oveqd 
 |-  ( k = K -> ( x ( meet ` k ) w ) = ( x ./\ w ) )
31 26 27 30 oveq123d 
 |-  ( k = K -> ( q ( join ` k ) ( x ( meet ` k ) w ) ) = ( q .\/ ( x ./\ w ) ) )
32 31 eqeq1d 
 |-  ( k = K -> ( ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x <-> ( q .\/ ( x ./\ w ) ) = x ) )
33 24 32 anbi12d 
 |-  ( k = K -> ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) <-> ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) ) )
34 19 fveq2d 
 |-  ( k = K -> ( LSSum ` ( ( DVecH ` k ) ` w ) ) = ( LSSum ` ( ( DVecH ` K ) ` w ) ) )
35 fveq2 
 |-  ( k = K -> ( DIsoC ` k ) = ( DIsoC ` K ) )
36 35 fveq1d 
 |-  ( k = K -> ( ( DIsoC ` k ) ` w ) = ( ( DIsoC ` K ) ` w ) )
37 36 fveq1d 
 |-  ( k = K -> ( ( ( DIsoC ` k ) ` w ) ` q ) = ( ( ( DIsoC ` K ) ` w ) ` q ) )
38 16 30 fveq12d 
 |-  ( k = K -> ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) = ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) )
39 34 37 38 oveq123d 
 |-  ( k = K -> ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) )
40 39 eqeq2d 
 |-  ( k = K -> ( u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) <-> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) )
41 33 40 imbi12d 
 |-  ( k = K -> ( ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) <-> ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) ) )
42 22 41 raleqbidv 
 |-  ( k = K -> ( A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) <-> A. q e. A ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) ) )
43 20 42 riotaeqbidv 
 |-  ( k = K -> ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) = ( iota_ u e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) A. q e. A ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) ) )
44 14 17 43 ifbieq12d 
 |-  ( k = K -> if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) ) = if ( x .<_ w , ( ( ( DIsoB ` K ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) A. q e. A ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) ) ) )
45 11 44 mpteq12dv 
 |-  ( k = K -> ( x e. ( Base ` k ) |-> if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) ) ) = ( x e. B |-> if ( x .<_ w , ( ( ( DIsoB ` K ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) A. q e. A ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) ) ) ) )
46 9 45 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> ( x e. ( Base ` k ) |-> if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) ) ) ) = ( w e. H |-> ( x e. B |-> if ( x .<_ w , ( ( ( DIsoB ` K ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) A. q e. A ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) ) ) ) ) )
47 df-dih 
 |-  DIsoH = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( x e. ( Base ` k ) |-> if ( x ( le ` k ) w , ( ( ( DIsoB ` k ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` k ) ` w ) ) A. q e. ( Atoms ` k ) ( ( -. q ( le ` k ) w /\ ( q ( join ` k ) ( x ( meet ` k ) w ) ) = x ) -> u = ( ( ( ( DIsoC ` k ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` k ) ` w ) ) ( ( ( DIsoB ` k ) ` w ) ` ( x ( meet ` k ) w ) ) ) ) ) ) ) ) )
48 46 47 6 mptfvmpt 
 |-  ( K e. _V -> ( DIsoH ` K ) = ( w e. H |-> ( x e. B |-> if ( x .<_ w , ( ( ( DIsoB ` K ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) A. q e. A ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) ) ) ) ) )
49 7 48 syl 
 |-  ( K e. V -> ( DIsoH ` K ) = ( w e. H |-> ( x e. B |-> if ( x .<_ w , ( ( ( DIsoB ` K ) ` w ) ` x ) , ( iota_ u e. ( LSubSp ` ( ( DVecH ` K ) ` w ) ) A. q e. A ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) ) ) ) ) )