Theorem cmtcomlemN 37270

Description: Lemma for cmtcomN 37271. (cmcmlem 29961 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
cmtcom.b	⊢ 𝐵 = (Base‘𝐾)
cmtcom.c	⊢ 𝐶 = (cm‘𝐾)

Assertion

Ref	Expression
cmtcomlemN	⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 → 𝑌𝐶𝑋))

Proof of Theorem cmtcomlemN

Step	Hyp	Ref	Expression
1		omllat 37264	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat)
2	1	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
3		omlop 37263	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OP)
4		cmtcom.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐾)
5		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (oc‘𝐾) = (oc‘𝐾)
6	4, 5	opoccl 37216	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
7	3, 6	sylan 580	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
8	7	3adant3 1131	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
9		simp3 1137	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
10		eqid 2738	. . . . . . . . . . . 12 ⊢ (le‘𝐾) = (le‘𝐾)
11		eqid 2738	. . . . . . . . . . . 12 ⊢ (join‘𝐾) = (join‘𝐾)
12	4, 10, 11	latlej2 18177	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌(le‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))
13	2, 8, 9, 12	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌(le‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))
14	4, 11	latjcl 18167	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵)
15	2, 8, 9, 14	syl3anc 1370	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵)
16		eqid 2738	. . . . . . . . . . . 12 ⊢ (meet‘𝐾) = (meet‘𝐾)
17	4, 10, 16	latleeqm2 18196	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵) → (𝑌(le‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ↔ ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌) = 𝑌))
18	2, 9, 15, 17	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌(le‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ↔ ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌) = 𝑌))
19	13, 18	mpbid 231	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌) = 𝑌)
20	19	oveq2d 7283	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌)) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)𝑌))
21		omlol 37262	. . . . . . . . . 10 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
22	21	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OL)
23	3	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP)
24	4, 5	opoccl 37216	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
25	23, 9, 24	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
26	4, 11	latjcl 18167	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵)
27	2, 8, 25, 26	syl3anc 1370	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵)
28	4, 16	latmassOLD 37251	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))(meet‘𝐾)𝑌) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌)))
29	22, 27, 15, 9, 28	syl13anc 1371	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))(meet‘𝐾)𝑌) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)(meet‘𝐾)𝑌)))
30	4, 11, 16, 5	oldmm1 37239	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌)) = (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))
31	21, 30	syl3an1 1162	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌)) = (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))
32	31	oveq1d 7282	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)𝑌))
33	20, 29, 32	3eqtr4rd 2789	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌) = (((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))(meet‘𝐾)𝑌))
34	33	adantr 481	. . . . . 6 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → (((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌) = (((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))(meet‘𝐾)𝑌))
35	4, 11, 16, 5	oldmj4 37246	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))) = (𝑋(meet‘𝐾)𝑌))
36	21, 35	syl3an1 1162	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))) = (𝑋(meet‘𝐾)𝑌))
37	4, 11, 16, 5	oldmj2 37244	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) = (𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))
38	21, 37	syl3an1 1162	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) = (𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))
39	36, 38	oveq12d 7285	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))) = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌))))
40	39	eqeq2d 2749	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = (((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))) ↔ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))))
41	40	biimpar 478	. . . . . . . . 9 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → 𝑋 = (((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))))
42	41	fveq2d 6770	. . . . . . . 8 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((oc‘𝐾)‘𝑋) = ((oc‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))))
43	4, 11, 16, 5	oldmj4 37246	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OL ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌) ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))
44	22, 27, 15, 43	syl3anc 1370	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))
45	44	adantr 481	. . . . . . . 8 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((oc‘𝐾)‘(((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌)))(join‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))) = ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)))
46	42, 45	eqtr2d 2779	. . . . . . 7 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌)) = ((oc‘𝐾)‘𝑋))
47	46	oveq1d 7282	. . . . . 6 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → (((((oc‘𝐾)‘𝑋)(join‘𝐾)((oc‘𝐾)‘𝑌))(meet‘𝐾)(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑌))(meet‘𝐾)𝑌) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌))
48	34, 47	eqtrd 2778	. . . . 5 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → (((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌) = (((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌))
49	48	oveq2d 7283	. . . 4 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌)) = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌)))
50		simp1 1135	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OML)
51	4, 16	latmcl 18168	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑌) ∈ 𝐵)
52	1, 51	syl3an1 1162	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑌) ∈ 𝐵)
53	50, 52, 9	3jca 1127	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐾 ∈ OML ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵))
54	4, 10, 16	latmle2 18193	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑌)(le‘𝐾)𝑌)
55	1, 54	syl3an1 1162	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑌)(le‘𝐾)𝑌)
56	4, 10, 11, 16, 5	omllaw2N 37266	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(meet‘𝐾)𝑌)(le‘𝐾)𝑌 → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌)) = 𝑌))
57	53, 55, 56	sylc 65	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌)) = 𝑌)
58	57	adantr 481	. . . 4 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘(𝑋(meet‘𝐾)𝑌))(meet‘𝐾)𝑌)) = 𝑌)
59	4, 16	latmcom 18191	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑌) = (𝑌(meet‘𝐾)𝑋))
60	1, 59	syl3an1 1162	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(meet‘𝐾)𝑌) = (𝑌(meet‘𝐾)𝑋))
61	4, 16	latmcom 18191	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌) = (𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋)))
62	2, 8, 9, 61	syl3anc 1370	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌) = (𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋)))
63	60, 62	oveq12d 7285	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌)) = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋))))
64	63	adantr 481	. . . 4 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(((oc‘𝐾)‘𝑋)(meet‘𝐾)𝑌)) = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋))))
65	49, 58, 64	3eqtr3d 2786	. . 3 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))) → 𝑌 = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋))))
66	65	ex 413	. 2 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌))) → 𝑌 = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋)))))
67		cmtcom.c	. . 3 ⊢ 𝐶 = (cm‘𝐾)
68	4, 11, 16, 5, 67	cmtvalN 37233	. 2 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋(meet‘𝐾)𝑌)(join‘𝐾)(𝑋(meet‘𝐾)((oc‘𝐾)‘𝑌)))))
69	4, 11, 16, 5, 67	cmtvalN 37233	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌𝐶𝑋 ↔ 𝑌 = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋)))))
70	69	3com23 1125	. 2 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌𝐶𝑋 ↔ 𝑌 = ((𝑌(meet‘𝐾)𝑋)(join‘𝐾)(𝑌(meet‘𝐾)((oc‘𝐾)‘𝑋)))))
71	66, 68, 70	3imtr4d 294	1 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 → 𝑌𝐶𝑋))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   class class class wbr 5073  ‘cfv 6426  (class class class)co 7267  Basecbs 16922  lecple 16979  occoc 16980  joincjn 18039  meetcmee 18040  Latclat 18159  OPcops 37194  cmccmtN 37195  OLcol 37196  OMLcoml 37197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5208  ax-sep 5221  ax-nul 5228  ax-pow 5286  ax-pr 5350  ax-un 7578

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3431  df-sbc 3716  df-csb 3832  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5074  df-opab 5136  df-mpt 5157  df-id 5484  df-xp 5590  df-rel 5591  df-cnv 5592  df-co 5593  df-dm 5594  df-rn 5595  df-res 5596  df-ima 5597  df-iota 6384  df-fun 6428  df-fn 6429  df-f 6430  df-f1 6431  df-fo 6432  df-f1o 6433  df-fv 6434  df-riota 7224  df-ov 7270  df-oprab 7271  df-proset 18023  df-poset 18041  df-lub 18074  df-glb 18075  df-join 18076  df-meet 18077  df-lat 18160  df-oposet 37198  df-cmtN 37199  df-ol 37200  df-oml 37201

This theorem is referenced by:  cmtcomN  37271