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 34364
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 28447 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 34348 . . . . 5 (𝐾 ∈ OML → 𝐾 ∈ Lat)
2 omlfh1.b . . . . . 6 𝐵 = (Base‘𝐾)
3 eqid 2620 . . . . . 6 (le‘𝐾) = (le‘𝐾)
4 omlfh1.j . . . . . 6 = (join‘𝐾)
5 omlfh1.m . . . . . 6 = (meet‘𝐾)
62, 3, 4, 5latledi 17070 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)))
71, 6sylan 488 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)))
873adant3 1079 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)))
91adantr 481 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ Lat)
10 simpr1 1065 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑋𝐵)
11 simpr2 1066 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑌𝐵)
12 simpr3 1067 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑍𝐵)
132, 4latjcl 17032 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑌𝐵𝑍𝐵) → (𝑌 𝑍) ∈ 𝐵)
149, 11, 12, 13syl3anc 1324 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑌 𝑍) ∈ 𝐵)
152, 5latmcom 17056 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑌 𝑍) ∈ 𝐵) → (𝑋 (𝑌 𝑍)) = ((𝑌 𝑍) 𝑋))
169, 10, 14, 15syl3anc 1324 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (𝑌 𝑍)) = ((𝑌 𝑍) 𝑋))
17 omlol 34346 . . . . . . . . 9 (𝐾 ∈ OML → 𝐾 ∈ OL)
1817adantr 481 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OL)
192, 5latmcl 17033 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
209, 10, 11, 19syl3anc 1324 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 𝑌) ∈ 𝐵)
212, 5latmcl 17033 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑍𝐵) → (𝑋 𝑍) ∈ 𝐵)
229, 10, 12, 21syl3anc 1324 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 𝑍) ∈ 𝐵)
23 eqid 2620 . . . . . . . . 9 (oc‘𝐾) = (oc‘𝐾)
242, 4, 5, 23oldmj1 34327 . . . . . . . 8 ((𝐾 ∈ OL ∧ (𝑋 𝑌) ∈ 𝐵 ∧ (𝑋 𝑍) ∈ 𝐵) → ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍))) = (((oc‘𝐾)‘(𝑋 𝑌)) ((oc‘𝐾)‘(𝑋 𝑍))))
2518, 20, 22, 24syl3anc 1324 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍))) = (((oc‘𝐾)‘(𝑋 𝑌)) ((oc‘𝐾)‘(𝑋 𝑍))))
262, 4, 5, 23oldmm1 34323 . . . . . . . . 9 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑌𝐵) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)))
2718, 10, 11, 26syl3anc 1324 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(𝑋 𝑌)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)))
282, 4, 5, 23oldmm1 34323 . . . . . . . . 9 ((𝐾 ∈ OL ∧ 𝑋𝐵𝑍𝐵) → ((oc‘𝐾)‘(𝑋 𝑍)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))
2918, 10, 12, 28syl3anc 1324 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(𝑋 𝑍)) = (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))
3027, 29oveq12d 6653 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘(𝑋 𝑌)) ((oc‘𝐾)‘(𝑋 𝑍))) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))
3125, 30eqtrd 2654 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍))) = ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))
3216, 31oveq12d 6653 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
33323adant3 1079 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
34 omlop 34347 . . . . . . . . . . 11 (𝐾 ∈ OML → 𝐾 ∈ OP)
3534adantr 481 . . . . . . . . . 10 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OP)
362, 23opoccl 34300 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑋𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
3735, 10, 36syl2anc 692 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑋) ∈ 𝐵)
382, 23opoccl 34300 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑌𝐵) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
3935, 11, 38syl2anc 692 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑌) ∈ 𝐵)
402, 4latjcl 17032 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
419, 37, 39, 40syl3anc 1324 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵)
422, 23opoccl 34300 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑍𝐵) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
4335, 12, 42syl2anc 692 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘𝑍) ∈ 𝐵)
442, 4latjcl 17032 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
459, 37, 43, 44syl3anc 1324 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
462, 5latmcl 17033 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) ∈ 𝐵)
479, 41, 45, 46syl3anc 1324 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) ∈ 𝐵)
482, 5latmassOLD 34335 . . . . . . 7 ((𝐾 ∈ OL ∧ ((𝑌 𝑍) ∈ 𝐵𝑋𝐵 ∧ ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) ∈ 𝐵)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
4918, 14, 10, 47, 48syl13anc 1326 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
50493adant3 1079 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))))
51 omlfh1.c . . . . . . . . . . . . . 14 𝐶 = (cm‘𝐾)
522, 23, 51cmt2N 34356 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋𝐶𝑌𝑋𝐶((oc‘𝐾)‘𝑌)))
53523adant3r3 1274 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑌𝑋𝐶((oc‘𝐾)‘𝑌)))
54 simpl 473 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ OML)
552, 4, 5, 23, 51cmtbr3N 34360 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵) → (𝑋𝐶((oc‘𝐾)‘𝑌) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌))))
5654, 10, 39, 55syl3anc 1324 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶((oc‘𝐾)‘𝑌) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌))))
5753, 56bitrd 268 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑌 ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌))))
5857biimpa 501 . . . . . . . . . 10 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ 𝑋𝐶𝑌) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌)))
5958adantrr 752 . . . . . . . . 9 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌)))
60593impa 1257 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) = (𝑋 ((oc‘𝐾)‘𝑌)))
612, 23, 51cmt2N 34356 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑍𝐵) → (𝑋𝐶𝑍𝑋𝐶((oc‘𝐾)‘𝑍)))
62613adant3r2 1273 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑍𝑋𝐶((oc‘𝐾)‘𝑍)))
632, 4, 5, 23, 51cmtbr3N 34360 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (𝑋𝐶((oc‘𝐾)‘𝑍) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍))))
6454, 10, 43, 63syl3anc 1324 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶((oc‘𝐾)‘𝑍) ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍))))
6562, 64bitrd 268 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋𝐶𝑍 ↔ (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍))))
6665biimpa 501 . . . . . . . . . 10 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ 𝑋𝐶𝑍) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍)))
6766adantrl 751 . . . . . . . . 9 (((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍)))
68673impa 1257 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))) = (𝑋 ((oc‘𝐾)‘𝑍)))
6960, 68oveq12d 6653 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
702, 5latmmdiN 34340 . . . . . . . . 9 ((𝐾 ∈ OL ∧ (𝑋𝐵 ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
7118, 10, 41, 45, 70syl13anc 1326 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
72713adant3 1079 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = ((𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌))) (𝑋 (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))))
732, 5latmmdiN 34340 . . . . . . . . 9 ((𝐾 ∈ OL ∧ (𝑋𝐵 ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵)) → (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
7418, 10, 39, 43, 73syl13anc 1326 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
75743adant3 1079 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = ((𝑋 ((oc‘𝐾)‘𝑌)) (𝑋 ((oc‘𝐾)‘𝑍))))
7669, 72, 753eqtr4d 2664 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))))
7776oveq2d 6651 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑌 𝑍) (𝑋 ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍))))) = ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
782, 5latmcl 17033 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑌) ∈ 𝐵 ∧ ((oc‘𝐾)‘𝑍) ∈ 𝐵) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
799, 39, 43, 78syl3anc 1324 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)
802, 5latm12 34336 . . . . . . 7 ((𝐾 ∈ OL ∧ ((𝑌 𝑍) ∈ 𝐵𝑋𝐵 ∧ (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)) ∈ 𝐵)) → ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
8118, 14, 10, 79, 80syl13anc 1326 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
82813adant3 1079 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑌 𝑍) (𝑋 (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
8350, 77, 823eqtrd 2658 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (((𝑌 𝑍) 𝑋) ((((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑌)) (((oc‘𝐾)‘𝑋) ((oc‘𝐾)‘𝑍)))) = (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))))
842, 4, 5, 23oldmj1 34327 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ 𝑌𝐵𝑍𝐵) → ((oc‘𝐾)‘(𝑌 𝑍)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))
8518, 11, 12, 84syl3anc 1324 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((oc‘𝐾)‘(𝑌 𝑍)) = (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))
8685oveq2d 6651 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) ((oc‘𝐾)‘(𝑌 𝑍))) = ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))))
87 eqid 2620 . . . . . . . . . 10 (0.‘𝐾) = (0.‘𝐾)
882, 23, 5, 87opnoncon 34314 . . . . . . . . 9 ((𝐾 ∈ OP ∧ (𝑌 𝑍) ∈ 𝐵) → ((𝑌 𝑍) ((oc‘𝐾)‘(𝑌 𝑍))) = (0.‘𝐾))
8935, 14, 88syl2anc 692 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) ((oc‘𝐾)‘(𝑌 𝑍))) = (0.‘𝐾))
9086, 89eqtr3d 2656 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍))) = (0.‘𝐾))
9190oveq2d 6651 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (𝑋 (0.‘𝐾)))
922, 5, 87olm01 34342 . . . . . . 7 ((𝐾 ∈ OL ∧ 𝑋𝐵) → (𝑋 (0.‘𝐾)) = (0.‘𝐾))
9318, 10, 92syl2anc 692 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (0.‘𝐾)) = (0.‘𝐾))
9491, 93eqtrd 2654 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (0.‘𝐾))
95943adant3 1079 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 ((𝑌 𝑍) (((oc‘𝐾)‘𝑌) ((oc‘𝐾)‘𝑍)))) = (0.‘𝐾))
9633, 83, 953eqtrd 2658 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾))
972, 4latjcl 17032 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑋 𝑌) ∈ 𝐵 ∧ (𝑋 𝑍) ∈ 𝐵) → ((𝑋 𝑌) (𝑋 𝑍)) ∈ 𝐵)
989, 20, 22, 97syl3anc 1324 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) (𝑋 𝑍)) ∈ 𝐵)
992, 5latmcl 17033 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ (𝑌 𝑍) ∈ 𝐵) → (𝑋 (𝑌 𝑍)) ∈ 𝐵)
1009, 10, 14, 99syl3anc 1324 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (𝑌 𝑍)) ∈ 𝐵)
1012, 3, 5, 23, 87omllaw3 34351 . . . . 5 ((𝐾 ∈ OML ∧ ((𝑋 𝑌) (𝑋 𝑍)) ∈ 𝐵 ∧ (𝑋 (𝑌 𝑍)) ∈ 𝐵) → ((((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)) ∧ ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍))))
10254, 98, 100, 101syl3anc 1324 . . . 4 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)) ∧ ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍))))
1031023adant3 1079 . . 3 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((((𝑋 𝑌) (𝑋 𝑍))(le‘𝐾)(𝑋 (𝑌 𝑍)) ∧ ((𝑋 (𝑌 𝑍)) ((oc‘𝐾)‘((𝑋 𝑌) (𝑋 𝑍)))) = (0.‘𝐾)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍))))
1048, 96, 103mp2and 714 . 2 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → ((𝑋 𝑌) (𝑋 𝑍)) = (𝑋 (𝑌 𝑍)))
105104eqcomd 2626 1 ((𝐾 ∈ OML ∧ (𝑋𝐵𝑌𝐵𝑍𝐵) ∧ (𝑋𝐶𝑌𝑋𝐶𝑍)) → (𝑋 (𝑌 𝑍)) = ((𝑋 𝑌) (𝑋 𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wcel 1988   class class class wbr 4644  cfv 5876  (class class class)co 6635  Basecbs 15838  lecple 15929  occoc 15930  joincjn 16925  meetcmee 16926  0.cp0 17018  Latclat 17026  OPcops 34278  cmccmtN 34279  OLcol 34280  OMLcoml 34281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-preset 16909  df-poset 16927  df-lub 16955  df-glb 16956  df-join 16957  df-meet 16958  df-p0 17020  df-lat 17027  df-oposet 34282  df-cmtN 34283  df-ol 34284  df-oml 34285
This theorem is referenced by:  omlfh3N  34365  omlmod1i2N  34366
  Copyright terms: Public domain W3C validator