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

Theorem djajN 38452
 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‘𝐾)
djaj.h 𝐻 = (LHyp‘𝐾)
djaj.i 𝐼 = ((DIsoA‘𝐾)‘𝑊)
djaj.j 𝐽 = ((vA‘𝐾)‘𝑊)
Assertion
Ref Expression
djajN (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 𝑌)) = ((𝐼𝑋)𝐽(𝐼𝑌)))

Proof of Theorem djajN
StepHypRef Expression
1 hllat 36678 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ Lat)
21ad2antrr 725 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ Lat)
3 hlop 36677 . . . . . . . . 9 (𝐾 ∈ HL → 𝐾 ∈ OP)
43ad2antrr 725 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OP)
5 eqid 2798 . . . . . . . . . 10 (Base‘𝐾) = (Base‘𝐾)
6 djaj.h . . . . . . . . . 10 𝐻 = (LHyp‘𝐾)
7 djaj.i . . . . . . . . . 10 𝐼 = ((DIsoA‘𝐾)‘𝑊)
85, 6, 7diadmclN 38352 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ (Base‘𝐾))
98adantrr 716 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑋 ∈ (Base‘𝐾))
10 eqid 2798 . . . . . . . . 9 (oc‘𝐾) = (oc‘𝐾)
115, 10opoccl 36509 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑋 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
124, 9, 11syl2anc 587 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
135, 6lhpbase 37313 . . . . . . . . 9 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
1413ad2antlr 726 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑊 ∈ (Base‘𝐾))
155, 10opoccl 36509 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))
164, 14, 15syl2anc 587 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))
17 djaj.k . . . . . . . 8 = (join‘𝐾)
185, 17latjcl 17656 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
192, 12, 16, 18syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
20 eqid 2798 . . . . . . 7 (meet‘𝐾) = (meet‘𝐾)
215, 20latmcl 17657 . . . . . 6 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
222, 19, 14, 21syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
235, 6, 7diadmclN 38352 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌 ∈ (Base‘𝐾))
2423adantrl 715 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑌 ∈ (Base‘𝐾))
255, 10opoccl 36509 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
264, 24, 25syl2anc 587 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
275, 17latjcl 17656 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
282, 26, 16, 27syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
295, 20latmcl 17657 . . . . . 6 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
302, 28, 14, 29syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
315, 20latmcl 17657 . . . . 5 ((𝐾 ∈ Lat ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))
322, 22, 30, 31syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))
33 eqid 2798 . . . . 5 (le‘𝐾) = (le‘𝐾)
345, 33, 20latmle2 17682 . . . . . 6 ((𝐾 ∈ Lat ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
352, 22, 30, 34syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
365, 33, 20latmle2 17682 . . . . . 6 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
372, 28, 14, 36syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
385, 33, 2, 32, 30, 14, 35, 37lattrd 17663 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)𝑊)
395, 33, 6, 7diaeldm 38351 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ dom 𝐼 ↔ ((((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾) ∧ (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)𝑊)))
4039adantr 484 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ dom 𝐼 ↔ ((((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾) ∧ (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)𝑊)))
4132, 38, 40mpbir2and 712 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ dom 𝐼)
42 eqid 2798 . . . 4 ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
43 eqid 2798 . . . 4 ((ocA‘𝐾)‘𝑊) = ((ocA‘𝐾)‘𝑊)
4417, 20, 10, 6, 42, 7, 43diaocN 38440 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
4541, 44syldan 594 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
46 hloml 36672 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ OML)
4746ad2antrr 725 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OML)
485, 17latjcl 17656 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 𝑌) ∈ (Base‘𝐾))
492, 9, 24, 48syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋 𝑌) ∈ (Base‘𝐾))
5033, 6, 7diadmleN 38353 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋(le‘𝐾)𝑊)
5150adantrr 716 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑋(le‘𝐾)𝑊)
5233, 6, 7diadmleN 38353 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌(le‘𝐾)𝑊)
5352adantrl 715 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑌(le‘𝐾)𝑊)
545, 33, 17latjle12 17667 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑋(le‘𝐾)𝑊𝑌(le‘𝐾)𝑊) ↔ (𝑋 𝑌)(le‘𝐾)𝑊))
552, 9, 24, 14, 54syl13anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋(le‘𝐾)𝑊𝑌(le‘𝐾)𝑊) ↔ (𝑋 𝑌)(le‘𝐾)𝑊))
5651, 53, 55mpbi2and 711 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋 𝑌)(le‘𝐾)𝑊)
575, 33, 17, 20, 10omlspjN 36576 . . . . 5 ((𝐾 ∈ OML ∧ ((𝑋 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ (𝑋 𝑌)(le‘𝐾)𝑊) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 𝑌))
5847, 49, 14, 56, 57syl121anc 1372 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 𝑌))
595, 17latjidm 17679 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
602, 16, 59syl2anc 587 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
6160oveq2d 7152 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))) = ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)))
625, 17latjass 17700 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((𝑋 𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) ((oc‘𝐾)‘𝑊)) = ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))))
632, 49, 16, 16, 62syl13anc 1369 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) ((oc‘𝐾)‘𝑊)) = ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))))
64 hlol 36676 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
6564ad2antrr 725 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OL)
665, 17, 20, 10oldmm2 36533 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ (𝑋 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)))
6765, 49, 14, 66syl3anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)))
685, 17, 20, 10oldmj1 36536 . . . . . . . . . . . . . 14 ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))
6965, 9, 24, 68syl3anc 1368 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))
705, 33, 20latleeqm1 17684 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋))
712, 9, 14, 70syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋))
7251, 71mpbid 235 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋(meet‘𝐾)𝑊) = 𝑋)
7372fveq2d 6650 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑋))
745, 17, 20, 10oldmm1 36532 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)))
7565, 9, 14, 74syl3anc 1368 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)))
7673, 75eqtr3d 2835 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)))
775, 33, 20latleeqm1 17684 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌))
782, 24, 14, 77syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌))
7953, 78mpbid 235 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑌(meet‘𝐾)𝑊) = 𝑌)
8079fveq2d 6650 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑌))
815, 17, 20, 10oldmm1 36532 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OL ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))
8265, 24, 14, 81syl3anc 1368 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))
8380, 82eqtr3d 2835 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))
8476, 83oveq12d 7154 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))))
8569, 84eqtrd 2833 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 𝑌)) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))))
8685oveq1d 7151 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊))
875, 20latmmdir 36550 . . . . . . . . . . . 12 ((𝐾 ∈ OL ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
8865, 19, 28, 14, 87syl13anc 1369 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
8986, 88eqtrd 2833 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
9089fveq2d 6650 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
9167, 90eqtr3d 2835 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
9291oveq1d 7151 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊)))
9363, 92eqtr3d 2835 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊)))
9461, 93eqtr3d 2835 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊)))
9594oveq1d 7151 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
9658, 95eqtr3d 2835 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋 𝑌) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
9796fveq2d 6650 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 𝑌)) = (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
98 simpl 486 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
996, 7diaclN 38365 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼𝑋) ∈ ran 𝐼)
10099adantrr 716 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑋) ∈ ran 𝐼)
1016, 42, 7diaelrnN 38360 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐼𝑋) ∈ ran 𝐼) → (𝐼𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
102100, 101syldan 594 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
1036, 7diaclN 38365 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼𝑌) ∈ ran 𝐼)
104103adantrl 715 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑌) ∈ ran 𝐼)
1056, 42, 7diaelrnN 38360 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐼𝑌) ∈ ran 𝐼) → (𝐼𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))
106104, 105syldan 594 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))
107 djaj.j . . . . 5 𝐽 = ((vA‘𝐾)‘𝑊)
1086, 42, 7, 43, 107djavalN 38450 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐼𝑋) ⊆ ((LTrn‘𝐾)‘𝑊) ∧ (𝐼𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))) → ((𝐼𝑋)𝐽(𝐼𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))))
10998, 102, 106, 108syl12anc 835 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝐼𝑋)𝐽(𝐼𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))))
1105, 33, 20latmle2 17682 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
1112, 19, 14, 110syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
1125, 33, 6, 7diaeldm 38351 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
113112adantr 484 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
11422, 111, 113mpbir2and 712 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)
1155, 33, 6, 7diaeldm 38351 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
116115adantr 484 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
11730, 37, 116mpbir2and 712 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)
11820, 6, 7diameetN 38371 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
11998, 114, 117, 118syl12anc 835 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
12017, 20, 10, 6, 42, 7, 43diaocN 38440 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)))
121120adantrr 716 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)))
12217, 20, 10, 6, 42, 7, 43diaocN 38440 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))
123122adantrl 715 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))
124121, 123ineq12d 4140 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌))))
125119, 124eqtrd 2833 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌))))
126125fveq2d 6650 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))))
127109, 126eqtr4d 2836 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝐼𝑋)𝐽(𝐼𝑌)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
12845, 97, 1273eqtr4d 2843 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 𝑌)) = ((𝐼𝑋)𝐽(𝐼𝑌)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∩ cin 3880   ⊆ wss 3881   class class class wbr 5031  dom cdm 5520  ran crn 5521  ‘cfv 6325  (class class class)co 7136  Basecbs 16478  lecple 16567  occoc 16568  joincjn 17549  meetcmee 17550  Latclat 17650  OPcops 36487  OLcol 36489  OMLcoml 36490  HLchlt 36665  LHypclh 37299  LTrncltrn 37416  DIsoAcdia 38343  ocAcocaN 38434  vAcdjaN 38446 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-riotaBAD 36268 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5426  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-1st 7674  df-2nd 7675  df-undef 7925  df-map 8394  df-proset 17533  df-poset 17551  df-plt 17563  df-lub 17579  df-glb 17580  df-join 17581  df-meet 17582  df-p0 17644  df-p1 17645  df-lat 17651  df-clat 17713  df-oposet 36491  df-cmtN 36492  df-ol 36493  df-oml 36494  df-covers 36581  df-ats 36582  df-atl 36613  df-cvlat 36637  df-hlat 36666  df-llines 36813  df-lplanes 36814  df-lvols 36815  df-lines 36816  df-psubsp 36818  df-pmap 36819  df-padd 37111  df-lhyp 37303  df-laut 37304  df-ldil 37419  df-ltrn 37420  df-trl 37474  df-disoa 38344  df-docaN 38435  df-djaN 38447 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator