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 39996
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 38221 . . . . . 6 (𝐾 ∈ HL β†’ 𝐾 ∈ Lat)
21ad2antrr 724 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ 𝐾 ∈ Lat)
3 hlop 38220 . . . . . . . . 9 (𝐾 ∈ HL β†’ 𝐾 ∈ OP)
43ad2antrr 724 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ 𝐾 ∈ OP)
5 eqid 2732 . . . . . . . . . 10 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
6 djaj.h . . . . . . . . . 10 𝐻 = (LHypβ€˜πΎ)
7 djaj.i . . . . . . . . . 10 𝐼 = ((DIsoAβ€˜πΎ)β€˜π‘Š)
85, 6, 7diadmclN 39896 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) β†’ 𝑋 ∈ (Baseβ€˜πΎ))
98adantrr 715 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ 𝑋 ∈ (Baseβ€˜πΎ))
10 eqid 2732 . . . . . . . . 9 (ocβ€˜πΎ) = (ocβ€˜πΎ)
115, 10opoccl 38052 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑋 ∈ (Baseβ€˜πΎ)) β†’ ((ocβ€˜πΎ)β€˜π‘‹) ∈ (Baseβ€˜πΎ))
124, 9, 11syl2anc 584 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜π‘‹) ∈ (Baseβ€˜πΎ))
135, 6lhpbase 38857 . . . . . . . . 9 (π‘Š ∈ 𝐻 β†’ π‘Š ∈ (Baseβ€˜πΎ))
1413ad2antlr 725 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ π‘Š ∈ (Baseβ€˜πΎ))
155, 10opoccl 38052 . . . . . . . 8 ((𝐾 ∈ OP ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((ocβ€˜πΎ)β€˜π‘Š) ∈ (Baseβ€˜πΎ))
164, 14, 15syl2anc 584 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜π‘Š) ∈ (Baseβ€˜πΎ))
17 djaj.k . . . . . . . 8 ∨ = (joinβ€˜πΎ)
185, 17latjcl 18388 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((ocβ€˜πΎ)β€˜π‘‹) ∈ (Baseβ€˜πΎ) ∧ ((ocβ€˜πΎ)β€˜π‘Š) ∈ (Baseβ€˜πΎ)) β†’ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∈ (Baseβ€˜πΎ))
192, 12, 16, 18syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∈ (Baseβ€˜πΎ))
20 eqid 2732 . . . . . . 7 (meetβ€˜πΎ) = (meetβ€˜πΎ)
215, 20latmcl 18389 . . . . . 6 ((𝐾 ∈ Lat ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ (Baseβ€˜πΎ))
222, 19, 14, 21syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ (Baseβ€˜πΎ))
235, 6, 7diadmclN 39896 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ π‘Œ ∈ dom 𝐼) β†’ π‘Œ ∈ (Baseβ€˜πΎ))
2423adantrl 714 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ π‘Œ ∈ (Baseβ€˜πΎ))
255, 10opoccl 38052 . . . . . . . 8 ((𝐾 ∈ OP ∧ π‘Œ ∈ (Baseβ€˜πΎ)) β†’ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ (Baseβ€˜πΎ))
264, 24, 25syl2anc 584 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ (Baseβ€˜πΎ))
275, 17latjcl 18388 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ (Baseβ€˜πΎ) ∧ ((ocβ€˜πΎ)β€˜π‘Š) ∈ (Baseβ€˜πΎ)) β†’ (((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∈ (Baseβ€˜πΎ))
282, 26, 16, 27syl3anc 1371 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∈ (Baseβ€˜πΎ))
295, 20latmcl 18389 . . . . . 6 ((𝐾 ∈ Lat ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ (Baseβ€˜πΎ))
302, 28, 14, 29syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ (Baseβ€˜πΎ))
315, 20latmcl 18389 . . . . 5 ((𝐾 ∈ Lat ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ (Baseβ€˜πΎ) ∧ ((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ (Baseβ€˜πΎ)) β†’ (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)) ∈ (Baseβ€˜πΎ))
322, 22, 30, 31syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)) ∈ (Baseβ€˜πΎ))
33 eqid 2732 . . . . 5 (leβ€˜πΎ) = (leβ€˜πΎ)
345, 33, 20latmle2 18414 . . . . . 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 1371 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))(leβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))
365, 33, 20latmle2 18414 . . . . . 6 ((𝐾 ∈ Lat ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(leβ€˜πΎ)π‘Š)
372, 28, 14, 36syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(leβ€˜πΎ)π‘Š)
385, 33, 2, 32, 30, 14, 35, 37lattrd 18395 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))(leβ€˜πΎ)π‘Š)
395, 33, 6, 7diaeldm 39895 . . . . 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 481 . . . 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 711 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)) ∈ dom 𝐼)
42 eqid 2732 . . . 4 ((LTrnβ€˜πΎ)β€˜π‘Š) = ((LTrnβ€˜πΎ)β€˜π‘Š)
43 eqid 2732 . . . 4 ((ocAβ€˜πΎ)β€˜π‘Š) = ((ocAβ€˜πΎ)β€˜π‘Š)
4417, 20, 10, 6, 42, 7, 43diaocN 39984 . . 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 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 38215 . . . . . 6 (𝐾 ∈ HL β†’ 𝐾 ∈ OML)
4746ad2antrr 724 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ 𝐾 ∈ OML)
485, 17latjcl 18388 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Baseβ€˜πΎ) ∧ π‘Œ ∈ (Baseβ€˜πΎ)) β†’ (𝑋 ∨ π‘Œ) ∈ (Baseβ€˜πΎ))
492, 9, 24, 48syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (𝑋 ∨ π‘Œ) ∈ (Baseβ€˜πΎ))
5033, 6, 7diadmleN 39897 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) β†’ 𝑋(leβ€˜πΎ)π‘Š)
5150adantrr 715 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ 𝑋(leβ€˜πΎ)π‘Š)
5233, 6, 7diadmleN 39897 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ π‘Œ ∈ dom 𝐼) β†’ π‘Œ(leβ€˜πΎ)π‘Š)
5352adantrl 714 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ π‘Œ(leβ€˜πΎ)π‘Š)
545, 33, 17latjle12 18399 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑋 ∈ (Baseβ€˜πΎ) ∧ π‘Œ ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ))) β†’ ((𝑋(leβ€˜πΎ)π‘Š ∧ π‘Œ(leβ€˜πΎ)π‘Š) ↔ (𝑋 ∨ π‘Œ)(leβ€˜πΎ)π‘Š))
552, 9, 24, 14, 54syl13anc 1372 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((𝑋(leβ€˜πΎ)π‘Š ∧ π‘Œ(leβ€˜πΎ)π‘Š) ↔ (𝑋 ∨ π‘Œ)(leβ€˜πΎ)π‘Š))
5651, 53, 55mpbi2and 710 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (𝑋 ∨ π‘Œ)(leβ€˜πΎ)π‘Š)
575, 33, 17, 20, 10omlspjN 38119 . . . . 5 ((𝐾 ∈ OML ∧ ((𝑋 ∨ π‘Œ) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) ∧ (𝑋 ∨ π‘Œ)(leβ€˜πΎ)π‘Š) β†’ (((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) = (𝑋 ∨ π‘Œ))
5847, 49, 14, 56, 57syl121anc 1375 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) = (𝑋 ∨ π‘Œ))
595, 17latjidm 18411 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((ocβ€˜πΎ)β€˜π‘Š) ∈ (Baseβ€˜πΎ)) β†’ (((ocβ€˜πΎ)β€˜π‘Š) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) = ((ocβ€˜πΎ)β€˜π‘Š))
602, 16, 59syl2anc 584 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((ocβ€˜πΎ)β€˜π‘Š) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) = ((ocβ€˜πΎ)β€˜π‘Š))
6160oveq2d 7421 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((𝑋 ∨ π‘Œ) ∨ (((ocβ€˜πΎ)β€˜π‘Š) ∨ ((ocβ€˜πΎ)β€˜π‘Š))) = ((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
625, 17latjass 18432 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((𝑋 ∨ π‘Œ) ∈ (Baseβ€˜πΎ) ∧ ((ocβ€˜πΎ)β€˜π‘Š) ∈ (Baseβ€˜πΎ) ∧ ((ocβ€˜πΎ)β€˜π‘Š) ∈ (Baseβ€˜πΎ))) β†’ (((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) = ((𝑋 ∨ π‘Œ) ∨ (((ocβ€˜πΎ)β€˜π‘Š) ∨ ((ocβ€˜πΎ)β€˜π‘Š))))
632, 49, 16, 16, 62syl13anc 1372 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) = ((𝑋 ∨ π‘Œ) ∨ (((ocβ€˜πΎ)β€˜π‘Š) ∨ ((ocβ€˜πΎ)β€˜π‘Š))))
64 hlol 38219 . . . . . . . . . . 11 (𝐾 ∈ HL β†’ 𝐾 ∈ OL)
6564ad2antrr 724 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ 𝐾 ∈ OL)
665, 17, 20, 10oldmm2 38076 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ (𝑋 ∨ π‘Œ) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((ocβ€˜πΎ)β€˜(((ocβ€˜πΎ)β€˜(𝑋 ∨ π‘Œ))(meetβ€˜πΎ)π‘Š)) = ((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
6765, 49, 14, 66syl3anc 1371 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜(((ocβ€˜πΎ)β€˜(𝑋 ∨ π‘Œ))(meetβ€˜πΎ)π‘Š)) = ((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
685, 17, 20, 10oldmj1 38079 . . . . . . . . . . . . . 14 ((𝐾 ∈ OL ∧ 𝑋 ∈ (Baseβ€˜πΎ) ∧ π‘Œ ∈ (Baseβ€˜πΎ)) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∨ π‘Œ)) = (((ocβ€˜πΎ)β€˜π‘‹)(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜π‘Œ)))
6965, 9, 24, 68syl3anc 1371 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∨ π‘Œ)) = (((ocβ€˜πΎ)β€˜π‘‹)(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜π‘Œ)))
705, 33, 20latleeqm1 18416 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ (𝑋(leβ€˜πΎ)π‘Š ↔ (𝑋(meetβ€˜πΎ)π‘Š) = 𝑋))
712, 9, 14, 70syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (𝑋(leβ€˜πΎ)π‘Š ↔ (𝑋(meetβ€˜πΎ)π‘Š) = 𝑋))
7251, 71mpbid 231 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (𝑋(meetβ€˜πΎ)π‘Š) = 𝑋)
7372fveq2d 6892 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜(𝑋(meetβ€˜πΎ)π‘Š)) = ((ocβ€˜πΎ)β€˜π‘‹))
745, 17, 20, 10oldmm1 38075 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OL ∧ 𝑋 ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((ocβ€˜πΎ)β€˜(𝑋(meetβ€˜πΎ)π‘Š)) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
7565, 9, 14, 74syl3anc 1371 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜(𝑋(meetβ€˜πΎ)π‘Š)) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
7673, 75eqtr3d 2774 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜π‘‹) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
775, 33, 20latleeqm1 18416 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ π‘Œ ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ (π‘Œ(leβ€˜πΎ)π‘Š ↔ (π‘Œ(meetβ€˜πΎ)π‘Š) = π‘Œ))
782, 24, 14, 77syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (π‘Œ(leβ€˜πΎ)π‘Š ↔ (π‘Œ(meetβ€˜πΎ)π‘Š) = π‘Œ))
7953, 78mpbid 231 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (π‘Œ(meetβ€˜πΎ)π‘Š) = π‘Œ)
8079fveq2d 6892 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜(π‘Œ(meetβ€˜πΎ)π‘Š)) = ((ocβ€˜πΎ)β€˜π‘Œ))
815, 17, 20, 10oldmm1 38075 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OL ∧ π‘Œ ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((ocβ€˜πΎ)β€˜(π‘Œ(meetβ€˜πΎ)π‘Š)) = (((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
8265, 24, 14, 81syl3anc 1371 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜(π‘Œ(meetβ€˜πΎ)π‘Š)) = (((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
8380, 82eqtr3d 2774 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜π‘Œ) = (((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
8476, 83oveq12d 7423 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((ocβ€˜πΎ)β€˜π‘‹)(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜π‘Œ)) = ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)(((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))))
8569, 84eqtrd 2772 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∨ π‘Œ)) = ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)(((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))))
8685oveq1d 7420 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((ocβ€˜πΎ)β€˜(𝑋 ∨ π‘Œ))(meetβ€˜πΎ)π‘Š) = (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)(((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))(meetβ€˜πΎ)π‘Š))
875, 20latmmdir 38093 . . . . . . . . . . . 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 1372 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)(((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))(meetβ€˜πΎ)π‘Š) = (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)))
8986, 88eqtrd 2772 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((ocβ€˜πΎ)β€˜(𝑋 ∨ π‘Œ))(meetβ€˜πΎ)π‘Š) = (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)))
9089fveq2d 6892 . . . . . . . . 9 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((ocβ€˜πΎ)β€˜(((ocβ€˜πΎ)β€˜(𝑋 ∨ π‘Œ))(meetβ€˜πΎ)π‘Š)) = ((ocβ€˜πΎ)β€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))))
9167, 90eqtr3d 2774 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) = ((ocβ€˜πΎ)β€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))))
9291oveq1d 7420 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) = (((ocβ€˜πΎ)β€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
9363, 92eqtr3d 2774 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((𝑋 ∨ π‘Œ) ∨ (((ocβ€˜πΎ)β€˜π‘Š) ∨ ((ocβ€˜πΎ)β€˜π‘Š))) = (((ocβ€˜πΎ)β€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
9461, 93eqtr3d 2774 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) = (((ocβ€˜πΎ)β€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))) ∨ ((ocβ€˜πΎ)β€˜π‘Š)))
9594oveq1d 7420 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((𝑋 ∨ π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) = ((((ocβ€˜πΎ)β€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))
9658, 95eqtr3d 2774 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (𝑋 ∨ π‘Œ) = ((((ocβ€˜πΎ)β€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))
9796fveq2d 6892 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (πΌβ€˜(𝑋 ∨ π‘Œ)) = (πΌβ€˜((((ocβ€˜πΎ)β€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)))
98 simpl 483 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
996, 7diaclN 39909 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) β†’ (πΌβ€˜π‘‹) ∈ ran 𝐼)
10099adantrr 715 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (πΌβ€˜π‘‹) ∈ ran 𝐼)
1016, 42, 7diaelrnN 39904 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (πΌβ€˜π‘‹) ∈ ran 𝐼) β†’ (πΌβ€˜π‘‹) βŠ† ((LTrnβ€˜πΎ)β€˜π‘Š))
102100, 101syldan 591 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (πΌβ€˜π‘‹) βŠ† ((LTrnβ€˜πΎ)β€˜π‘Š))
1036, 7diaclN 39909 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ π‘Œ ∈ dom 𝐼) β†’ (πΌβ€˜π‘Œ) ∈ ran 𝐼)
104103adantrl 714 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (πΌβ€˜π‘Œ) ∈ ran 𝐼)
1056, 42, 7diaelrnN 39904 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (πΌβ€˜π‘Œ) ∈ ran 𝐼) β†’ (πΌβ€˜π‘Œ) βŠ† ((LTrnβ€˜πΎ)β€˜π‘Š))
106104, 105syldan 591 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (πΌβ€˜π‘Œ) βŠ† ((LTrnβ€˜πΎ)β€˜π‘Š))
107 djaj.j . . . . 5 𝐽 = ((vAβ€˜πΎ)β€˜π‘Š)
1086, 42, 7, 43, 107djavalN 39994 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ ((πΌβ€˜π‘‹) βŠ† ((LTrnβ€˜πΎ)β€˜π‘Š) ∧ (πΌβ€˜π‘Œ) βŠ† ((LTrnβ€˜πΎ)β€˜π‘Š))) β†’ ((πΌβ€˜π‘‹)𝐽(πΌβ€˜π‘Œ)) = (((ocAβ€˜πΎ)β€˜π‘Š)β€˜((((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘‹)) ∩ (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘Œ)))))
10998, 102, 106, 108syl12anc 835 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((πΌβ€˜π‘‹)𝐽(πΌβ€˜π‘Œ)) = (((ocAβ€˜πΎ)β€˜π‘Š)β€˜((((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘‹)) ∩ (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘Œ)))))
1105, 33, 20latmle2 18414 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š)) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) β†’ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(leβ€˜πΎ)π‘Š)
1112, 19, 14, 110syl3anc 1371 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(leβ€˜πΎ)π‘Š)
1125, 33, 6, 7diaeldm 39895 . . . . . . . 8 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ dom 𝐼 ↔ (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ (Baseβ€˜πΎ) ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(leβ€˜πΎ)π‘Š)))
113112adantr 481 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ dom 𝐼 ↔ (((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ (Baseβ€˜πΎ) ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(leβ€˜πΎ)π‘Š)))
11422, 111, 113mpbir2and 711 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ dom 𝐼)
1155, 33, 6, 7diaeldm 39895 . . . . . . . 8 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) β†’ (((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ dom 𝐼 ↔ (((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ (Baseβ€˜πΎ) ∧ ((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(leβ€˜πΎ)π‘Š)))
116115adantr 481 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ dom 𝐼 ↔ (((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ (Baseβ€˜πΎ) ∧ ((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(leβ€˜πΎ)π‘Š)))
11730, 37, 116mpbir2and 711 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š) ∈ dom 𝐼)
11820, 6, 7diameetN 39915 . . . . . 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 39984 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) β†’ (πΌβ€˜((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)) = (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘‹)))
121120adantrr 715 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (πΌβ€˜((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)) = (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘‹)))
12217, 20, 10, 6, 42, 7, 43diaocN 39984 . . . . . . 7 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ π‘Œ ∈ dom 𝐼) β†’ (πΌβ€˜((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)) = (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘Œ)))
123122adantrl 714 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (πΌβ€˜((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)) = (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘Œ)))
124121, 123ineq12d 4212 . . . . 5 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((πΌβ€˜((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)) ∩ (πΌβ€˜((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))) = ((((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘‹)) ∩ (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘Œ))))
125119, 124eqtrd 2772 . . . 4 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (πΌβ€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š))) = ((((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘‹)) ∩ (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘Œ))))
126125fveq2d 6892 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)))) = (((ocAβ€˜πΎ)β€˜π‘Š)β€˜((((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘‹)) ∩ (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜π‘Œ)))))
127109, 126eqtr4d 2775 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ ((πΌβ€˜π‘‹)𝐽(πΌβ€˜π‘Œ)) = (((ocAβ€˜πΎ)β€˜π‘Š)β€˜(πΌβ€˜(((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)(meetβ€˜πΎ)((((ocβ€˜πΎ)β€˜π‘Œ) ∨ ((ocβ€˜πΎ)β€˜π‘Š))(meetβ€˜πΎ)π‘Š)))))
12845, 97, 1273eqtr4d 2782 1 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ π‘Œ ∈ dom 𝐼)) β†’ (πΌβ€˜(𝑋 ∨ π‘Œ)) = ((πΌβ€˜π‘‹)𝐽(πΌβ€˜π‘Œ)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ∩ cin 3946   βŠ† wss 3947   class class class wbr 5147  dom cdm 5675  ran crn 5676  β€˜cfv 6540  (class class class)co 7405  Basecbs 17140  lecple 17200  occoc 17201  joincjn 18260  meetcmee 18261  Latclat 18380  OPcops 38030  OLcol 38032  OMLcoml 38033  HLchlt 38208  LHypclh 38843  LTrncltrn 38960  DIsoAcdia 39887  ocAcocaN 39978  vAcdjaN 39990
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-riotaBAD 37811
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-undef 8254  df-map 8818  df-proset 18244  df-poset 18262  df-plt 18279  df-lub 18295  df-glb 18296  df-join 18297  df-meet 18298  df-p0 18374  df-p1 18375  df-lat 18381  df-clat 18448  df-oposet 38034  df-cmtN 38035  df-ol 38036  df-oml 38037  df-covers 38124  df-ats 38125  df-atl 38156  df-cvlat 38180  df-hlat 38209  df-llines 38357  df-lplanes 38358  df-lvols 38359  df-lines 38360  df-psubsp 38362  df-pmap 38363  df-padd 38655  df-lhyp 38847  df-laut 38848  df-ldil 38963  df-ltrn 38964  df-trl 39018  df-disoa 39888  df-docaN 39979  df-djaN 39991
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator