djajN - Mathbox for Norm Megill

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

Theorem djajN 41125

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**
Step	Hyp	Ref	Expression
1		hllat 39350	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2	1	ad2antrr 726	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ Lat)
3		hlop 39349	. . . . . . . . 9 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
4	3	ad2antrr 726	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OP)
5		eqid 2729	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
6		djaj.h	. . . . . . . . . 10 ⊢ 𝐻 = (LHyp‘𝐾)
7		djaj.i	. . . . . . . . . 10 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
8	5, 6, 7	diadmclN 41025	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ (Base‘𝐾))
9	8	adantrr 717	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑋 ∈ (Base‘𝐾))
10		eqid 2729	. . . . . . . . 9 ⊢ (oc‘𝐾) = (oc‘𝐾)
11	5, 10	opoccl 39181	. . . . . . . 8 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
12	4, 9, 11	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
13	5, 6	lhpbase 39986	. . . . . . . . 9 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
14	13	ad2antlr 727	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑊 ∈ (Base‘𝐾))
15	5, 10	opoccl 39181	. . . . . . . 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 18381	. . . . . . 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 2729	. . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾)
21	5, 20	latmcl 18382	. . . . . 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 41025	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌 ∈ (Base‘𝐾))
24	23	adantrl 716	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑌 ∈ (Base‘𝐾))
25	5, 10	opoccl 39181	. . . . . . . 8 ⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
26	4, 24, 25	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
27	5, 17	latjcl 18381	. . . . . . 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 18382	. . . . . 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 18382	. . . . 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 2729	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
34	5, 33, 20	latmle2 18407	. . . . . 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 18407	. . . . . 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 18388	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)𝑊)
39	5, 33, 6, 7	diaeldm 41024	. . . . 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 2729	. . . 4 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
43		eqid 2729	. . . 4 ⊢ ((ocA‘𝐾)‘𝑊) = ((ocA‘𝐾)‘𝑊)
44	17, 20, 10, 6, 42, 7, 43	diaocN 41113	. . 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 39344	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
47	46	ad2antrr 726	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OML)
48	5, 17	latjcl 18381	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∨ 𝑌) ∈ (Base‘𝐾))
49	2, 9, 24, 48	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌) ∈ (Base‘𝐾))
50	33, 6, 7	diadmleN 41026	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋(le‘𝐾)𝑊)
51	50	adantrr 717	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑋(le‘𝐾)𝑊)
52	33, 6, 7	diadmleN 41026	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌(le‘𝐾)𝑊)
53	52	adantrl 716	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑌(le‘𝐾)𝑊)
54	5, 33, 17	latjle12 18392	. . . . . . 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 39248	. . . . 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 18404	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
60	2, 16, 59	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
61	60	oveq2d 7385	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))) = ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)))
62	5, 17	latjass 18425	. . . . . . . 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 39348	. . . . . . . . . . 11 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
65	64	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OL)
66	5, 17, 20, 10	oldmm2 39205	. . . . . . . . . 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 39208	. . . . . . . . . . . . . 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 18409	. . . . . . . . . . . . . . . . . 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 6844	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑋))
74	5, 17, 20, 10	oldmm1 39204	. . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)))
77	5, 33, 20	latleeqm1 18409	. . . . . . . . . . . . . . . . . 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 6844	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑌))
81	5, 17, 20, 10	oldmm1 39204	. . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))
84	76, 83	oveq12d 7387	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))))
85	69, 84	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))))
86	85	oveq1d 7384	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊))
87	5, 20	latmmdir 39222	. . . . . . . . . . . 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 2764	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
90	89	fveq2d 6844	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
91	67, 90	eqtr3d 2766	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
92	91	oveq1d 7384	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∨ ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊)))
93	63, 92	eqtr3d 2766	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊)))
94	61, 93	eqtr3d 2766	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊)))
95	94	oveq1d 7384	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
96	58, 95	eqtr3d 2766	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
97	96	fveq2d 6844	. 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 41038	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ ran 𝐼)
100	99	adantrr 717	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑋) ∈ ran 𝐼)
101	6, 42, 7	diaelrnN 41033	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ∈ ran 𝐼) → (𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
102	100, 101	syldan 591	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
103	6, 7	diaclN 41038	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘𝑌) ∈ ran 𝐼)
104	103	adantrl 716	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑌) ∈ ran 𝐼)
105	6, 42, 7	diaelrnN 41033	. . . . 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 41123	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊) ∧ (𝐼‘𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))))
109	98, 102, 106, 108	syl12anc 836	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))))
110	5, 33, 20	latmle2 18407	. . . . . . . 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 41024	. . . . . . . 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 41024	. . . . . . . 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 41044	. . . . . 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 836	. . . . 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 41113	. . . . . . 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 41113	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))
123	122	adantrl 716	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))
124	121, 123	ineq12d 4180	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))))
125	119, 124	eqtrd 2764	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))))
126	125	fveq2d 6844	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))))
127	109, 126	eqtr4d 2767	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
128	45, 97, 127	3eqtr4d 2774	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∩ cin 3910 ⊆ wss 3911 class class class wbr 5102 dom cdm 5631 ran crn 5632 ‘cfv 6499 (class class class)co 7369 Basecbs 17156 lecple 17204 occoc 17205 joincjn 18253 meetcmee 18254 Latclat 18373 OPcops 39159 OLcol 39161 OMLcoml 39162 HLchlt 39337 LHypclh 39972 LTrncltrn 40089 DIsoAcdia 41016 ocAcocaN 41107 vAcdjaN 41119

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-riotaBAD 38940

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-1st 7947 df-2nd 7948 df-undef 8229 df-map 8778 df-proset 18236 df-poset 18255 df-plt 18270 df-lub 18286 df-glb 18287 df-join 18288 df-meet 18289 df-p0 18365 df-p1 18366 df-lat 18374 df-clat 18441 df-oposet 39163 df-cmtN 39164 df-ol 39165 df-oml 39166 df-covers 39253 df-ats 39254 df-atl 39285 df-cvlat 39309 df-hlat 39338 df-llines 39486 df-lplanes 39487 df-lvols 39488 df-lines 39489 df-psubsp 39491 df-pmap 39492 df-padd 39784 df-lhyp 39976 df-laut 39977 df-ldil 40092 df-ltrn 40093 df-trl 40147 df-disoa 41017 df-docaN 41108 df-djaN 41120

This theorem is referenced by: (None)

W3C validator