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

Theorem djajN 34413
Description: Transfer lattice join to  DVecA partial vector space closed subspace join. Part of Lemma M of [Crawley] p. 120 line 29, with closed subspace join rather than subspace sum. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
djaj.k  |-  .\/  =  ( join `  K )
djaj.h  |-  H  =  ( LHyp `  K
)
djaj.i  |-  I  =  ( ( DIsoA `  K
) `  W )
djaj.j  |-  J  =  ( ( vA `  K ) `  W
)
Assertion
Ref Expression
djajN  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  ( X  .\/  Y ) )  =  ( ( I `  X ) J ( I `  Y ) ) )

Proof of Theorem djajN
StepHypRef Expression
1 hllat 32637 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  Lat )
21ad2antrr 730 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  K  e.  Lat )
3 hlop 32636 . . . . . . . . 9  |-  ( K  e.  HL  ->  K  e.  OP )
43ad2antrr 730 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  K  e.  OP )
5 eqid 2429 . . . . . . . . . 10  |-  ( Base `  K )  =  (
Base `  K )
6 djaj.h . . . . . . . . . 10  |-  H  =  ( LHyp `  K
)
7 djaj.i . . . . . . . . . 10  |-  I  =  ( ( DIsoA `  K
) `  W )
85, 6, 7diadmclN 34313 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  X  e.  ( Base `  K
) )
98adantrr 721 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  X  e.  (
Base `  K )
)
10 eqid 2429 . . . . . . . . 9  |-  ( oc
`  K )  =  ( oc `  K
)
115, 10opoccl 32468 . . . . . . . 8  |-  ( ( K  e.  OP  /\  X  e.  ( Base `  K ) )  -> 
( ( oc `  K ) `  X
)  e.  ( Base `  K ) )
124, 9, 11syl2anc 665 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  X )  e.  (
Base `  K )
)
135, 6lhpbase 33271 . . . . . . . . 9  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
1413ad2antlr 731 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  W  e.  (
Base `  K )
)
155, 10opoccl 32468 . . . . . . . 8  |-  ( ( K  e.  OP  /\  W  e.  ( Base `  K ) )  -> 
( ( oc `  K ) `  W
)  e.  ( Base `  K ) )
164, 14, 15syl2anc 665 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  W )  e.  (
Base `  K )
)
17 djaj.k . . . . . . . 8  |-  .\/  =  ( join `  K )
185, 17latjcl 16248 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( ( oc `  K ) `  X
)  e.  ( Base `  K )  /\  (
( oc `  K
) `  W )  e.  ( Base `  K
) )  ->  (
( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) )  e.  ( Base `  K
) )
192, 12, 16, 18syl3anc 1264 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) )  e.  (
Base `  K )
)
20 eqid 2429 . . . . . . 7  |-  ( meet `  K )  =  (
meet `  K )
215, 20latmcl 16249 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  (
( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W )  e.  ( Base `  K
) )
222, 19, 14, 21syl3anc 1264 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  ( Base `  K
) )
235, 6, 7diadmclN 34313 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  Y  e.  dom  I )  ->  Y  e.  ( Base `  K
) )
2423adantrl 720 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  Y  e.  (
Base `  K )
)
255, 10opoccl 32468 . . . . . . . 8  |-  ( ( K  e.  OP  /\  Y  e.  ( Base `  K ) )  -> 
( ( oc `  K ) `  Y
)  e.  ( Base `  K ) )
264, 24, 25syl2anc 665 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  Y )  e.  (
Base `  K )
)
275, 17latjcl 16248 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( ( oc `  K ) `  Y
)  e.  ( Base `  K )  /\  (
( oc `  K
) `  W )  e.  ( Base `  K
) )  ->  (
( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) )  e.  ( Base `  K
) )
282, 26, 16, 27syl3anc 1264 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) )  e.  (
Base `  K )
)
295, 20latmcl 16249 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( ( ( oc
`  K ) `  Y )  .\/  (
( oc `  K
) `  W )
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  (
( ( ( oc
`  K ) `  Y )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W )  e.  ( Base `  K
) )
302, 28, 14, 29syl3anc 1264 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  ( Base `  K
) )
315, 20latmcl 16249 . . . . 5  |-  ( ( K  e.  Lat  /\  ( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  ( Base `  K
)  /\  ( (
( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W )  e.  (
Base `  K )
)  ->  ( (
( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) (
meet `  K )
( ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) )  e.  ( Base `  K ) )
322, 22, 30, 31syl3anc 1264 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( meet `  K ) ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) )  e.  ( Base `  K
) )
33 eqid 2429 . . . . 5  |-  ( le
`  K )  =  ( le `  K
)
345, 33, 20latmle2 16274 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  ( Base `  K
)  /\  ( (
( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W )  e.  (
Base `  K )
)  ->  ( (
( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) (
meet `  K )
( ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ( le `  K ) ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) )
352, 22, 30, 34syl3anc 1264 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( meet `  K ) ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ) ( le `  K ) ( ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) )
365, 33, 20latmle2 16274 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( ( ( oc
`  K ) `  Y )  .\/  (
( oc `  K
) `  W )
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  (
( ( ( oc
`  K ) `  Y )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) ( le `  K ) W )
372, 28, 14, 36syl3anc 1264 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( le `  K
) W )
385, 33, 2, 32, 30, 14, 35, 37lattrd 16255 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( meet `  K ) ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ) ( le `  K ) W )
395, 33, 6, 7diaeldm 34312 . . . . 5  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( meet `  K ) ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) )  e. 
dom  I  <->  ( (
( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) )  e.  ( Base `  K )  /\  (
( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ( le `  K ) W ) ) )
4039adantr 466 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) (
meet `  K )
( ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) )  e.  dom  I  <->  ( ( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) )  e.  ( Base `  K )  /\  (
( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ( le `  K ) W ) ) )
4132, 38, 40mpbir2and 930 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( meet `  K ) ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) )  e. 
dom  I )
42 eqid 2429 . . . 4  |-  ( (
LTrn `  K ) `  W )  =  ( ( LTrn `  K
) `  W )
43 eqid 2429 . . . 4  |-  ( ( ocA `  K ) `
 W )  =  ( ( ocA `  K
) `  W )
4417, 20, 10, 6, 42, 7, 43diaocN 34401 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( meet `  K ) ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) )  e. 
dom  I )  -> 
( I `  (
( ( ( oc
`  K ) `  ( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) )  =  ( ( ( ocA `  K ) `
 W ) `  ( I `  (
( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ) ) )
4541, 44syldan 472 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  ( ( ( ( oc `  K ) `
 ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( meet `  K ) ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ) ) 
