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

Theorem omlfh1N 33361
Description: Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in [Kalmbach] p. 25. (fh1 27662 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
omlfh1.b 𝐵 = (Base‘𝐾)
omlfh1.j = (join‘𝐾)
omlfh1.m = (meet‘𝐾)
omlfh1.c 𝐶 = (cm‘𝐾)
Assertion
Ref Expression
omlfh1N ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (𝑌 𝑍)) = ((𝑋 𝑌) (𝑋 𝑍)))

Proof of Theorem omlfh1N
StepHypRef Expression
1 omllat 33345 . . . . 5 (𝐾 ∈ OML → 𝐾 ∈ Lat)
2 omlfh1.b . . . . . 6 𝐵 = (Base‘𝐾)
3 eqid 2604 . . . . . 6 (le‘𝐾) = (le‘𝐾)
4 omlfh1.j . . . . . 6 = (join‘𝐾)
5 omlfh1.m . . . . . 6 = (meet‘𝐾)
62, 3, 4, 5latledi 16853 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)))
71, 6sylan 486 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)))
873adant3 1073 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)))
91adantr 479 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ Lat)
10 simpr1 1059 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑋𝐵)
11 simpr2 1060 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑌𝐵)
12 simpr3 1061 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑍𝐵)
132, 4latjcl 16815 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑌𝐵𝑍𝐵) → (𝑌 𝑍) ∈ 𝐵)
149, 11, 12, 13syl3anc 1317 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑌 𝑍) ∈ 𝐵)
152, 5latmcom 16839 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑌 𝑍) ∈ 𝐵) → (𝑋 (𝑌 𝑍)) = ((𝑌 𝑍) 𝑋))
169, 10, 14, 15syl3anc 1317 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (𝑌 𝑍)) = ((𝑌 𝑍) 𝑋))
17 omlol 33343 . . . . . . . . 9 (𝐾 ∈ OML → 𝐾 ∈ OL)
1817adantr 479 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OL)
192, 5latmcl 16816 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
209, 10, 11, 19syl3anc 1317 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 𝑌) ∈ 𝐵)
212, 5latmcl 16816 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑍𝐵) → (𝑋 𝑍) ∈ 𝐵)
229, 10, 12, 21syl3anc 1317 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 𝑍) ∈ 𝐵)
23 eqid 2604 . . . . . . . . 9 (oc‘𝐾) = (oc‘𝐾)
242, 4, 5, 23oldmj1 33324 . . . . . . . 8 ((𝐾 ∈ OL ∧ (𝑋 𝑌) ∈ 𝐵 ∧ (𝑋 𝑍) ∈ 𝐵) → ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍))) = (((oc‘𝐾)‘(𝑋 𝑌)) ((oc‘𝐾)‘(𝑋 𝑍))))
2518, 20, 22, 24syl3anc 1317 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍))) = (((oc‘𝐾)‘(𝑋 𝑌)) ((oc‘𝐾)‘(𝑋 𝑍))))
262, 4, 5, 23oldmm1 33320 . . . . . . . . 9 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)))
2718, 10, 11, 26syl3anc 1317 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)))
282, 4, 5, 23oldmm1 33320 . . . . . . . . 9 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑍𝐵) → ((oc‘𝐾)‘(𝑋 𝑍)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))
2918, 10, 12, 28syl3anc 1317 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(𝑋 𝑍)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))
3027, 29oveq12d 6540 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘(𝑋 𝑌)) ((oc‘𝐾)‘(𝑋 𝑍))) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))
3125, 30eqtrd 2638 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍))) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))
3216, 31oveq12d 6540 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
33323adant3 1073 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
34 omlop 33344 . . . . . . . . . . 11 (𝐾 ∈ OML → 𝐾 ∈ OP)
3534adantr 479 . . . . . . . . . 10 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OP)
362, 23opoccl 33297 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
3735, 10, 36syl2anc 690 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
382, 23opoccl 33297 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑌𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
3935, 11, 38syl2anc 690 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
402, 4latjcl 16815 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
419, 37, 39, 40syl3anc 1317 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
422, 23opoccl 33297 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑍𝐵) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
4335, 12, 42syl2anc 690 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
442, 4latjcl 16815 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
459, 37, 43, 44syl3anc 1317 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
462, 5latmcl 16816 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) ∈ 𝐵)
479, 41, 45, 46syl3anc 1317 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) ∈ 𝐵)
482, 5latmassOLD 33332 . . . . . . 7 ((𝐾 ∈ OL ∧ ((𝑌 𝑍) ∈ 𝐵𝑋𝐵 ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) ∈ 𝐵)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
4918, 14, 10, 47, 48syl13anc 1319 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
50493adant3 1073 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
51 omlfh1.c . . . . . . . . . . . . . 14 𝐶 = (cm‘𝐾)
522, 23, 51cmt2N 33353 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋𝐶𝑌𝑋𝐶((oc‘𝐾)‘𝑌)))
53523adant3r3 1267 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑌𝑋𝐶((oc‘𝐾)‘𝑌)))
54 simpl 471 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OML)
552, 4, 5, 23, 51cmtbr3N 33357 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (𝑋𝐶((oc‘𝐾)‘𝑌) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌))))
5654, 10, 39, 55syl3anc 1317 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶((oc‘𝐾)‘𝑌) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌))))
5753, 56bitrd 266 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑌 ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌))))
5857biimpa 499 . . . . . . . . . 10 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ 𝑋𝐶𝑌) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌)))
5958adantrr 748 . . . . . . . . 9 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌)))
60593impa 1250 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌)))
612, 23, 51cmt2N 33353 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑍𝐵) → (𝑋𝐶𝑍𝑋𝐶((oc‘𝐾)‘𝑍)))
62613adant3r2 1266 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑍𝑋𝐶((oc‘𝐾)‘𝑍)))
632, 4, 5, 23, 51cmtbr3N 33357 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (𝑋𝐶((oc‘𝐾)‘𝑍) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍))))
6454, 10, 43, 63syl3anc 1317 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶((oc‘𝐾)‘𝑍) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍))))
6562, 64bitrd 266 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑍 ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍))))
6665biimpa 499 . . . . . . . . . 10 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ 𝑋𝐶𝑍) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍)))
6766adantrl 747 . . . . . . . . 9 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍)))
68673impa 1250 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍)))
6960, 68oveq12d 6540 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
702, 5latmmdiN 33337 . . . . . . . . 9 ((𝐾 ∈ OL ∧ (𝑋𝐵 ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
7118, 10, 41, 45, 70syl13anc 1319 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
72713adant3 1073 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
732, 5latmmdiN 33337 . . . . . . . . 9 ((𝐾 ∈ OL ∧ (𝑋𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵)) → (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
7418, 10, 39, 43, 73syl13anc 1319 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
75743adant3 1073 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
7669, 72, 753eqtr4d 2648 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))))
7776oveq2d 6538 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))) = ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
782, 5latmcl 16816 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
799, 39, 43, 78syl3anc 1317 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
802, 5latm12 33333 . . . . . . 7 ((𝐾 ∈ OL ∧ ((𝑌 𝑍) ∈ 𝐵𝑋𝐵 ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)) → ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
8118, 14, 10, 79, 80syl13anc 1319 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
82813adant3 1073 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
8350, 77, 823eqtrd 2642 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
842, 4, 5, 23oldmj1 33324 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ 𝑌𝐵𝑍𝐵) → ((oc‘𝐾)‘(𝑌 𝑍)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))
8518, 11, 12, 84syl3anc 1317 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(𝑌 𝑍)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))
8685oveq2d 6538 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) ((oc‘𝐾)‘(𝑌 𝑍))) = ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))))
87 eqid 2604 . . . . . . . . . 10 (0.‘𝐾) = (0.‘𝐾)
882, 23, 5, 87opnoncon 33311 . . . . . . . . 9 ((𝐾 ∈ OP ∧ (𝑌 𝑍) ∈ 𝐵) → ((𝑌 𝑍) ((oc‘𝐾)‘(𝑌 𝑍))) = (0.‘𝐾))
8935, 14, 88syl2anc 690 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) ((oc‘𝐾)‘(𝑌 𝑍))) = (0.‘𝐾))
9086, 89eqtr3d 2640 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = (0.‘𝐾))
9190oveq2d 6538 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 (0.‘𝐾)))
922, 5, 87olm01 33339 . . . . . . 7 ((𝐾 ∈ OL ∧ 𝑋𝐵) → (𝑋 (0.‘𝐾)) = (0.‘𝐾))
9318, 10, 92syl2anc 690 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (0.‘𝐾)) = (0.‘𝐾))
9491, 93eqtrd 2638 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (0.‘𝐾))
95943adant3 1073 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (0.‘𝐾))
9633, 83, 953eqtrd 2642 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾))
972, 4latjcl 16815 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑋 𝑌) ∈ 𝐵 ∧ (𝑋 𝑍) ∈ 𝐵) → ((𝑋 𝑌) (𝑋 𝑍)) ∈ 𝐵)
989, 20, 22, 97syl3anc 1317 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) (𝑋 𝑍)) ∈ 𝐵)
992, 5latmcl 16816 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑌 𝑍) ∈ 𝐵) → (𝑋 (𝑌 𝑍)) ∈ 𝐵)
1009, 10, 14, 99syl3anc 1317 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (𝑌 𝑍)) ∈ 𝐵)
1012, 3, 5, 23, 87omllaw3 33348 . . . . 5 ((𝐾 ∈ OML ∧ ((𝑋 𝑌) (𝑋 𝑍)) ∈ 𝐵 ∧ (𝑋 (𝑌 𝑍)) ∈ 𝐵) → ((((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)) ∧ ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍))))
10254, 98, 100, 101syl3anc 1317 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)) ∧ ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍))))
1031023adant3 1073 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)) ∧ ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍))))
1048, 96, 103mp2and 710 . 2 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍)))
105104eqcomd 2610 1 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (𝑌 𝑍)) = ((𝑋 𝑌) (𝑋 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1975   class class class wbr 4572  cfv 5785  (class class class)co 6522  Basecbs 15636  lecple 15716  occoc 15717  joincjn 16708  meetcmee 16709  0.cp0 16801  Latclat 16809  OPcops 33275  cmccmtN 33276  OLcol 33277  OMLcoml 33278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-rep 4688  ax-sep 4698  ax-nul 4707  ax-pow 4759  ax-pr 4823  ax-un 6819
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-ral 2895  df-rex 2896  df-reu 2897  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-op 4126  df-uni 4362  df-iun 4446  df-br 4573  df-opab 4633  df-mpt 4634  df-id 4938  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790  df-fo 5791  df-f1o 5792  df-fv 5793  df-riota 6484  df-ov 6525  df-oprab 6526  df-preset 16692  df-poset 16710  df-lub 16738  df-glb 16739  df-join 16740  df-meet 16741  df-p0 16803  df-lat 16810  df-oposet 33279  df-cmtN 33280  df-ol 33281  df-oml 33282
This theorem is referenced by:  omlfh3N  33362  omlmod1i2N  33363
  Copyright terms: Public domain W3C validator