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 41939

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 40165	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2	1	ad2antrr 738	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ Lat)
3		hlop 40164	. . . . . . . . 9 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
4	3	ad2antrr 738	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OP)
5		eqid 2763	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
6		djaj.h	. . . . . . . . . 10 ⊢ 𝐻 = (LHyp‘𝐾)
7		djaj.i	. . . . . . . . . 10 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
8	5, 6, 7	diadmclN 41839	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ (Base‘𝐾))
9	8	adantrr 729	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑋 ∈ (Base‘𝐾))
10		eqid 2763	. . . . . . . . 9 ⊢ (oc‘𝐾) = (oc‘𝐾)
11	5, 10	opoccl 39996	. . . . . . . 8 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
12	4, 9, 11	syl2anc 595	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
13	5, 6	lhpbase 40800	. . . . . . . . 9 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
14	13	ad2antlr 739	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑊 ∈ (Base‘𝐾))
15	5, 10	opoccl 39996	. . . . . . . 8 ⊢ ((𝐾 ∈ OP ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))
16	4, 14, 15	syl2anc 595	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))
17		djaj.k	. . . . . . . 8 ⊢ ∨ = (join‘𝐾)
18	5, 17	latjcl 18499	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
19	2, 12, 16, 18	syl3anc 1398	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
20		eqid 2763	. . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾)
21	5, 20	latmcl 18500	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
22	2, 19, 14, 21	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
23	5, 6, 7	diadmclN 41839	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌 ∈ (Base‘𝐾))
24	23	adantrl 728	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑌 ∈ (Base‘𝐾))
25	5, 10	opoccl 39996	. . . . . . . 8 ⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
26	4, 24, 25	syl2anc 595	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
27	5, 17	latjcl 18499	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
28	2, 26, 16, 27	syl3anc 1398	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
29	5, 20	latmcl 18500	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
30	2, 28, 14, 29	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
31	5, 20	latmcl 18500	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))
32	2, 22, 30, 31	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))
33		eqid 2763	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
34	5, 33, 20	latmle2 18525	. . . . . 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 1398	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
36	5, 33, 20	latmle2 18525	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
37	2, 28, 14, 36	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
38	5, 33, 2, 32, 30, 14, 35, 37	lattrd 18506	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)𝑊)
39	5, 33, 6, 7	diaeldm 41838	. . . . 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 485	. . . 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 725	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ dom 𝐼)
42		eqid 2763	. . . 4 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
43		eqid 2763	. . . 4 ⊢ ((ocA‘𝐾)‘𝑊) = ((ocA‘𝐾)‘𝑊)
44	17, 20, 10, 6, 42, 7, 43	diaocN 41927	. . 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 602	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
46		hloml 40159	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
47	46	ad2antrr 738	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OML)
48	5, 17	latjcl 18499	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∨ 𝑌) ∈ (Base‘𝐾))
49	2, 9, 24, 48	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌) ∈ (Base‘𝐾))
50	33, 6, 7	diadmleN 41840	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋(le‘𝐾)𝑊)
51	50	adantrr 729	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑋(le‘𝐾)𝑊)
52	33, 6, 7	diadmleN 41840	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌(le‘𝐾)𝑊)
53	52	adantrl 728	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑌(le‘𝐾)𝑊)
54	5, 33, 17	latjle12 18510	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑋(le‘𝐾)𝑊 ∧ 𝑌(le‘𝐾)𝑊) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)𝑊))
55	2, 9, 24, 14, 54	syl13anc 1399	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋(le‘𝐾)𝑊 ∧ 𝑌(le‘𝐾)𝑊) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)𝑊))
56	51, 53, 55	mpbi2and 724	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌)(le‘𝐾)𝑊)
57	5, 33, 17, 20, 10	omlspjN 40063	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ ((𝑋 ∨ 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ (𝑋 ∨ 𝑌)(le‘𝐾)𝑊) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 ∨ 𝑌))
58	47, 49, 14, 56, 57	syl121anc 1402	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 ∨ 𝑌))
59	5, 17	latjidm 18522	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
60	2, 16, 59	syl2anc 595	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
61	60	oveq2d 7426	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))) = ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)))
62	5, 17	latjass 18543	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ ((𝑋 ∨ 𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∨ ((oc‘𝐾)‘𝑊)) = ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))))
63	2, 49, 16, 16, 62	syl13anc 1399	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∨ ((oc‘𝐾)‘𝑊)) = ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))))
64		hlol 40163	. . . . . . . . . . 11 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
65	64	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OL)
66	5, 17, 20, 10	oldmm2 40020	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∨ 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)))
67	65, 49, 14, 66	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)))
68	5, 17, 20, 10	oldmj1 40023	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))
69	65, 9, 24, 68	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))
70	5, 33, 20	latleeqm1 18527	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋))
71	2, 9, 14, 70	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋))
72	51, 71	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋(meet‘𝐾)𝑊) = 𝑋)
73	72	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑋))
74	5, 17, 20, 10	oldmm1 40019	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)))
75	65, 9, 14, 74	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)))
76	73, 75	eqtr3d 2800	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)))
77	5, 33, 20	latleeqm1 18527	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌))
78	2, 24, 14, 77	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌))
79	53, 78	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑌(meet‘𝐾)𝑊) = 𝑌)
80	79	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑌))
81	5, 17, 20, 10	oldmm1 40019	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ OL ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))
82	65, 24, 14, 81	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))
83	80, 82	eqtr3d 2800	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))
84	76, 83	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))))
85	69, 84	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))))
86	85	oveq1d 7425	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊))
87	5, 20	latmmdir 40037	. . . . . . . . . . . 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 1399	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
89	86, 88	eqtrd 2798	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
90	89	fveq2d 6885	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
91	67, 90	eqtr3d 2800	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
92	91	oveq1d 7425	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∨ ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊)))
93	63, 92	eqtr3d 2800	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊)))
94	61, 93	eqtr3d 2800	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊)))
95	94	oveq1d 7425	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
96	58, 95	eqtr3d 2800	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
97	96	fveq2d 6885	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 ∨ 𝑌)) = (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
98		simpl 487	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
99	6, 7	diaclN 41852	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ ran 𝐼)
100	99	adantrr 729	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑋) ∈ ran 𝐼)
101	6, 42, 7	diaelrnN 41847	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ∈ ran 𝐼) → (𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
102	100, 101	syldan 602	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
103	6, 7	diaclN 41852	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘𝑌) ∈ ran 𝐼)
104	103	adantrl 728	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑌) ∈ ran 𝐼)
105	6, 42, 7	diaelrnN 41847	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑌) ∈ ran 𝐼) → (𝐼‘𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))
106	104, 105	syldan 602	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))
107		djaj.j	. . . . 5 ⊢ 𝐽 = ((vA‘𝐾)‘𝑊)
108	6, 42, 7, 43, 107	djavalN 41937	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊) ∧ (𝐼‘𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))))
109	98, 102, 106, 108	syl12anc 849	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))))
110	5, 33, 20	latmle2 18525	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
111	2, 19, 14, 110	syl3anc 1398	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
112	5, 33, 6, 7	diaeldm 41838	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
113	112	adantr 485	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
114	22, 111, 113	mpbir2and 725	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)
115	5, 33, 6, 7	diaeldm 41838	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
116	115	adantr 485	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
117	30, 37, 116	mpbir2and 725	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)
118	20, 6, 7	diameetN 41858	. . . . . 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 849	. . . . 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 41927	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)))
121	120	adantrr 729	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)))
122	17, 20, 10, 6, 42, 7, 43	diaocN 41927	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))
123	122	adantrl 728	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))
124	121, 123	ineq12d 4174	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))))
125	119, 124	eqtrd 2798	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))))
126	125	fveq2d 6885	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))))
127	109, 126	eqtr4d 2801	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
128	45, 97, 127	3eqtr4d 2808	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ∩ cin 3904 ⊆ wss 3905 class class class wbr 5109 dom cdm 5661 ran crn 5662 ‘cfv 6536 (class class class)co 7410 Basecbs 17273 lecple 17321 occoc 17322 joincjn 18371 meetcmee 18372 Latclat 18491 OPcops 39974 OLcol 39976 OMLcoml 39977 HLchlt 40152 LHypclh 40786 LTrncltrn 40903 DIsoAcdia 41830 ocAcocaN 41921 vAcdjaN 41933

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-riotaBAD 39755

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5110 df-opab 5174 df-mpt 5193 df-id 5556 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-1st 7982 df-2nd 7983 df-undef 8265 df-map 8822 df-proset 18354 df-poset 18373 df-plt 18388 df-lub 18404 df-glb 18405 df-join 18406 df-meet 18407 df-p0 18483 df-p1 18484 df-lat 18492 df-clat 18559 df-oposet 39978 df-cmtN 39979 df-ol 39980 df-oml 39981 df-covers 40068 df-ats 40069 df-atl 40100 df-cvlat 40124 df-hlat 40153 df-llines 40300 df-lplanes 40301 df-lvols 40302 df-lines 40303 df-psubsp 40305 df-pmap 40306 df-padd 40598 df-lhyp 40790 df-laut 40791 df-ldil 40906 df-ltrn 40907 df-trl 40961 df-disoa 41831 df-docaN 41922 df-djaN 41934

This theorem is used by: (None)

W3C validator