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 36915
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 29553 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 36899 . . . . 5 (𝐾 ∈ OML → 𝐾 ∈ Lat)
2 omlfh1.b . . . . . 6 𝐵 = (Base‘𝐾)
3 eqid 2738 . . . . . 6 (le‘𝐾) = (le‘𝐾)
4 omlfh1.j . . . . . 6 = (join‘𝐾)
5 omlfh1.m . . . . . 6 = (meet‘𝐾)
62, 3, 4, 5latledi 17815 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)))
71, 6sylan 583 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)))
873adant3 1133 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)))
91adantr 484 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ Lat)
10 simpr1 1195 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑋𝐵)
11 simpr2 1196 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑌𝐵)
12 simpr3 1197 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑍𝐵)
132, 4latjcl 17777 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑌𝐵𝑍𝐵) → (𝑌 𝑍) ∈ 𝐵)
149, 11, 12, 13syl3anc 1372 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑌 𝑍) ∈ 𝐵)
152, 5latmcom 17801 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑌 𝑍) ∈ 𝐵) → (𝑋 (𝑌 𝑍)) = ((𝑌 𝑍) 𝑋))
169, 10, 14, 15syl3anc 1372 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (𝑌 𝑍)) = ((𝑌 𝑍) 𝑋))
17 omlol 36897 . . . . . . . . 9 (𝐾 ∈ OML → 𝐾 ∈ OL)
1817adantr 484 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OL)
192, 5latmcl 17778 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
209, 10, 11, 19syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 𝑌) ∈ 𝐵)
212, 5latmcl 17778 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑍𝐵) → (𝑋 𝑍) ∈ 𝐵)
229, 10, 12, 21syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 𝑍) ∈ 𝐵)
23 eqid 2738 . . . . . . . . 9 (oc‘𝐾) = (oc‘𝐾)
242, 4, 5, 23oldmj1 36878 . . . . . . . 8 ((𝐾 ∈ OL ∧ (𝑋 𝑌) ∈ 𝐵 ∧ (𝑋 𝑍) ∈ 𝐵) → ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍))) = (((oc‘𝐾)‘(𝑋 𝑌)) ((oc‘𝐾)‘(𝑋 𝑍))))
2518, 20, 22, 24syl3anc 1372 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍))) = (((oc‘𝐾)‘(𝑋 𝑌)) ((oc‘𝐾)‘(𝑋 𝑍))))
262, 4, 5, 23oldmm1 36874 . . . . . . . . 9 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)))
2718, 10, 11, 26syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)))
282, 4, 5, 23oldmm1 36874 . . . . . . . . 9 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑍𝐵) → ((oc‘𝐾)‘(𝑋 𝑍)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))
2918, 10, 12, 28syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(𝑋 𝑍)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))
3027, 29oveq12d 7188 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘(𝑋 𝑌)) ((oc‘𝐾)‘(𝑋 𝑍))) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))
3125, 30eqtrd 2773 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍))) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))
3216, 31oveq12d 7188 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
33323adant3 1133 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
34 omlop 36898 . . . . . . . . . . 11 (𝐾 ∈ OML → 𝐾 ∈ OP)
3534adantr 484 . . . . . . . . . 10 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OP)
362, 23opoccl 36851 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
3735, 10, 36syl2anc 587 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
382, 23opoccl 36851 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑌𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
3935, 11, 38syl2anc 587 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
402, 4latjcl 17777 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
419, 37, 39, 40syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
422, 23opoccl 36851 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑍𝐵) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
4335, 12, 42syl2anc 587 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
442, 4latjcl 17777 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
459, 37, 43, 44syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
462, 5latmcl 17778 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) ∈ 𝐵)
479, 41, 45, 46syl3anc 1372 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) ∈ 𝐵)
482, 5latmassOLD 36886 . . . . . . 7 ((𝐾 ∈ OL ∧ ((𝑌 𝑍) ∈ 𝐵𝑋𝐵 ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) ∈ 𝐵)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
4918, 14, 10, 47, 48syl13anc 1373 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
50493adant3 1133 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
51 omlfh1.c . . . . . . . . . . . . . 14 𝐶 = (cm‘𝐾)
522, 23, 51cmt2N 36907 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋𝐶𝑌𝑋𝐶((oc‘𝐾)‘𝑌)))
53523adant3r3 1185 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑌𝑋𝐶((oc‘𝐾)‘𝑌)))
54 simpl 486 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OML)
552, 4, 5, 23, 51cmtbr3N 36911 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (𝑋𝐶((oc‘𝐾)‘𝑌) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌))))
5654, 10, 39, 55syl3anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶((oc‘𝐾)‘𝑌) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌))))
5753, 56bitrd 282 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑌 ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌))))
5857biimpa 480 . . . . . . . . . 10 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ 𝑋𝐶𝑌) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌)))
5958adantrr 717 . . . . . . . . 9 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌)))
60593impa 1111 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌)))
612, 23, 51cmt2N 36907 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑍𝐵) → (𝑋𝐶𝑍𝑋𝐶((oc‘𝐾)‘𝑍)))
62613adant3r2 1184 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑍𝑋𝐶((oc‘𝐾)‘𝑍)))
632, 4, 5, 23, 51cmtbr3N 36911 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (𝑋𝐶((oc‘𝐾)‘𝑍) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍))))
6454, 10, 43, 63syl3anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶((oc‘𝐾)‘𝑍) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍))))
6562, 64bitrd 282 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑍 ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍))))
6665biimpa 480 . . . . . . . . . 10 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ 𝑋𝐶𝑍) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍)))
6766adantrl 716 . . . . . . . . 9 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍)))
68673impa 1111 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍)))
6960, 68oveq12d 7188 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
702, 5latmmdiN 36891 . . . . . . . . 9 ((𝐾 ∈ OL ∧ (𝑋𝐵 ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
7118, 10, 41, 45, 70syl13anc 1373 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
72713adant3 1133 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
732, 5latmmdiN 36891 . . . . . . . . 9 ((𝐾 ∈ OL ∧ (𝑋𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵)) → (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
7418, 10, 39, 43, 73syl13anc 1373 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
75743adant3 1133 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
7669, 72, 753eqtr4d 2783 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))))
7776oveq2d 7186 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))) = ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
782, 5latmcl 17778 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
799, 39, 43, 78syl3anc 1372 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
802, 5latm12 36887 . . . . . . 7 ((𝐾 ∈ OL ∧ ((𝑌 𝑍) ∈ 𝐵𝑋𝐵 ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)) → ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
8118, 14, 10, 79, 80syl13anc 1373 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
82813adant3 1133 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
8350, 77, 823eqtrd 2777 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
842, 4, 5, 23oldmj1 36878 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ 𝑌𝐵𝑍𝐵) → ((oc‘𝐾)‘(𝑌 𝑍)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))
8518, 11, 12, 84syl3anc 1372 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(𝑌 𝑍)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))
8685oveq2d 7186 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) ((oc‘𝐾)‘(𝑌 𝑍))) = ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))))
87 eqid 2738 . . . . . . . . . 10 (0.‘𝐾) = (0.‘𝐾)
882, 23, 5, 87opnoncon 36865 . . . . . . . . 9 ((𝐾 ∈ OP ∧ (𝑌 𝑍) ∈ 𝐵) → ((𝑌 𝑍) ((oc‘𝐾)‘(𝑌 𝑍))) = (0.‘𝐾))
8935, 14, 88syl2anc 587 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) ((oc‘𝐾)‘(𝑌 𝑍))) = (0.‘𝐾))
9086, 89eqtr3d 2775 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = (0.‘𝐾))
9190oveq2d 7186 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 (0.‘𝐾)))
922, 5, 87olm01 36893 . . . . . . 7 ((𝐾 ∈ OL ∧ 𝑋𝐵) → (𝑋 (0.‘𝐾)) = (0.‘𝐾))
9318, 10, 92syl2anc 587 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (0.‘𝐾)) = (0.‘𝐾))
9491, 93eqtrd 2773 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (0.‘𝐾))
95943adant3 1133 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (0.‘𝐾))
9633, 83, 953eqtrd 2777 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾))
972, 4latjcl 17777 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑋 𝑌) ∈ 𝐵 ∧ (𝑋 𝑍) ∈ 𝐵) → ((𝑋 𝑌) (𝑋 𝑍)) ∈ 𝐵)
989, 20, 22, 97syl3anc 1372 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) (𝑋 𝑍)) ∈ 𝐵)
992, 5latmcl 17778 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑌 𝑍) ∈ 𝐵) → (𝑋 (𝑌 𝑍)) ∈ 𝐵)
1009, 10, 14, 99syl3anc 1372 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (𝑌 𝑍)) ∈ 𝐵)
1012, 3, 5, 23, 87omllaw3 36902 . . . . 5 ((𝐾 ∈ OML ∧ ((𝑋 𝑌) (𝑋 𝑍)) ∈ 𝐵 ∧ (𝑋 (𝑌 𝑍)) ∈ 𝐵) → ((((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)) ∧ ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍))))
10254, 98, 100, 101syl3anc 1372 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)) ∧ ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍))))
1031023adant3 1133 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)) ∧ ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍))))
1048, 96, 103mp2and 699 . 2 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍)))
105104eqcomd 2744 1 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (𝑌 𝑍)) = ((𝑋 𝑌) (𝑋 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wcel 2114   class class class wbr 5030  cfv 6339  (class class class)co 7170  Basecbs 16586  lecple 16675  occoc 16676  joincjn 17670  meetcmee 17671  0.cp0 17763  Latclat 17771  OPcops 36829  cmccmtN 36830  OLcol 36831  OMLcoml 36832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-proset 17654  df-poset 17672  df-lub 17700  df-glb 17701  df-join 17702  df-meet 17703  df-p0 17765  df-lat 17772  df-oposet 36833  df-cmtN 36834  df-ol 36835  df-oml 36836
This theorem is referenced by:  omlfh3N  36916  omlmod1i2N  36917
  Copyright terms: Public domain W3C validator