Metamath Proof Explorer

Theorem dihval

Description: Value of isomorphism H for a lattice K . Definition of isomorphism map in Crawley p. 122 line 3. (Contributed by NM, 3-Feb-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 dihval 
|- ( ( ( K e. V /\ W e. H ) /\ X e. B ) -> ( I ` X ) = 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 7 8 9 10 11 12 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 ) ) ) ) ) ) ) )
14 13 fveq1d 
 |-  ( ( K e. V /\ W e. H ) -> ( I ` X ) = ( ( 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 ) ) ) ) ) ) ) ` X ) )
15 breq1 
 |-  ( x = X -> ( x .<_ W <-> X .<_ W ) )
16 fveq2 
 |-  ( x = X -> ( D ` x ) = ( D ` X ) )
17 oveq1 
 |-  ( x = X -> ( x ./\ W ) = ( X ./\ W ) )
18 17 oveq2d 
 |-  ( x = X -> ( q .\/ ( x ./\ W ) ) = ( q .\/ ( X ./\ W ) ) )
19 id 
 |-  ( x = X -> x = X )
20 18 19 eqeq12d 
 |-  ( x = X -> ( ( q .\/ ( x ./\ W ) ) = x <-> ( q .\/ ( X ./\ W ) ) = X ) )
21 20 anbi2d 
 |-  ( x = X -> ( ( -. q .<_ W /\ ( q .\/ ( x ./\ W ) ) = x ) <-> ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) ) )
22 fvoveq1 
 |-  ( x = X -> ( D ` ( x ./\ W ) ) = ( D ` ( X ./\ W ) ) )
23 22 oveq2d 
 |-  ( x = X -> ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) )
24 23 eqeq2d 
 |-  ( x = X -> ( u = ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) <-> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) )
25 21 24 imbi12d 
 |-  ( x = X -> ( ( ( -. q .<_ W /\ ( q .\/ ( x ./\ W ) ) = x ) -> u = ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) ) <-> ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
26 25 ralbidv 
 |-  ( x = X -> ( A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( x ./\ W ) ) = x ) -> u = ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) ) <-> A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
27 26 riotabidv 
 |-  ( x = X -> ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( x ./\ W ) ) = x ) -> u = ( ( C ` q ) .(+) ( D ` ( x ./\ W ) ) ) ) ) = ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) )
28 15 16 27 ifbieq12d 
 |-  ( x = X -> 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 ) ) ) ) ) ) = 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 ) ) ) ) ) ) )
29 eqid 
 |-  ( 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 ) ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) )
30 fvex 
 |-  ( D ` X ) e. _V
31 riotaex 
 |-  ( iota_ u e. S A. q e. A ( ( -. q .<_ W /\ ( q .\/ ( X ./\ W ) ) = X ) -> u = ( ( C ` q ) .(+) ( D ` ( X ./\ W ) ) ) ) ) e. _V
32 30 31 ifex 
 |-  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 ) ) ) ) ) ) e. _V
33 28 29 32 fvmpt 
 |-  ( X e. B -> ( ( 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 ) ) ) ) ) ) ) ` X ) = 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 ) ) ) ) ) ) )
34 14 33 sylan9eq 
 |-  ( ( ( K e. V /\ W e. H ) /\ X e. B ) -> ( I ` X ) = 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 ) ) ) ) ) ) )