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

Theorem djajN 36947
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 35172 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ Lat)
21ad2antrr 697 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ Lat)
3 hlop 35171 . . . . . . . . 9 (𝐾 ∈ HL → 𝐾 ∈ OP)
43ad2antrr 697 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OP)
5 eqid 2771 . . . . . . . . . 10 (Base‘𝐾) = (Base‘𝐾)
6 djaj.h . . . . . . . . . 10 𝐻 = (LHyp‘𝐾)
7 djaj.i . . . . . . . . . 10 𝐼 = ((DIsoA‘𝐾)‘𝑊)
85, 6, 7diadmclN 36847 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ (Base‘𝐾))
98adantrr 688 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑋 ∈ (Base‘𝐾))
10 eqid 2771 . . . . . . . . 9 (oc‘𝐾) = (oc‘𝐾)
115, 10opoccl 35003 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑋 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
124, 9, 11syl2anc 565 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
135, 6lhpbase 35806 . . . . . . . . 9 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
1413ad2antlr 698 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑊 ∈ (Base‘𝐾))
155, 10opoccl 35003 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))
164, 14, 15syl2anc 565 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))
17 djaj.k . . . . . . . 8 = (join‘𝐾)
185, 17latjcl 17259 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
192, 12, 16, 18syl3anc 1476 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
20 eqid 2771 . . . . . . 7 (meet‘𝐾) = (meet‘𝐾)
215, 20latmcl 17260 . . . . . 6 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
222, 19, 14, 21syl3anc 1476 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
235, 6, 7diadmclN 36847 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌 ∈ (Base‘𝐾))
2423adantrl 687 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑌 ∈ (Base‘𝐾))
255, 10opoccl 35003 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
264, 24, 25syl2anc 565 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
275, 17latjcl 17259 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
282, 26, 16, 27syl3anc 1476 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
295, 20latmcl 17260 . . . . . 6 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
302, 28, 14, 29syl3anc 1476 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
315, 20latmcl 17260 . . . . 5 ((𝐾 ∈ Lat ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))
322, 22, 30, 31syl3anc 1476 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))
33 eqid 2771 . . . . 5 (le‘𝐾) = (le‘𝐾)
345, 33, 20latmle2 17285 . . . . . 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 1476 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
365, 33, 20latmle2 17285 . . . . . 6 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
372, 28, 14, 36syl3anc 1476 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
385, 33, 2, 32, 30, 14, 35, 37lattrd 17266 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)𝑊)
395, 33, 6, 7diaeldm 36846 . . . . 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 466 . . . 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 684 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ dom 𝐼)
42 eqid 2771 . . . 4 ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
43 eqid 2771 . . . 4 ((ocA‘𝐾)‘𝑊) = ((ocA‘𝐾)‘𝑊)
4417, 20, 10, 6, 42, 7, 43diaocN 36935 . . 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 571 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
46 hloml 35166 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ OML)
4746ad2antrr 697 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OML)
485, 17latjcl 17259 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 𝑌) ∈ (Base‘𝐾))
492, 9, 24, 48syl3anc 1476 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋 𝑌) ∈ (Base‘𝐾))
5033, 6, 7diadmleN 36848 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋(le‘𝐾)𝑊)
5150adantrr 688 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑋(le‘𝐾)𝑊)
5233, 6, 7diadmleN 36848 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌(le‘𝐾)𝑊)
5352adantrl 687 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑌(le‘𝐾)𝑊)
545, 33, 17latjle12 17270 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑋(le‘𝐾)𝑊𝑌(le‘𝐾)𝑊) ↔ (𝑋 𝑌)(le‘𝐾)𝑊))
552, 9, 24, 14, 54syl13anc 1478 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋(le‘𝐾)𝑊𝑌(le‘𝐾)𝑊) ↔ (𝑋 𝑌)(le‘𝐾)𝑊))
5651, 53, 55mpbi2and 683 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋 𝑌)(le‘𝐾)𝑊)
575, 33, 17, 20, 10omlspjN 35070 . . . . 5 ((𝐾 ∈ OML ∧ ((𝑋 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ (𝑋 𝑌)(le‘𝐾)𝑊) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 𝑌))
5847, 49, 14, 56, 57syl121anc 1481 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 𝑌))
595, 17latjidm 17282 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
602, 16, 59syl2anc 565 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
6160oveq2d 6809 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))) = ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)))
625, 17latjass 17303 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((𝑋 𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) ((oc‘𝐾)‘𝑊)) = ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))))
632, 49, 16, 16, 62syl13anc 1478 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) ((oc‘𝐾)‘𝑊)) = ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))))
64 hlol 35170 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
6564ad2antrr 697 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OL)
665, 17, 20, 10oldmm2 35027 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ (𝑋 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)))
6765, 49, 14, 66syl3anc 1476 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)))
685, 17, 20, 10oldmj1 35030 . . . . . . . . . . . . . 14 ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))
6965, 9, 24, 68syl3anc 1476 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))
705, 33, 20latleeqm1 17287 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋))
712, 9, 14, 70syl3anc 1476 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋))
7251, 71mpbid 222 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋(meet‘𝐾)𝑊) = 𝑋)
7372fveq2d 6336 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑋))
745, 17, 20, 10oldmm1 35026 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)))
7565, 9, 14, 74syl3anc 1476 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)))
7673, 75eqtr3d 2807 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)))
775, 33, 20latleeqm1 17287 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌))
782, 24, 14, 77syl3anc 1476 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌))
7953, 78mpbid 222 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑌(meet‘𝐾)𝑊) = 𝑌)
8079fveq2d 6336 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑌))
815, 17, 20, 10oldmm1 35026 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OL ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))
8265, 24, 14, 81syl3anc 1476 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))
8380, 82eqtr3d 2807 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))
8476, 83oveq12d 6811 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))))
8569, 84eqtrd 2805 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 𝑌)) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))))
8685oveq1d 6808 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊))
875, 20latmmdir 35044 . . . . . . . . . . . 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 1478 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
8986, 88eqtrd 2805 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
9089fveq2d 6336 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
9167, 90eqtr3d 2807 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
9291oveq1d 6808 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊)))
9363, 92eqtr3d 2807 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊)))
9461, 93eqtr3d 2807 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊)))
9594oveq1d 6808 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
9658, 95eqtr3d 2807 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋 𝑌) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
9796fveq2d 6336 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 𝑌)) = (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
98 simpl 468 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
996, 7diaclN 36860 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼𝑋) ∈ ran 𝐼)
10099adantrr 688 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑋) ∈ ran 𝐼)
1016, 42, 7diaelrnN 36855 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐼𝑋) ∈ ran 𝐼) → (𝐼𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
102100, 101syldan 571 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
1036, 7diaclN 36860 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼𝑌) ∈ ran 𝐼)
104103adantrl 687 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑌) ∈ ran 𝐼)
1056, 42, 7diaelrnN 36855 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐼𝑌) ∈ ran 𝐼) → (𝐼𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))
106104, 105syldan 571 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))
107 djaj.j . . . . 5 𝐽 = ((vA‘𝐾)‘𝑊)
1086, 42, 7, 43, 107djavalN 36945 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐼𝑋) ⊆ ((LTrn‘𝐾)‘𝑊) ∧ (𝐼𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))) → ((𝐼𝑋)𝐽(𝐼𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))))
10998, 102, 106, 108syl12anc 1474 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝐼𝑋)𝐽(𝐼𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))))
1105, 33, 20latmle2 17285 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
1112, 19, 14, 110syl3anc 1476 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
1125, 33, 6, 7diaeldm 36846 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
113112adantr 466 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
11422, 111, 113mpbir2and 684 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)
1155, 33, 6, 7diaeldm 36846 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
116115adantr 466 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
11730, 37, 116mpbir2and 684 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)
11820, 6, 7diameetN 36866 . . . . . 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 1474 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
12017, 20, 10, 6, 42, 7, 43diaocN 36935 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)))
121120adantrr 688 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)))
12217, 20, 10, 6, 42, 7, 43diaocN 36935 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))
123122adantrl 687 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))
124121, 123ineq12d 3966 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌))))
125119, 124eqtrd 2805 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌))))
126125fveq2d 6336 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))))
127109, 126eqtr4d 2808 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝐼𝑋)𝐽(𝐼𝑌)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
12845, 97, 1273eqtr4d 2815 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 𝑌)) = ((𝐼𝑋)𝐽(𝐼𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  cin 3722  wss 3723   class class class wbr 4786  dom cdm 5249  ran crn 5250  cfv 6031  (class class class)co 6793  Basecbs 16064  lecple 16156  occoc 16157  joincjn 17152  meetcmee 17153  Latclat 17253  OPcops 34981  OLcol 34983  OMLcoml 34984  HLchlt 35159  LHypclh 35792  LTrncltrn 35909  DIsoAcdia 36838  ocAcocaN 36929  vAcdjaN 36941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-riotaBAD 34761
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-1st 7315  df-2nd 7316  df-undef 7551  df-map 8011  df-preset 17136  df-poset 17154  df-plt 17166  df-lub 17182  df-glb 17183  df-join 17184  df-meet 17185  df-p0 17247  df-p1 17248  df-lat 17254  df-clat 17316  df-oposet 34985  df-cmtN 34986  df-ol 34987  df-oml 34988  df-covers 35075  df-ats 35076  df-atl 35107  df-cvlat 35131  df-hlat 35160  df-llines 35306  df-lplanes 35307  df-lvols 35308  df-lines 35309  df-psubsp 35311  df-pmap 35312  df-padd 35604  df-lhyp 35796  df-laut 35797  df-ldil 35912  df-ltrn 35913  df-trl 35968  df-disoa 36839  df-docaN 36930  df-djaN 36942
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator