cmtbr3N - Mathbox for Norm Megill

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

Theorem cmtbr3N 35413

Description: Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (cmbr3 29043 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
cmtbr2.b	⊢ 𝐵 = (Base‘𝐾)
cmtbr2.j	⊢ ∨ = (join‘𝐾)
cmtbr2.m	⊢ ∧ = (meet‘𝐾)
cmtbr2.o	⊢ ⊥ = (oc‘𝐾)
cmtbr2.c	⊢ 𝐶 = (cm‘𝐾)

**Assertion**
Ref	Expression
cmtbr3N	⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))

**Proof of Theorem cmtbr3N**
Step	Hyp	Ref	Expression
1		cmtbr2.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
2		cmtbr2.c	. . . . 5 ⊢ 𝐶 = (cm‘𝐾)
3	1, 2	cmtcomN 35408	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑌𝐶𝑋))
4		cmtbr2.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
5		cmtbr2.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
6		cmtbr2.o	. . . . . 6 ⊢ ⊥ = (oc‘𝐾)
7	1, 4, 5, 6, 2	cmtbr2N 35412	. . . . 5 ⊢ ((𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌𝐶𝑋 ↔ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
8	7	3com23 1117	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌𝐶𝑋 ↔ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
9	3, 8	bitrd 271	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
10		oveq2 6932	. . . . . 6 ⊢ (𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋))) → (𝑋 ∧ 𝑌) = (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
11	10	adantl 475	. . . . 5 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))) → (𝑋 ∧ 𝑌) = (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
12		omlol 35399	. . . . . . . . 9 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL)
13	12	3ad2ant1 1124	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OL)
14		simp2 1128	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
15		omllat 35401	. . . . . . . . . 10 ⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat)
16	15	3ad2ant1 1124	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
17		simp3 1129	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
18	1, 4	latjcl 17441	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌 ∨ 𝑋) ∈ 𝐵)
19	16, 17, 14, 18	syl3anc 1439	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 ∨ 𝑋) ∈ 𝐵)
20		omlop 35400	. . . . . . . . . . 11 ⊢ (𝐾 ∈ OML → 𝐾 ∈ OP)
21	20	3ad2ant1 1124	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OP)
22	1, 6	opoccl 35353	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)
23	21, 14, 22	syl2anc 579	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵)
24	1, 4	latjcl 17441	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ ( ⊥ ‘𝑋) ∈ 𝐵) → (𝑌 ∨ ( ⊥ ‘𝑋)) ∈ 𝐵)
25	16, 17, 23, 24	syl3anc 1439	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 ∨ ( ⊥ ‘𝑋)) ∈ 𝐵)
26	1, 5	latmassOLD 35388	. . . . . . . 8 ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ (𝑌 ∨ 𝑋) ∈ 𝐵 ∧ (𝑌 ∨ ( ⊥ ‘𝑋)) ∈ 𝐵)) → ((𝑋 ∧ (𝑌 ∨ 𝑋)) ∧ (𝑌 ∨ ( ⊥ ‘𝑋))) = (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
27	13, 14, 19, 25, 26	syl13anc 1440	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (𝑌 ∨ 𝑋)) ∧ (𝑌 ∨ ( ⊥ ‘𝑋))) = (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))))
28	1, 4	latjcom 17449	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑌 ∨ 𝑋) = (𝑋 ∨ 𝑌))
29	16, 17, 14, 28	syl3anc 1439	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 ∨ 𝑋) = (𝑋 ∨ 𝑌))
30	29	oveq2d 6940	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑌 ∨ 𝑋)) = (𝑋 ∧ (𝑋 ∨ 𝑌)))
31	1, 4, 5	latabs2 17478	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑋 ∨ 𝑌)) = 𝑋)
32	15, 31	syl3an1 1163	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑋 ∨ 𝑌)) = 𝑋)
33	30, 32	eqtrd 2814	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (𝑌 ∨ 𝑋)) = 𝑋)
34	1, 4	latjcom 17449	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ ( ⊥ ‘𝑋) ∈ 𝐵) → (𝑌 ∨ ( ⊥ ‘𝑋)) = (( ⊥ ‘𝑋) ∨ 𝑌))
35	16, 17, 23, 34	syl3anc 1439	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 ∨ ( ⊥ ‘𝑋)) = (( ⊥ ‘𝑋) ∨ 𝑌))
36	33, 35	oveq12d 6942	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (𝑌 ∨ 𝑋)) ∧ (𝑌 ∨ ( ⊥ ‘𝑋))) = (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)))
37	27, 36	eqtr3d 2816	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))) = (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)))
38	37	adantr 474	. . . . 5 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))) → (𝑋 ∧ ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))) = (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)))
39	11, 38	eqtr2d 2815	. . . 4 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋)))) → (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌))
40	39	ex 403	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌 = ((𝑌 ∨ 𝑋) ∧ (𝑌 ∨ ( ⊥ ‘𝑋))) → (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))
41	9, 40	sylbid 232	. 2 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 → (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))
42		simp1 1127	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ OML)
43	1, 6	opoccl 35353	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵)
44	21, 17, 43	syl2anc 579	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘𝑌) ∈ 𝐵)
45	1, 5	latmcl 17442	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵)
46	16, 14, 44, 45	syl3anc 1439	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵)
47	42, 46, 14	3jca 1119	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐾 ∈ OML ∧ (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵))
48		eqid 2778	. . . . . . . . . 10 ⊢ (le‘𝐾) = (le‘𝐾)
49	1, 48, 5	latmle1 17466	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘𝑌) ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑌))(le‘𝐾)𝑋)
50	16, 14, 44, 49	syl3anc 1439	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑌))(le‘𝐾)𝑋)
51	1, 48, 4, 5, 6	omllaw2N 35403	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((𝑋 ∧ ( ⊥ ‘𝑌))(le‘𝐾)𝑋 → ((𝑋 ∧ ( ⊥ ‘𝑌)) ∨ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋)) = 𝑋))
52	47, 50, 51	sylc 65	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ ( ⊥ ‘𝑌)) ∨ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋)) = 𝑋)
53	1, 6	opoccl 35353	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∈ 𝐵)
54	21, 46, 53	syl2anc 579	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∈ 𝐵)
55	1, 5	latmcl 17442	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∈ 𝐵)
56	16, 54, 14, 55	syl3anc 1439	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∈ 𝐵)
57	1, 4	latjcom 17449	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∧ ( ⊥ ‘𝑌)) ∈ 𝐵 ∧ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∈ 𝐵) → ((𝑋 ∧ ( ⊥ ‘𝑌)) ∨ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋)) = ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
58	16, 46, 56, 57	syl3anc 1439	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ ( ⊥ ‘𝑌)) ∨ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋)) = ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
59	52, 58	eqtr3d 2816	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 = ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
60	59	adantr 474	. . . . 5 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)) → 𝑋 = ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
61	1, 4, 5, 6	oldmm3N 35378	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∨ 𝑌))
62	12, 61	syl3an1 1163	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∨ 𝑌))
63	62	oveq2d 6940	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌)))) = (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)))
64	1, 5	latmcom 17465	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌)))) = (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋))
65	16, 14, 54, 64	syl3anc 1439	. . . . . . . . 9 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌)))) = (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋))
66	63, 65	eqtr3d 2816	. . . . . . . 8 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋))
67	66	eqeq1d 2780	. . . . . . 7 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌) ↔ (( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) = (𝑋 ∧ 𝑌)))
68		oveq1 6931	. . . . . . 7 ⊢ ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) = (𝑋 ∧ 𝑌) → ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
69	67, 68	syl6bi 245	. . . . . 6 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌) → ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌)))))
70	69	imp 397	. . . . 5 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)) → ((( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) ∧ 𝑋) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
71	60, 70	eqtrd 2814	. . . 4 ⊢ (((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)) → 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))
72	71	ex 403	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌) → 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌)))))
73	1, 4, 5, 6, 2	cmtvalN 35370	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌)))))
74	72, 73	sylibrd 251	. 2 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌) → 𝑋𝐶𝑌))
75	41, 74	impbid 204	1 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∧ w3a 1071 = wceq 1601 ∈ wcel 2107 class class class wbr 4888 ‘cfv 6137 (class class class)co 6924 Basecbs 16259 lecple 16349 occoc 16350 joincjn 17334 meetcmee 17335 Latclat 17435 OPcops 35331 cmccmtN 35332 OLcol 35333 OMLcoml 35334

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-rep 5008 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 ax-un 7228

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-reu 3097 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-iun 4757 df-br 4889 df-opab 4951 df-mpt 4968 df-id 5263 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-rn 5368 df-res 5369 df-ima 5370 df-iota 6101 df-fun 6139 df-fn 6140 df-f 6141 df-f1 6142 df-fo 6143 df-f1o 6144 df-fv 6145 df-riota 6885 df-ov 6927 df-oprab 6928 df-proset 17318 df-poset 17336 df-lub 17364 df-glb 17365 df-join 17366 df-meet 17367 df-lat 17436 df-oposet 35335 df-cmtN 35336 df-ol 35337 df-oml 35338

This theorem is referenced by: cmtbr4N 35414 omlfh1N 35417

W3C validator