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 37825

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 36051	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2	1	ad2antrr 722	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ Lat)
3		hlop 36050	. . . . . . . . 9 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
4	3	ad2antrr 722	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OP)
5		eqid 2797	. . . . . . . . . 10 ⊢ (Base‘𝐾) = (Base‘𝐾)
6		djaj.h	. . . . . . . . . 10 ⊢ 𝐻 = (LHyp‘𝐾)
7		djaj.i	. . . . . . . . . 10 ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊)
8	5, 6, 7	diadmclN 37725	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋 ∈ (Base‘𝐾))
9	8	adantrr 713	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑋 ∈ (Base‘𝐾))
10		eqid 2797	. . . . . . . . 9 ⊢ (oc‘𝐾) = (oc‘𝐾)
11	5, 10	opoccl 35882	. . . . . . . 8 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
12	4, 9, 11	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾))
13	5, 6	lhpbase 36686	. . . . . . . . 9 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
14	13	ad2antlr 723	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑊 ∈ (Base‘𝐾))
15	5, 10	opoccl 35882	. . . . . . . 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 17494	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
19	2, 12, 16, 18	syl3anc 1364	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
20		eqid 2797	. . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾)
21	5, 20	latmcl 17495	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
22	2, 19, 14, 21	syl3anc 1364	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
23	5, 6, 7	diadmclN 37725	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌 ∈ (Base‘𝐾))
24	23	adantrl 712	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑌 ∈ (Base‘𝐾))
25	5, 10	opoccl 35882	. . . . . . . 8 ⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
26	4, 24, 25	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾))
27	5, 17	latjcl 17494	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
28	2, 26, 16, 27	syl3anc 1364	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾))
29	5, 20	latmcl 17495	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
30	2, 28, 14, 29	syl3anc 1364	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾))
31	5, 20	latmcl 17495	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))
32	2, 22, 30, 31	syl3anc 1364	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))
33		eqid 2797	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
34	5, 33, 20	latmle2 17520	. . . . . 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 1364	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
36	5, 33, 20	latmle2 17520	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
37	2, 28, 14, 36	syl3anc 1364	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
38	5, 33, 2, 32, 30, 14, 35, 37	lattrd 17501	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))(le‘𝐾)𝑊)
39	5, 33, 6, 7	diaeldm 37724	. . . . 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 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‘𝐾)𝑊)))
41	32, 38, 40	mpbir2and 709	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∈ dom 𝐼)
42		eqid 2797	. . . 4 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
43		eqid 2797	. . . 4 ⊢ ((ocA‘𝐾)‘𝑊) = ((ocA‘𝐾)‘𝑊)
44	17, 20, 10, 6, 42, 7, 43	diaocN 37813	. . 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 36045	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OML)
47	46	ad2antrr 722	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OML)
48	5, 17	latjcl 17494	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → (𝑋 ∨ 𝑌) ∈ (Base‘𝐾))
49	2, 9, 24, 48	syl3anc 1364	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌) ∈ (Base‘𝐾))
50	33, 6, 7	diadmleN 37726	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → 𝑋(le‘𝐾)𝑊)
51	50	adantrr 713	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑋(le‘𝐾)𝑊)
52	33, 6, 7	diadmleN 37726	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → 𝑌(le‘𝐾)𝑊)
53	52	adantrl 712	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝑌(le‘𝐾)𝑊)
54	5, 33, 17	latjle12 17505	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑋(le‘𝐾)𝑊 ∧ 𝑌(le‘𝐾)𝑊) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)𝑊))
55	2, 9, 24, 14, 54	syl13anc 1365	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋(le‘𝐾)𝑊 ∧ 𝑌(le‘𝐾)𝑊) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)𝑊))
56	51, 53, 55	mpbi2and 708	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌)(le‘𝐾)𝑊)
57	5, 33, 17, 20, 10	omlspjN 35949	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ ((𝑋 ∨ 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ (𝑋 ∨ 𝑌)(le‘𝐾)𝑊) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 ∨ 𝑌))
58	47, 49, 14, 56, 57	syl121anc 1368	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = (𝑋 ∨ 𝑌))
59	5, 17	latjidm 17517	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
60	2, 16, 59	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
61	60	oveq2d 7039	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))) = ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)))
62	5, 17	latjass 17538	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ ((𝑋 ∨ 𝑌) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾) ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∨ ((oc‘𝐾)‘𝑊)) = ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))))
63	2, 49, 16, 16, 62	syl13anc 1365	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∨ ((oc‘𝐾)‘𝑊)) = ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))))
64		hlol 36049	. . . . . . . . . . 11 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
65	64	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → 𝐾 ∈ OL)
66	5, 17, 20, 10	oldmm2 35906	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∨ 𝑌) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)))
67	65, 49, 14, 66	syl3anc 1364	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊)) = ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)))
68	5, 17, 20, 10	oldmj1 35909	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑌 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))
69	65, 9, 24, 68	syl3anc 1364	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)))
70	5, 33, 20	latleeqm1 17522	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋))
71	2, 9, 14, 70	syl3anc 1364	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋(le‘𝐾)𝑊 ↔ (𝑋(meet‘𝐾)𝑊) = 𝑋))
72	51, 71	mpbid 233	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋(meet‘𝐾)𝑊) = 𝑋)
73	72	fveq2d 6549	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑋))
74	5, 17, 20, 10	oldmm1 35905	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)))
75	65, 9, 14, 74	syl3anc 1364	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)))
76	73, 75	eqtr3d 2835	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑋) = (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)))
77	5, 33, 20	latleeqm1 17522	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌))
78	2, 24, 14, 77	syl3anc 1364	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑌(le‘𝐾)𝑊 ↔ (𝑌(meet‘𝐾)𝑊) = 𝑌))
79	53, 78	mpbid 233	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑌(meet‘𝐾)𝑊) = 𝑌)
80	79	fveq2d 6549	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘𝑌))
81	5, 17, 20, 10	oldmm1 35905	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ OL ∧ 𝑌 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))
82	65, 24, 14, 81	syl3anc 1364	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑌(meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))
83	80, 82	eqtr3d 2835	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘𝑌) = (((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))
84	76, 83	oveq12d 7041	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)((oc‘𝐾)‘𝑌)) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))))
85	69, 84	eqtrd 2833	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(𝑋 ∨ 𝑌)) = ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))))
86	85	oveq1d 7038	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊))
87	5, 20	latmmdir 35923	. . . . . . . . . . . 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 1365	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)(((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
89	86, 88	eqtrd 2833	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊) = (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
90	89	fveq2d 6549	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((oc‘𝐾)‘(((oc‘𝐾)‘(𝑋 ∨ 𝑌))(meet‘𝐾)𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
91	67, 90	eqtr3d 2835	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))))
92	91	oveq1d 7038	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) ∨ ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊)))
93	63, 92	eqtr3d 2835	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ (((oc‘𝐾)‘𝑊) ∨ ((oc‘𝐾)‘𝑊))) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊)))
94	61, 93	eqtr3d 2835	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊)) = (((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊)))
95	94	oveq1d 7038	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((𝑋 ∨ 𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
96	58, 95	eqtr3d 2835	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝑋 ∨ 𝑌) = ((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))
97	96	fveq2d 6549	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 ∨ 𝑌)) = (𝐼‘((((oc‘𝐾)‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))
98		simpl 483	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
99	6, 7	diaclN 37738	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ ran 𝐼)
100	99	adantrr 713	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑋) ∈ ran 𝐼)
101	6, 42, 7	diaelrnN 37733	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘𝑋) ∈ ran 𝐼) → (𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
102	100, 101	syldan 591	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊))
103	6, 7	diaclN 37738	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘𝑌) ∈ ran 𝐼)
104	103	adantrl 712	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘𝑌) ∈ ran 𝐼)
105	6, 42, 7	diaelrnN 37733	. . . . 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 37823	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐼‘𝑋) ⊆ ((LTrn‘𝐾)‘𝑊) ∧ (𝐼‘𝑌) ⊆ ((LTrn‘𝐾)‘𝑊))) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))))
109	98, 102, 106, 108	syl12anc 833	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))))
110	5, 33, 20	latmle2 17520	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
111	2, 19, 14, 110	syl3anc 1364	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)
112	5, 33, 6, 7	diaeldm 37724	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
113	112	adantr 481	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
114	22, 111, 113	mpbir2and 709	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)
115	5, 33, 6, 7	diaeldm 37724	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
116	115	adantr 481	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼 ↔ (((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(le‘𝐾)𝑊)))
117	30, 37, 116	mpbir2and 709	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊) ∈ dom 𝐼)
118	20, 6, 7	diameetN 37744	. . . . . 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 833	. . . . 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 37813	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)))
121	120	adantrr 713	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)))
122	17, 20, 10, 6, 42, 7, 43	diaocN 37813	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ dom 𝐼) → (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))
123	122	adantrl 712	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))
124	121, 123	ineq12d 4116	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)) ∩ (𝐼‘((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))))
125	119, 124	eqtrd 2833	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊))) = ((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌))))
126	125	fveq2d 6549	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))) = (((ocA‘𝐾)‘𝑊)‘((((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑋)) ∩ (((ocA‘𝐾)‘𝑊)‘(𝐼‘𝑌)))))
127	109, 126	eqtr4d 2836	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → ((𝐼‘𝑋)𝐽(𝐼‘𝑌)) = (((ocA‘𝐾)‘𝑊)‘(𝐼‘(((((oc‘𝐾)‘𝑋) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)(meet‘𝐾)((((oc‘𝐾)‘𝑌) ∨ ((oc‘𝐾)‘𝑊))(meet‘𝐾)𝑊)))))
128	45, 97, 127	3eqtr4d 2843	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1525 ∈ wcel 2083 ∩ cin 3864 ⊆ wss 3865 class class class wbr 4968 dom cdm 5450 ran crn 5451 ‘cfv 6232 (class class class)co 7023 Basecbs 16316 lecple 16405 occoc 16406 joincjn 17387 meetcmee 17388 Latclat 17488 OPcops 35860 OLcol 35862 OMLcoml 35863 HLchlt 36038 LHypclh 36672 LTrncltrn 36789 DIsoAcdia 37716 ocAcocaN 37807 vAcdjaN 37819

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-rep 5088 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-riotaBAD 35641

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-reu 3114 df-rmo 3115 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-int 4789 df-iun 4833 df-iin 4834 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-riota 6984 df-ov 7026 df-oprab 7027 df-mpo 7028 df-1st 7552 df-2nd 7553 df-undef 7797 df-map 8265 df-proset 17371 df-poset 17389 df-plt 17401 df-lub 17417 df-glb 17418 df-join 17419 df-meet 17420 df-p0 17482 df-p1 17483 df-lat 17489 df-clat 17551 df-oposet 35864 df-cmtN 35865 df-ol 35866 df-oml 35867 df-covers 35954 df-ats 35955 df-atl 35986 df-cvlat 36010 df-hlat 36039 df-llines 36186 df-lplanes 36187 df-lvols 36188 df-lines 36189 df-psubsp 36191 df-pmap 36192 df-padd 36484 df-lhyp 36676 df-laut 36677 df-ldil 36792 df-ltrn 36793 df-trl 36847 df-disoa 37717 df-docaN 37808 df-djaN 37820

This theorem is referenced by: (None)

W3C validator