.\/  ( ( oc
`  K ) `  W ) ) (
meet `  K ) W ) )  =  ( ( ( ocA `  K ) `  W
) `  ( I `  ( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ) ) )
46 hloml 32631 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  OML )
4746ad2antrr 730 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  K  e.  OML )
485, 17latjcl 16248 . . . . . 6  |-  ( ( K  e.  Lat  /\  X  e.  ( Base `  K )  /\  Y  e.  ( Base `  K
) )  ->  ( X  .\/  Y )  e.  ( Base `  K
) )
492, 9, 24, 48syl3anc 1264 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( X  .\/  Y )  e.  ( Base `  K ) )
5033, 6, 7diadmleN 34314 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  X
( le `  K
) W )
5150adantrr 721 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  X ( le
`  K ) W )
5233, 6, 7diadmleN 34314 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  Y  e.  dom  I )  ->  Y
( le `  K
) W )
5352adantrl 720 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  Y ( le
`  K ) W )
545, 33, 17latjle12 16259 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( X  e.  ( Base `  K )  /\  Y  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) ) )  -> 
( ( X ( le `  K ) W  /\  Y ( le `  K ) W )  <->  ( X  .\/  Y ) ( le
`  K ) W ) )
552, 9, 24, 14, 54syl13anc 1266 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( X ( le `  K
) W  /\  Y
( le `  K
) W )  <->  ( X  .\/  Y ) ( le
`  K ) W ) )
5651, 53, 55mpbi2and 929 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( X  .\/  Y ) ( le `  K ) W )
575, 33, 17, 20, 10omlspjN 32535 . . . . 5  |-  ( ( K  e.  OML  /\  ( ( X  .\/  Y )  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  /\  ( X  .\/  Y ) ( le `  K ) W )  ->  (
( ( X  .\/  Y )  .\/  ( ( oc `  K ) `
 W ) ) ( meet `  K
) W )  =  ( X  .\/  Y
) )
5847, 49, 14, 56, 57syl121anc 1269 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( X  .\/  Y ) 
.\/  ( ( oc
`  K ) `  W ) ) (
meet `  K ) W )  =  ( X  .\/  Y ) )
595, 17latjidm 16271 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( ( oc `  K ) `  W
)  e.  ( Base `  K ) )  -> 
( ( ( oc
`  K ) `  W )  .\/  (
( oc `  K
) `  W )
)  =  ( ( oc `  K ) `
 W ) )
602, 16, 59syl2anc 665 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( oc `  K ) `
 W )  .\/  ( ( oc `  K ) `  W
) )  =  ( ( oc `  K
) `  W )
)
6160oveq2d 6321 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( X 
.\/  Y )  .\/  ( ( ( oc
`  K ) `  W )  .\/  (
( oc `  K
) `  W )
) )  =  ( ( X  .\/  Y
)  .\/  ( ( oc `  K ) `  W ) ) )
625, 17latjass 16292 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( ( X  .\/  Y )  e.  ( Base `  K )  /\  (
( oc `  K
) `  W )  e.  ( Base `  K
)  /\  ( ( oc `  K ) `  W )  e.  (
Base `  K )
) )  ->  (
( ( X  .\/  Y )  .\/  ( ( oc `  K ) `
 W ) ) 
.\/  ( ( oc
`  K ) `  W ) )  =  ( ( X  .\/  Y )  .\/  ( ( ( oc `  K
) `  W )  .\/  ( ( oc `  K ) `  W
) ) ) )
632, 49, 16, 16, 62syl13anc 1266 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( X  .\/  Y ) 
.\/  ( ( oc
`  K ) `  W ) )  .\/  ( ( oc `  K ) `  W
) )  =  ( ( X  .\/  Y
)  .\/  ( (
( oc `  K
) `  W )  .\/  ( ( oc `  K ) `  W
) ) ) )
64 hlol 32635 . . . . . . . . . . 11  |-  ( K  e.  HL  ->  K  e.  OL )
6564ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  K  e.  OL )
665, 17, 20, 10oldmm2 32492 . . . . . . . . . 10  |-  ( ( K  e.  OL  /\  ( X  .\/  Y )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( ( oc `  K ) `  ( ( ( oc
`  K ) `  ( X  .\/  Y ) ) ( meet `  K
) W ) )  =  ( ( X 
.\/  Y )  .\/  ( ( oc `  K ) `  W
) ) )
6765, 49, 14, 66syl3anc 1264 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  ( ( ( oc
`  K ) `  ( X  .\/  Y ) ) ( meet `  K
) W ) )  =  ( ( X 
.\/  Y )  .\/  ( ( oc `  K ) `  W
) ) )
685, 17, 20, 10oldmj1 32495 . . . . . . . . . . . . . 14  |-  ( ( K  e.  OL  /\  X  e.  ( Base `  K )  /\  Y  e.  ( Base `  K
) )  ->  (
( oc `  K
) `  ( X  .\/  Y ) )  =  ( ( ( oc
`  K ) `  X ) ( meet `  K ) ( ( oc `  K ) `
 Y ) ) )
6965, 9, 24, 68syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  ( X  .\/  Y ) )  =  ( ( ( oc `  K
) `  X )
( meet `  K )
( ( oc `  K ) `  Y
) ) )
705, 33, 20latleeqm1 16276 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  Lat  /\  X  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  ( X ( le `  K ) W  <->  ( X
( meet `  K ) W )  =  X ) )
712, 9, 14, 70syl3anc 1264 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( X ( le `  K ) W  <->  ( X (
meet `  K ) W )  =  X ) )
7251, 71mpbid 213 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( X (
meet `  K ) W )  =  X )
7372fveq2d 5885 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  ( X ( meet `  K
) W ) )  =  ( ( oc
`  K ) `  X ) )
745, 17, 20, 10oldmm1 32491 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  OL  /\  X  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  (
( oc `  K
) `  ( X
( meet `  K ) W ) )  =  ( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) )
7565, 9, 14, 74syl3anc 1264 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  ( X ( meet `  K
) W ) )  =  ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) )
7673, 75eqtr3d 2472 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  X )  =  ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) )
775, 33, 20latleeqm1 16276 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  Lat  /\  Y  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  ( Y ( le `  K ) W  <->  ( Y
( meet `  K ) W )  =  Y ) )
782, 24, 14, 77syl3anc 1264 . . . . . . . . . . . . . . . . 17  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( Y ( le `  K ) W  <->  ( Y (
meet `  K ) W )  =  Y ) )
7953, 78mpbid 213 . . . . . . . . . . . . . . . 16  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( Y (
meet `  K ) W )  =  Y )
8079fveq2d 5885 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  ( Y ( meet `  K
) W ) )  =  ( ( oc
`  K ) `  Y ) )
815, 17, 20, 10oldmm1 32491 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  OL  /\  Y  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  (
( oc `  K
) `  ( Y
( meet `  K ) W ) )  =  ( ( ( oc
`  K ) `  Y )  .\/  (
( oc `  K
) `  W )
) )
8265, 24, 14, 81syl3anc 1264 . . . . . . . . . . . . . . 15  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  ( Y ( meet `  K
) W ) )  =  ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) )
8380, 82eqtr3d 2472 . . . . . . . . . . . . . 14  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  Y )  =  ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) )
8476, 83oveq12d 6323 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( oc `  K ) `
 X ) (
meet `  K )
( ( oc `  K ) `  Y
) )  =  ( ( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) ) )
8569, 84eqtrd 2470 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  ( X  .\/  Y ) )  =  ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K )
( ( ( oc
`  K ) `  Y )  .\/  (
( oc `  K
) `  W )
) ) )
8685oveq1d 6320 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( oc `  K ) `
 ( X  .\/  Y ) ) ( meet `  K ) W )  =  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K )
