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 37116
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 35342 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ Lat)
21ad2antrr 717 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ Lat)
3 hlop 35341 . . . . . . . . 9 (𝐾 ∈ HL → 𝐾 ∈ OP)
43ad2antrr 717 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OP)
5 eqid 2765 . . . . . . . . . 10 (Base‘𝐾) = (Base‘𝐾)
6 djaj.h . . . . . . . . . 10 𝐻 = (LHyp‘𝐾)
7 djaj.i . . . . . . . . . 10 𝐼 = ((DIsoA‘𝐾)‘𝑊)
85, 6, 7diadmclN 37016 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ (Base‘𝐾))
98adantrr 708 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑋 ∈ (Base‘𝐾))
10 eqid 2765 . . . . . . . . 9 (oc‘𝐾) = (oc‘𝐾)
115, 10opoccl 35173 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑋 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
124, 9, 11syl2anc 579 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
135, 6lhpbase 35977 . . . . . . . . 9 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
1413ad2antlr 718 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑊 ∈ (Base‘𝐾))
155, 10opoccl 35173 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))
164, 14, 15syl2anc 579 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))
17 djaj.k . . . . . . . 8 = (join‘𝐾)
185, 17latjcl 17333 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
192, 12, 16, 18syl3anc 1490 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
20 eqid 2765 . . . . . . 7 (meet‘𝐾) = (meet‘𝐾)
215, 20latmcl 17334 . . . . . 6 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
222, 19, 14, 21syl3anc 1490 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
235, 6, 7diadmclN 37016 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌 ∈ (Base‘𝐾))
2423adantrl 707 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑌 ∈ (Base‘𝐾))
255, 10opoccl 35173 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
264, 24, 25syl2anc 579 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
275, 17latjcl 17333 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
282, 26, 16, 27syl3anc 1490 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
295, 20latmcl 17334 . . . . . 6 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
302, 28, 14, 29syl3anc 1490 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
315, 20latmcl 17334 . . . . 5 ((𝐾 ∈ Lat ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))
322, 22, 30, 31syl3anc 1490 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))
33 eqid 2765 . . . . 5 (le‘𝐾) = (le‘𝐾)
345, 33, 20latmle2 17359 . . . . . 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 1490 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
365, 33, 20latmle2 17359 . . . . . 6 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
372, 28, 14, 36syl3anc 1490 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
385, 33, 2, 32, 30, 14, 35, 37lattrd 17340 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)𝑊)
395, 33, 6, 7diaeldm 37015 . . . . 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 472 . . . 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 704 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ dom 𝐼)
42 eqid 2765 . . . 4 ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
43 eqid 2765 . . . 4 ((ocA‘𝐾)‘𝑊) = ((ocA‘𝐾)‘𝑊)
4417, 20, 10, 6, 42, 7, 43diaocN 37104 . . 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 585 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
46 hloml 35336 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ OML)
4746ad2antrr 717 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OML)
485, 17latjcl 17333 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 𝑌) ∈ (Base‘𝐾))
492, 9, 24, 48syl3anc 1490 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋 𝑌) ∈ (Base‘𝐾))
5033, 6, 7diadmleN 37017 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋(le‘𝐾)𝑊)
5150adantrr 708 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑋(le‘𝐾)𝑊)
5233, 6, 7diadmleN 37017 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌(le‘𝐾)𝑊)
5352adantrl 707 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝑌(le‘𝐾)𝑊)
545, 33, 17latjle12 17344 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑋(le‘𝐾)𝑊𝑌(le‘𝐾)𝑊) ↔ (𝑋 𝑌)(le‘𝐾)𝑊))
552, 9, 24, 14, 54syl13anc 1491 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋(le‘𝐾)𝑊𝑌(le‘𝐾)𝑊) ↔ (𝑋 𝑌)(le‘𝐾)𝑊))
5651, 53, 55mpbi2and 703 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋 𝑌)(le‘𝐾)𝑊)
575, 33, 17, 20, 10omlspjN 35240 . . . . 5 ((𝐾 ∈ OML ∧ ((𝑋 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ (𝑋 𝑌)(le‘𝐾)𝑊) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 𝑌))
5847, 49, 14, 56, 57syl121anc 1494 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 𝑌))
595, 17latjidm 17356 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
602, 16, 59syl2anc 579 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
6160oveq2d 6862 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))) = ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)))
625, 17latjass 17377 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((𝑋 𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) ((oc‘𝐾)‘𝑊)) = ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))))
632, 49, 16, 16, 62syl13anc 1491 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) ((oc‘𝐾)‘𝑊)) = ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))))
64 hlol 35340 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ OL)
6564ad2antrr 717 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OL)
665, 17, 20, 10oldmm2 35197 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ (𝑋 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)))
6765, 49, 14, 66syl3anc 1490 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)))
685, 17, 20, 10oldmj1 35200 . . . . . . . . . . . . . 14 ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))
6965, 9, 24, 68syl3anc 1490 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))
705, 33, 20latleeqm1 17361 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋))
712, 9, 14, 70syl3anc 1490 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋))
7251, 71mpbid 223 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋(meet‘𝐾)𝑊) = 𝑋)
7372fveq2d 6383 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑋))
745, 17, 20, 10oldmm1 35196 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)))
7565, 9, 14, 74syl3anc 1490 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)))
7673, 75eqtr3d 2801 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)))
775, 33, 20latleeqm1 17361 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌))
782, 24, 14, 77syl3anc 1490 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌))
7953, 78mpbid 223 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑌(meet‘𝐾)𝑊) = 𝑌)
8079fveq2d 6383 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑌))
815, 17, 20, 10oldmm1 35196 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OL ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))
8265, 24, 14, 81syl3anc 1490 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))
8380, 82eqtr3d 2801 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))
8476, 83oveq12d 6864 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))))
8569, 84eqtrd 2799 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 𝑌)) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))))
8685oveq1d 6861 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊))
875, 20latmmdir 35214 . . . . . . . . . . . 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 1491 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
8986, 88eqtrd 2799 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
9089fveq2d 6383 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 𝑌))(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
9167, 90eqtr3d 2801 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
9291oveq1d 6861 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊)))
9363, 92eqtr3d 2801 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) (((oc‘𝐾)‘𝑊) ((oc‘𝐾)‘𝑊))) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊)))
9461, 93eqtr3d 2801 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝑋 𝑌) ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊)))
9594oveq1d 6861 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((𝑋 𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
9658, 95eqtr3d 2801 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝑋 𝑌) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
9796fveq2d 6383 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 𝑌)) = (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
98 simpl 474 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
996, 7diaclN 37029 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼𝑋) ∈ ran 𝐼)
10099adantrr 708 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑋) ∈ ran 𝐼)
1016, 42, 7diaelrnN 37024 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐼𝑋) ∈ ran 𝐼) → (𝐼𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
102100, 101syldan 585 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
1036, 7diaclN 37029 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼𝑌) ∈ ran 𝐼)
104103adantrl 707 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑌) ∈ ran 𝐼)
1056, 42, 7diaelrnN 37024 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐼𝑌) ∈ ran 𝐼) → (𝐼𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))
106104, 105syldan 585 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))
107 djaj.j . . . . 5 𝐽 = ((vA‘𝐾)‘𝑊)
1086, 42, 7, 43, 107djavalN 37114 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐼𝑋) ⊆ ((LTrn‘𝐾)‘𝑊) ∧ (𝐼𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))) → ((𝐼𝑋)𝐽(𝐼𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))))
10998, 102, 106, 108syl12anc 865 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝐼𝑋)𝐽(𝐼𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))))
1105, 33, 20latmle2 17359 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
1112, 19, 14, 110syl3anc 1490 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
1125, 33, 6, 7diaeldm 37015 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
113112adantr 472 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
11422, 111, 113mpbir2and 704 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)
1155, 33, 6, 7diaeldm 37015 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
116115adantr 472 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
11730, 37, 116mpbir2and 704 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)
11820, 6, 7diameetN 37035 . . . . . 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 865 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
12017, 20, 10, 6, 42, 7, 43diaocN 37104 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)))
121120adantrr 708 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)))
12217, 20, 10, 6, 42, 7, 43diaocN 37104 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))
123122adantrl 707 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))
124121, 123ineq12d 3979 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝐼‘((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌))))
125119, 124eqtrd 2799 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌))))
126125fveq2d 6383 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼𝑌)))))
127109, 126eqtr4d 2802 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → ((𝐼𝑋)𝐽(𝐼𝑌)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
12845, 97, 1273eqtr4d 2809 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋 ∈ dom 𝐼𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 𝑌)) = ((𝐼𝑋)𝐽(𝐼𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  cin 3733  wss 3734   class class class wbr 4811  dom cdm 5279  ran crn 5280  cfv 6070  (class class class)co 6846  Basecbs 16146  lecple 16237  occoc 16238  joincjn 17226  meetcmee 17227  Latclat 17327  OPcops 35151  OLcol 35153  OMLcoml 35154  HLchlt 35329  LHypclh 35963  LTrncltrn 36080  DIsoAcdia 37007  ocAcocaN 37098  vAcdjaN 37110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-riotaBAD 34932
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-1st 7370  df-2nd 7371  df-undef 7606  df-map 8066  df-proset 17210  df-poset 17228  df-plt 17240  df-lub 17256  df-glb 17257  df-join 17258  df-meet 17259  df-p0 17321  df-p1 17322  df-lat 17328  df-clat 17390  df-oposet 35155  df-cmtN 35156  df-ol 35157  df-oml 35158  df-covers 35245  df-ats 35246  df-atl 35277  df-cvlat 35301  df-hlat 35330  df-llines 35477  df-lplanes 35478  df-lvols 35479  df-lines 35480  df-psubsp 35482  df-pmap 35483  df-padd 35775  df-lhyp 35967  df-laut 35968  df-ldil 36083  df-ltrn 36084  df-trl 36138  df-disoa 37008  df-docaN 37099  df-djaN 37111
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator