Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihmeetlem2N Structured version   Unicode version

Theorem dihmeetlem2N 34666
Description: Isomorphism H of a conjunction. (Contributed by NM, 22-Mar-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
dihmeetlem2.b  |-  B  =  ( Base `  K
)
dihmeetlem2.m  |-  ./\  =  ( meet `  K )
dihmeetlem2.h  |-  H  =  ( LHyp `  K
)
dihmeetlem2.i  |-  I  =  ( ( DIsoH `  K
) `  W )
dihmeetlem2.l  |-  .<_  =  ( le `  K )
dihmeetlem2.j  |-  .\/  =  ( join `  K )
dihmeetlem2.a  |-  A  =  ( Atoms `  K )
dihmeetlem2.p  |-  P  =  ( ( oc `  K ) `  W
)
dihmeetlem2.t  |-  T  =  ( ( LTrn `  K
) `  W )
dihmeetlem2.r  |-  R  =  ( ( trL `  K
) `  W )
dihmeetlem2.e  |-  E  =  ( ( TEndo `  K
) `  W )
dihmeetlem2.g  |-  G  =  ( iota_ h  e.  T  ( h `  P
)  =  q )
dihmeetlem2.o  |-  .0.  =  ( h  e.  T  |->  (  _I  |`  B ) )
Assertion
Ref Expression
dihmeetlem2N  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( I `  ( X  ./\  Y ) )  =  ( ( I `
 X )  i^i  ( I `  Y
) ) )

Proof of Theorem dihmeetlem2N
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eqid 2441 . . . . . 6  |-  ( glb `  K )  =  ( glb `  K )
2 dihmeetlem2.m . . . . . 6  |-  ./\  =  ( meet `  K )
3 simp1l 1007 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  K  e.  HL )
4 simp2l 1009 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  X  e.  B )
5 simp3l 1011 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  Y  e.  B )
61, 2, 3, 4, 5meetval 15185 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( X  ./\  Y
)  =  ( ( glb `  K ) `
 { X ,  Y } ) )
76fveq2d 5692 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( ( ( DIsoB `  K ) `  W
) `  ( X  ./\ 
Y ) )  =  ( ( ( DIsoB `  K ) `  W
) `  ( ( glb `  K ) `  { X ,  Y }
) ) )
8 simp1 983 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( K  e.  HL  /\  W  e.  H ) )
9 dihmeetlem2.b . . . . . . . . 9  |-  B  =  ( Base `  K
)
10 dihmeetlem2.l . . . . . . . . 9  |-  .<_  =  ( le `  K )
11 dihmeetlem2.h . . . . . . . . 9  |-  H  =  ( LHyp `  K
)
12 eqid 2441 . . . . . . . . 9  |-  ( (
DIsoB `  K ) `  W )  =  ( ( DIsoB `  K ) `  W )
139, 10, 11, 12dibeldmN 34525 . . . . . . . 8  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( X  e.  dom  ( ( DIsoB `  K
) `  W )  <->  ( X  e.  B  /\  X  .<_  W ) ) )
1413biimpar 482 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W ) )  ->  X  e.  dom  ( ( DIsoB `  K ) `  W
) )
15143adant3 1003 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  X  e.  dom  ( (
DIsoB `  K ) `  W ) )
169, 10, 11, 12dibeldmN 34525 . . . . . . . 8  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( Y  e.  dom  ( ( DIsoB `  K
) `  W )  <->  ( Y  e.  B  /\  Y  .<_  W ) ) )
1716biimpar 482 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  Y  e.  dom  ( ( DIsoB `  K ) `  W
) )
18173adant2 1002 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  Y  e.  dom  ( (
DIsoB `  K ) `  W ) )
19 prssg 4025 . . . . . . 7  |-  ( ( X  e.  B  /\  Y  e.  B )  ->  ( ( X  e. 
dom  ( ( DIsoB `  K ) `  W
)  /\  Y  e.  dom  ( ( DIsoB `  K
) `  W )
)  <->  { X ,  Y }  C_  dom  ( (
DIsoB `  K ) `  W ) ) )
204, 5, 19syl2anc 656 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( ( X  e. 
dom  ( ( DIsoB `  K ) `  W
)  /\  Y  e.  dom  ( ( DIsoB `  K
) `  W )
)  <->  { X ,  Y }  C_  dom  ( (
DIsoB `  K ) `  W ) ) )
2115, 18, 20mpbi2and 907 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  { X ,  Y }  C_ 
dom  ( ( DIsoB `  K ) `  W
) )
22 prnzg 3992 . . . . . 6  |-  ( X  e.  B  ->  { X ,  Y }  =/=  (/) )
234, 22syl 16 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  { X ,  Y }  =/=  (/) )
241, 11, 12dibglbN 34533 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( { X ,  Y }  C_  dom  ( ( DIsoB `  K
) `  W )  /\  { X ,  Y }  =/=  (/) ) )  -> 
( ( ( DIsoB `  K ) `  W
) `  ( ( glb `  K ) `  { X ,  Y }
) )  =  |^|_ x  e.  { X ,  Y }  ( (
( DIsoB `  K ) `  W ) `  x
) )
258, 21, 23, 24syl12anc 1211 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( ( ( DIsoB `  K ) `  W
) `  ( ( glb `  K ) `  { X ,  Y }
) )  =  |^|_ x  e.  { X ,  Y }  ( (
( DIsoB `  K ) `  W ) `  x
) )
267, 25eqtrd 2473 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( ( ( DIsoB `  K ) `  W
) `  ( X  ./\ 
Y ) )  = 
|^|_ x  e.  { X ,  Y }  ( ( ( DIsoB `  K ) `  W ) `  x
) )
27 hllat 32730 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  Lat )
283, 27syl 16 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  K  e.  Lat )
299, 2latmcl 15218 . . . . 5  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  e.  B )
3028, 4, 5, 29syl3anc 1213 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( X  ./\  Y
)  e.  B )
31 simp1r 1008 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  W  e.  H )
329, 11lhpbase 33364 . . . . . 6  |-  ( W  e.  H  ->  W  e.  B )
3331, 32syl 16 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  W  e.  B )
349, 10, 2latmle1 15242 . . . . . 6  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  .<_  X )
3528, 4, 5, 34syl3anc 1213 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( X  ./\  Y
)  .<_  X )
36 simp2r 1010 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  X  .<_  W )
379, 10, 28, 30, 4, 33, 35, 36lattrd 15224 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( X  ./\  Y
)  .<_  W )
38 dihmeetlem2.i . . . . 5  |-  I  =  ( ( DIsoH `  K
) `  W )
399, 10, 11, 38, 12dihvalb 34604 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( X 
./\  Y )  e.  B  /\  ( X 
./\  Y )  .<_  W ) )  -> 
( I `  ( X  ./\  Y ) )  =  ( ( (
DIsoB `  K ) `  W ) `  ( X  ./\  Y ) ) )
408, 30, 37, 39syl12anc 1211 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( I `  ( X  ./\  Y ) )  =  ( ( (
DIsoB `  K ) `  W ) `  ( X  ./\  Y ) ) )
41 simpl1 986 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  /\  x  e. 
{ X ,  Y } )  ->  ( K  e.  HL  /\  W  e.  H ) )
42 vex 2973 . . . . . . 7  |-  x  e. 
_V
4342elpr 3892 . . . . . 6  |-  ( x  e.  { X ,  Y }  <->  ( x  =  X  \/  x  =  Y ) )
44 simpl2 987 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  /\  x  =  X )  ->  ( X  e.  B  /\  X  .<_  W ) )
45 eleq1 2501 . . . . . . . . . 10  |-  ( x  =  X  ->  (
x  e.  B  <->  X  e.  B ) )
46 breq1 4292 . . . . . . . . . 10  |-  ( x  =  X  ->  (
x  .<_  W  <->  X  .<_  W ) )
4745, 46anbi12d 705 . . . . . . . . 9  |-  ( x  =  X  ->  (
( x  e.  B  /\  x  .<_  W )  <-> 
( X  e.  B  /\  X  .<_  W ) ) )
4847adantl 463 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  /\  x  =  X )  ->  (
( x  e.  B  /\  x  .<_  W )  <-> 
( X  e.  B  /\  X  .<_  W ) ) )
4944, 48mpbird 232 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  /\  x  =  X )  ->  (
x  e.  B  /\  x  .<_  W ) )
50 simpl3 988 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  /\  x  =  Y )  ->  ( Y  e.  B  /\  Y  .<_  W ) )
51 eleq1 2501 . . . . . . . . . 10  |-  ( x  =  Y  ->  (
x  e.  B  <->  Y  e.  B ) )
52 breq1 4292 . . . . . . . . . 10  |-  ( x  =  Y  ->  (
x  .<_  W  <->  Y  .<_  W ) )
5351, 52anbi12d 705 . . . . . . . . 9  |-  ( x  =  Y  ->  (
( x  e.  B  /\  x  .<_  W )  <-> 
( Y  e.  B  /\  Y  .<_  W ) ) )
5453adantl 463 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  /\  x  =  Y )  ->  (
( x  e.  B  /\  x  .<_  W )  <-> 
( Y  e.  B  /\  Y  .<_  W ) ) )
5550, 54mpbird 232 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  /\  x  =  Y )  ->  (
x  e.  B  /\  x  .<_  W ) )
5649, 55jaodan 778 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  /\  ( x  =  X  \/  x  =  Y ) )  -> 
( x  e.  B  /\  x  .<_  W ) )
5743, 56sylan2b 472 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  /\  x  e. 
{ X ,  Y } )  ->  (
x  e.  B  /\  x  .<_  W ) )
589, 10, 11, 38, 12dihvalb 34604 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( x  e.  B  /\  x  .<_  W ) )  ->  (
I `  x )  =  ( ( (
DIsoB `  K ) `  W ) `  x
) )
5941, 57, 58syl2anc 656 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  /\  x  e. 
{ X ,  Y } )  ->  (
I `  x )  =  ( ( (
DIsoB `  K ) `  W ) `  x
) )
6059iineq2dv 4190 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  |^|_ x  e.  { X ,  Y }  ( I `
 x )  = 
|^|_ x  e.  { X ,  Y }  ( ( ( DIsoB `  K ) `  W ) `  x
) )
6126, 40, 603eqtr4d 2483 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( I `  ( X  ./\  Y ) )  =  |^|_ x  e.  { X ,  Y } 
( I `  x
) )
62 fveq2 5688 . . . 4  |-  ( x  =  X  ->  (
I `  x )  =  ( I `  X ) )
63 fveq2 5688 . . . 4  |-  ( x  =  Y  ->  (
I `  x )  =  ( I `  Y ) )
6462, 63iinxprg 4245 . . 3  |-  ( ( X  e.  B  /\  Y  e.  B )  -> 
|^|_ x  e.  { X ,  Y }  ( I `
 x )  =  ( ( I `  X )  i^i  (
I `  Y )
) )
654, 5, 64syl2anc 656 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  ->  |^|_ x  e.  { X ,  Y }  ( I `
 x )  =  ( ( I `  X )  i^i  (
I `  Y )
) )
6661, 65eqtrd 2473 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e.  B  /\  X  .<_  W )  /\  ( Y  e.  B  /\  Y  .<_  W ) )  -> 
( I `  ( X  ./\  Y ) )  =  ( ( I `
 X )  i^i  ( I `  Y
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1761    =/= wne 2604    i^i cin 3324    C_ wss 3325   (/)c0 3634   {cpr 3876   |^|_ciin 4169   class class class wbr 4289    e. cmpt 4347    _I cid 4627   dom cdm 4836    |` cres 4838   ` cfv 5415   iota_crio 6048  (class class class)co 6090   Basecbs 14170   lecple 14241   occoc 14242   glbcglb 15109   joincjn 15110   meetcmee 15111   Latclat 15211   Atomscatm 32630   HLchlt 32717   LHypclh 33350   LTrncltrn 33467   trLctrl 33524   TEndoctendo 34118   DIsoBcdib 34505   DIsoHcdih 34595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-iin 4171  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-map 7212  df-poset 15112  df-plt 15124  df-lub 15140  df-glb 15141  df-join 15142  df-meet 15143  df-p0 15205  df-p1 15206  df-lat 15212  df-clat 15274  df-oposet 32543  df-ol 32545  df-oml 32546  df-covers 32633  df-ats 32634  df-atl 32665  df-cvlat 32689  df-hlat 32718  df-lhyp 33354  df-laut 33355  df-ldil 33470  df-ltrn 33471  df-trl 33525  df-disoa 34396  df-dib 34506  df-dih 34596
This theorem is referenced by:  dihmeetbN  34670
  Copyright terms: Public domain W3C validator