Proof of Theorem djajN
| Step | Hyp | Ref
| Expression |
| 1 | | hllat 39364 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
| 2 | 1 | ad2antrr 726 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ Lat) |
| 3 | | hlop 39363 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
| 4 | 3 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OP) |
| 5 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 6 | | djaj.h |
. . . . . . . . . 10
⊢ 𝐻 = (LHyp‘𝐾) |
| 7 | | djaj.i |
. . . . . . . . . 10
⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) |
| 8 | 5, 6, 7 | diadmclN 41039 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ (Base‘𝐾)) |
| 9 | 8 | adantrr 717 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑋 ∈ (Base‘𝐾)) |
| 10 | | eqid 2737 |
. . . . . . . . 9
⊢
(oc‘𝐾) =
(oc‘𝐾) |
| 11 | 5, 10 | opoccl 39195 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
| 12 | 4, 9, 11 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾)) |
| 13 | 5, 6 | lhpbase 40000 |
. . . . . . . . 9
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
| 14 | 13 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑊 ∈ (Base‘𝐾)) |
| 15 | 5, 10 | opoccl 39195 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) |
| 16 | 4, 14, 15 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) |
| 17 | | djaj.k |
. . . . . . . 8
⊢ ∨ =
(join‘𝐾) |
| 18 | 5, 17 | latjcl 18484 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧
((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾)) |
| 19 | 2, 12, 16, 18 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾)) |
| 20 | | eqid 2737 |
. . . . . . 7
⊢
(meet‘𝐾) =
(meet‘𝐾) |
| 21 | 5, 20 | latmcl 18485 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧
(((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) |
| 22 | 2, 19, 14, 21 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) |
| 23 | 5, 6, 7 | diadmclN 41039 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌 ∈ (Base‘𝐾)) |
| 24 | 23 | adantrl 716 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑌 ∈ (Base‘𝐾)) |
| 25 | 5, 10 | opoccl 39195 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾)) |
| 26 | 4, 24, 25 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾)) |
| 27 | 5, 17 | latjcl 18484 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧
((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾)) |
| 28 | 2, 26, 16, 27 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾)) |
| 29 | 5, 20 | latmcl 18485 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧
(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) |
| 30 | 2, 28, 14, 29 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) |
| 31 | 5, 20 | latmcl 18485 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧
((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾)) |
| 32 | 2, 22, 30, 31 | syl3anc 1373 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾)) |
| 33 | | eqid 2737 |
. . . . 5
⊢
(le‘𝐾) =
(le‘𝐾) |
| 34 | 5, 33, 20 | latmle2 18510 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧
((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) |
| 35 | 2, 22, 30, 34 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) |
| 36 | 5, 33, 20 | latmle2 18510 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧
(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊) |
| 37 | 2, 28, 14, 36 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊) |
| 38 | 5, 33, 2, 32, 30, 14, 35, 37 | lattrd 18491 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)𝑊) |
| 39 | 5, 33, 6, 7 | diaeldm 41038 |
. . . . 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‘𝐾)𝑊))) |
| 40 | 39 | adantr 480 |
. . . 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‘𝐾)𝑊))) |
| 41 | 32, 38, 40 | mpbir2and 713 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ dom 𝐼) |
| 42 | | eqid 2737 |
. . . 4
⊢
((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊) |
| 43 | | eqid 2737 |
. . . 4
⊢
((ocA‘𝐾)‘𝑊) = ((ocA‘𝐾)‘𝑊) |
| 44 | 17, 20, 10, 6, 42, 7, 43 | diaocN 41127 |
. . 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‘𝐾)𝑊))))) |
| 45 | 41, 44 | syldan 591 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))) |
| 46 | | hloml 39358 |
. . . . . 6
⊢ (𝐾 ∈ HL → 𝐾 ∈ OML) |
| 47 | 46 | ad2antrr 726 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OML) |
| 48 | 5, 17 | latjcl 18484 |
. . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∨ 𝑌) ∈ (Base‘𝐾)) |
| 49 | 2, 9, 24, 48 | syl3anc 1373 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌) ∈ (Base‘𝐾)) |
| 50 | 33, 6, 7 | diadmleN 41040 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋(le‘𝐾)𝑊) |
| 51 | 50 | adantrr 717 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑋(le‘𝐾)𝑊) |
| 52 | 33, 6, 7 | diadmleN 41040 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌(le‘𝐾)𝑊) |
| 53 | 52 | adantrl 716 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑌(le‘𝐾)𝑊) |
| 54 | 5, 33, 17 | latjle12 18495 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑋(le‘𝐾)𝑊 ∧ 𝑌(le‘𝐾)𝑊) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)𝑊)) |
| 55 | 2, 9, 24, 14, 54 | syl13anc 1374 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋(le‘𝐾)𝑊 ∧ 𝑌(le‘𝐾)𝑊) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)𝑊)) |
| 56 | 51, 53, 55 | mpbi2and 712 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌)(le‘𝐾)𝑊) |
| 57 | 5, 33, 17, 20, 10 | omlspjN 39262 |
. . . . 5
⊢ ((𝐾 ∈ OML ∧ ((𝑋 ∨ 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ (𝑋 ∨ 𝑌)(le‘𝐾)𝑊) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 ∨ 𝑌)) |
| 58 | 47, 49, 14, 56, 57 | syl121anc 1377 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 ∨ 𝑌)) |
| 59 | 5, 17 | latjidm 18507 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧
((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)) |
| 60 | 2, 16, 59 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)) |
| 61 | 60 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))) = ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))) |
| 62 | 5, 17 | latjass 18528 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ ((𝑋 ∨ 𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∨ ((oc‘𝐾)‘𝑊)) = ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊)))) |
| 63 | 2, 49, 16, 16, 62 | syl13anc 1374 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∨ ((oc‘𝐾)‘𝑊)) = ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊)))) |
| 64 | | hlol 39362 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) |
| 65 | 64 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OL) |
| 66 | 5, 17, 20, 10 | oldmm2 39219 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ OL ∧ (𝑋 ∨ 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))) |
| 67 | 65, 49, 14, 66 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))) |
| 68 | 5, 17, 20, 10 | oldmj1 39222 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) |
| 69 | 65, 9, 24, 68 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌))) |
| 70 | 5, 33, 20 | latleeqm1 18512 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋)) |
| 71 | 2, 9, 14, 70 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋)) |
| 72 | 51, 71 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋(meet‘𝐾)𝑊) = 𝑋) |
| 73 | 72 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑋)) |
| 74 | 5, 17, 20, 10 | oldmm1 39218 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))) |
| 75 | 65, 9, 14, 74 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))) |
| 76 | 73, 75 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))) |
| 77 | 5, 33, 20 | latleeqm1 18512 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌)) |
| 78 | 2, 24, 14, 77 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌)) |
| 79 | 53, 78 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑌(meet‘𝐾)𝑊) = 𝑌) |
| 80 | 79 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑌)) |
| 81 | 5, 17, 20, 10 | oldmm1 39218 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ OL ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))) |
| 82 | 65, 24, 14, 81 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))) |
| 83 | 80, 82 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))) |
| 84 | 76, 83 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))) |
| 85 | 69, 84 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))) |
| 86 | 85 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊)) |
| 87 | 5, 20 | latmmdir 39236 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ OL ∧
((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) |
| 88 | 65, 19, 28, 14, 87 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) |
| 89 | 86, 88 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) |
| 90 | 89 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) |
| 91 | 67, 90 | eqtr3d 2779 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) |
| 92 | 91 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∨ ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))) |
| 93 | 63, 92 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))) |
| 94 | 61, 93 | eqtr3d 2779 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))) |
| 95 | 94 | oveq1d 7446 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) |
| 96 | 58, 95 | eqtr3d 2779 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) |
| 97 | 96 | fveq2d 6910 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 ∨ 𝑌)) = (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) |
| 98 | | simpl 482 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 99 | 6, 7 | diaclN 41052 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ ran 𝐼) |
| 100 | 99 | adantrr 717 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑋) ∈ ran 𝐼) |
| 101 | 6, 42, 7 | diaelrnN 41047 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ∈ ran 𝐼) → (𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊)) |
| 102 | 100, 101 | syldan 591 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊)) |
| 103 | 6, 7 | diaclN 41052 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘𝑌) ∈ ran 𝐼) |
| 104 | 103 | adantrl 716 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑌) ∈ ran 𝐼) |
| 105 | 6, 42, 7 | diaelrnN 41047 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑌) ∈ ran 𝐼) → (𝐼‘𝑌) ⊆ ((LTrn‘𝐾)‘𝑊)) |
| 106 | 104, 105 | syldan 591 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑌) ⊆ ((LTrn‘𝐾)‘𝑊)) |
| 107 | | djaj.j |
. . . . 5
⊢ 𝐽 = ((vA‘𝐾)‘𝑊) |
| 108 | 6, 42, 7, 43, 107 | djavalN 41137 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊) ∧ (𝐼‘𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))))) |
| 109 | 98, 102, 106, 108 | syl12anc 837 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))))) |
| 110 | 5, 33, 20 | latmle2 18510 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧
(((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊) |
| 111 | 2, 19, 14, 110 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊) |
| 112 | 5, 33, 6, 7 | diaeldm 41038 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊))) |
| 113 | 112 | adantr 480 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊))) |
| 114 | 22, 111, 113 | mpbir2and 713 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼) |
| 115 | 5, 33, 6, 7 | diaeldm 41038 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊))) |
| 116 | 115 | adantr 480 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊))) |
| 117 | 30, 37, 116 | mpbir2and 713 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼) |
| 118 | 20, 6, 7 | diameetN 41058 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) |
| 119 | 98, 114, 117, 118 | syl12anc 837 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) |
| 120 | 17, 20, 10, 6, 42, 7, 43 | diaocN 41127 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋))) |
| 121 | 120 | adantrr 717 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋))) |
| 122 | 17, 20, 10, 6, 42, 7, 43 | diaocN 41127 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))) |
| 123 | 122 | adantrl 716 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))) |
| 124 | 121, 123 | ineq12d 4221 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))) |
| 125 | 119, 124 | eqtrd 2777 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))) |
| 126 | 125 | fveq2d 6910 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))))) |
| 127 | 109, 126 | eqtr4d 2780 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))) |
| 128 | 45, 97, 127 | 3eqtr4d 2787 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌))) |