( ( ( oc
`  K ) `  Y )  .\/  (
( oc `  K
) `  W )
) ) ( meet `  K ) W ) )
875, 20latmmdir 32509 . . . . . . . . . . . 12  |-  ( ( K  e.  OL  /\  ( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) )  e.  (
Base `  K )  /\  ( ( ( oc
`  K ) `  Y )  .\/  (
( oc `  K
) `  W )
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) ) )  -> 
( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ) (
meet `  K ) W )  =  ( ( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )
8865, 19, 28, 14, 87syl13anc 1266 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K )
( ( ( oc
`  K ) `  Y )  .\/  (
( oc `  K
) `  W )
) ) ( meet `  K ) W )  =  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( meet `  K ) ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ) )
8986, 88eqtrd 2470 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( oc `  K ) `
 ( X  .\/  Y ) ) ( meet `  K ) W )  =  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( meet `  K ) ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ) )
9089fveq2d 5885 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( oc
`  K ) `  ( ( ( oc
`  K ) `  ( X  .\/  Y ) ) ( meet `  K
) W ) )  =  ( ( oc
`  K ) `  ( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ) )
9167, 90eqtr3d 2472 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( X 
.\/  Y )  .\/  ( ( oc `  K ) `  W
) )  =  ( ( oc `  K
) `  ( (
( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) (
meet `  K )
( ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ) )
9291oveq1d 6320 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( X  .\/  Y ) 
.\/  ( ( oc
`  K ) `  W ) )  .\/  ( ( oc `  K ) `  W
) )  =  ( ( ( oc `  K ) `  (
( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  .\/  (
( oc `  K
) `  W )
) )
9363, 92eqtr3d 2472 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( X 
.\/  Y )  .\/  ( ( ( oc
`  K ) `  W )  .\/  (
( oc `  K
) `  W )
) )  =  ( ( ( oc `  K ) `  (
( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  .\/  (
( oc `  K
) `  W )
) )
9461, 93eqtr3d 2472 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( X 
.\/  Y )  .\/  ( ( oc `  K ) `  W
) )  =  ( ( ( oc `  K ) `  (
( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  .\/  (
( oc `  K
) `  W )
) )
9594oveq1d 6320 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( X  .\/  Y ) 
.\/  ( ( oc
`  K ) `  W ) ) (
meet `  K ) W )  =  ( ( ( ( oc
`  K ) `  ( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) )
9658, 95eqtr3d 2472 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( X  .\/  Y )  =  ( ( ( ( oc `  K ) `  (
( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) )
9796fveq2d 5885 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  ( X  .\/  Y ) )  =  ( I `
 ( ( ( ( oc `  K
) `  ( (
( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) (
meet `  K )
( ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) ) )
98 simpl 458 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
996, 7diaclN 34326 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
I `  X )  e.  ran  I )
10099adantrr 721 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  X )  e.  ran  I )
1016, 42, 7diaelrnN 34321 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( I `  X )  e.  ran  I )  ->  (
I `  X )  C_  ( ( LTrn `  K
) `  W )
)
102100, 101syldan 472 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  X )  C_  (
( LTrn `  K ) `  W ) )
1036, 7diaclN 34326 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  Y  e.  dom  I )  ->  (
I `  Y )  e.  ran  I )
104103adantrl 720 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  Y )  e.  ran  I )
1056, 42, 7diaelrnN 34321 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( I `  Y )  e.  ran  I )  ->  (
I `  Y )  C_  ( ( LTrn `  K
) `  W )
)
106104, 105syldan 472 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  Y )  C_  (
( LTrn `  K ) `  W ) )
107 djaj.j . . . . 5  |-  J  =  ( ( vA `  K ) `  W
)
1086, 42, 7, 43, 107djavalN 34411 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( I `
 X )  C_  ( ( LTrn `  K
) `  W )  /\  ( I `  Y
)  C_  ( ( LTrn `  K ) `  W ) ) )  ->  ( ( I `
 X ) J ( I `  Y
) )  =  ( ( ( ocA `  K
) `  W ) `  ( ( ( ( ocA `  K ) `
 W ) `  ( I `  X
) )  i^i  (
( ( ocA `  K
) `  W ) `  ( I `  Y
) ) ) ) )
10998, 102, 106, 108syl12anc 1262 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( I `
 X ) J ( I `  Y
) )  =  ( ( ( ocA `  K
) `  W ) `  ( ( ( ( ocA `  K ) `
 W ) `  ( I `  X
) )  i^i  (
( ( ocA `  K
) `  W ) `  ( I `  Y
) ) ) ) )
1105, 33, 20latmle2 16274 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  ->  (
( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) ( le `  K ) W )
1112, 19, 14, 110syl3anc 1264 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( le `  K
) W )
1125, 33, 6, 7diaeldm 34312 . . . . . . . 8  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  dom  I  <->  ( (
( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W )  e.  ( Base `  K
)  /\  ( (
( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( le
`  K ) W ) ) )
113112adantr 466 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W )  e.  dom  I 
<->  ( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  ( Base `  K
)  /\  ( (
( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( le
`  K ) W ) ) )
11422, 111, 113mpbir2and 930 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  dom  I )
1155, 33, 6, 7diaeldm 34312 . . . . . . . 8  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  dom  I  <->  ( (
( ( ( oc
`  K ) `  Y )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W )  e.  ( Base `  K
)  /\  ( (
( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( le
`  K ) W ) ) )
116115adantr 466 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W )  e.  dom  I 
<->  ( ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  ( Base `  K
)  /\  ( (
( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) ( le
`  K ) W ) ) )
11730, 37, 116mpbir2and 930 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  dom  I )
11820, 6, 7diameetN 34332 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( ( ( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W )  e.  dom  I  /\  ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W )  e.  dom  I ) )  ->  ( I `  ( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  =  ( ( I `  (
( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) )  i^i  ( I `  ( ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ) )
11998, 114, 117, 118syl12anc 1262 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  ( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  =  ( ( I `  (
( ( ( oc
`  K ) `  X )  .\/  (
( oc `  K
) `  W )
) ( meet `  K
) W ) )  i^i  ( I `  ( ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ) )
12017, 20, 10, 6, 42, 7, 43diaocN 34401 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  X  e.  dom  I )  ->  (
I `  ( (
( ( oc `  K ) `  X
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) )  =  ( ( ( ocA `  K ) `  W
) `  ( I `  X ) ) )
121120adantrr 721 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  ( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) )  =  ( ( ( ocA `  K
) `  W ) `  ( I `  X
) ) )
12217, 20, 10, 6, 42, 7, 43diaocN 34401 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  Y  e.  dom  I )  ->  (
I `  ( (
( ( oc `  K ) `  Y
)  .\/  ( ( oc `  K ) `  W ) ) (
meet `  K ) W ) )  =  ( ( ( ocA `  K ) `  W
) `  ( I `  Y ) ) )
123122adantrl 720 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  ( ( ( ( oc `  K ) `
 Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) )  =  ( ( ( ocA `  K
) `  W ) `  ( I `  Y
) ) )
124121, 123ineq12d 3671 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( I `
 ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) )  i^i  ( I `
 ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  =  ( ( ( ( ocA `  K ) `  W
) `  ( I `  X ) )  i^i  ( ( ( ocA `  K ) `  W
) `  ( I `  Y ) ) ) )
125119, 124eqtrd 2470 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  ( ( ( ( ( oc `  K
) `  X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) )  =  ( ( ( ( ocA `  K ) `  W
) `  ( I `  X ) )  i^i  ( ( ( ocA `  K ) `  W
) `  ( I `  Y ) ) ) )
126125fveq2d 5885 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( ( ocA `  K ) `
 W ) `  ( I `  (
( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ) )  =  ( ( ( ocA `  K ) `  W
) `  ( (
( ( ocA `  K
) `  W ) `  ( I `  X
) )  i^i  (
( ( ocA `  K
) `  W ) `  ( I `  Y
) ) ) ) )
127109, 126eqtr4d 2473 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( ( I `
 X ) J ( I `  Y
) )  =  ( ( ( ocA `  K
) `  W ) `  ( I `  (
( ( ( ( oc `  K ) `
 X )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ( meet `  K
) ( ( ( ( oc `  K
) `  Y )  .\/  ( ( oc `  K ) `  W
) ) ( meet `  K ) W ) ) ) ) )
12845, 97, 1273eqtr4d 2480 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( X  e. 
dom  I  /\  Y  e.  dom  I ) )  ->  ( I `  ( X  .\/  Y ) )  =  ( ( I `  X ) J ( I `  Y ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1870    i^i cin 3441    C_ wss 3442   class class class wbr 4426   dom cdm 4854   ran crn 4855   ` cfv 5601  (class class class)co 6305   Basecbs 15084   lecple 15159   occoc 15160   joincjn 16140   meetcmee 16141   Latclat 16242   OPcops 32446   OLcol 32448   OMLcoml 32449   HLchlt 32624   LHypclh 33257   LTrncltrn 33374   DIsoAcdia 34304   ocAcocaN 34395   vAcdjaN 34407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-riotaBAD 32233
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1st 6807  df-2nd 6808  df-undef 7028  df-map 7482  df-preset 16124  df-poset 16142  df-plt 16155  df-lub 16171  df-glb 16172  df-join 16173  df-meet 16174  df-p0 16236  df-p1 16237  df-lat 16243  df-clat 16305  df-oposet 32450  df-cmtN 32451  df-ol 32452  df-oml 32453  df-covers 32540  df-ats 32541  df-atl 32572  df-cvlat 32596  df-hlat 32625  df-llines 32771  df-lplanes 32772  df-lvols 32773  df-lines 32774  df-psubsp 32776  df-pmap 32777  df-padd 33069  df-lhyp 33261  df-laut 33262  df-ldil 33377  df-ltrn 33378  df-trl 33433  df-disoa 34305  df-docaN 34396  df-djaN 34408
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator