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 
|- .<_ = ( le ` 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 e. V /\ W e. H ) -> I = ( x e. B |-> if ( x .<_ W , ( D ` x ) , ( iota_ u e. S A. q e. 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 
 |-  .<_ = ( 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 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 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 ) ) ) ) ) ) ) ) )
14 13 fveq1d 
 |-  ( K e. V -> ( ( DIsoH ` 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 ) ) ) ) ) ) ) ) ` W ) )
15 7 14 eqtrid 
 |-  ( K e. V -> I = ( ( 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 ) ) ) ) ) ) ) ) ` 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 -> ( A. q e. A ( ( -. q .<_ w /\ ( q .\/ ( x ./\ w ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` w ) ` q ) ( LSSum ` ( ( DVecH ` K ) ` w ) ) ( ( ( DIsoB ` K ) ` w ) ` ( x ./\ w ) ) ) ) <-> A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( x ./\ W ) ) = x ) -> u = ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) ) ) )
40 23 39 riotaeqbidv 
 |-  ( w = 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 ) ) ) ) ) = ( iota_ u e. S A. q e. 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 ) , ( 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 ) ) ) ) ) ) = if ( x .<_ W , ( D ` x ) , ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( x ./\ W ) ) = x ) -> u = ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) ) ) ) )
42 41 mpteq2dv 
 |-  ( w = 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 ) ) ) ) ) ) ) = ( x e. B |-> if ( x .<_ W , ( D ` x ) , ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( x ./\ W ) ) = x ) -> u = ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) ) ) ) ) )
43 eqid 
 |-  ( 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 ) ) ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) ) )
44 42 43 1 mptfvmpt 
 |-  ( W e. H -> ( ( 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 ) ) ) ) ) ) ) ) ` W ) = ( x e. B |-> if ( x .<_ W , ( D ` x ) , ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( x ./\ W ) ) = x ) -> u = ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) ) ) ) ) )
45 15 44 sylan9eq 
 |-  ( ( K e. V /\ W e. H ) -> I = ( x e. B |-> if ( x .<_ W , ( D ` x ) , ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( x ./\ W ) ) = x ) -> u = ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) ) ) ) ) )