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 37766
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 30602 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 37750 . . . . 5 (𝐾 ∈ OML β†’ 𝐾 ∈ Lat)
2 omlfh1.b . . . . . 6 𝐡 = (Baseβ€˜πΎ)
3 eqid 2733 . . . . . 6 (leβ€˜πΎ) = (leβ€˜πΎ)
4 omlfh1.j . . . . . 6 ∨ = (joinβ€˜πΎ)
5 omlfh1.m . . . . . 6 ∧ = (meetβ€˜πΎ)
62, 3, 4, 5latledi 18371 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))(leβ€˜πΎ)(𝑋 ∧ (π‘Œ ∨ 𝑍)))
71, 6sylan 581 . . . 4 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))(leβ€˜πΎ)(𝑋 ∧ (π‘Œ ∨ 𝑍)))
873adant3 1133 . . 3 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))(leβ€˜πΎ)(𝑋 ∧ (π‘Œ ∨ 𝑍)))
91adantr 482 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ Lat)
10 simpr1 1195 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝑋 ∈ 𝐡)
11 simpr2 1196 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ π‘Œ ∈ 𝐡)
12 simpr3 1197 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝑍 ∈ 𝐡)
132, 4latjcl 18333 . . . . . . . 8 ((𝐾 ∈ Lat ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) β†’ (π‘Œ ∨ 𝑍) ∈ 𝐡)
149, 11, 12, 13syl3anc 1372 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (π‘Œ ∨ 𝑍) ∈ 𝐡)
152, 5latmcom 18357 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ (π‘Œ ∨ 𝑍) ∈ 𝐡) β†’ (𝑋 ∧ (π‘Œ ∨ 𝑍)) = ((π‘Œ ∨ 𝑍) ∧ 𝑋))
169, 10, 14, 15syl3anc 1372 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ (π‘Œ ∨ 𝑍)) = ((π‘Œ ∨ 𝑍) ∧ 𝑋))
17 omlol 37748 . . . . . . . . 9 (𝐾 ∈ OML β†’ 𝐾 ∈ OL)
1817adantr 482 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ OL)
192, 5latmcl 18334 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (𝑋 ∧ π‘Œ) ∈ 𝐡)
209, 10, 11, 19syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ π‘Œ) ∈ 𝐡)
212, 5latmcl 18334 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) β†’ (𝑋 ∧ 𝑍) ∈ 𝐡)
229, 10, 12, 21syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ 𝑍) ∈ 𝐡)
23 eqid 2733 . . . . . . . . 9 (ocβ€˜πΎ) = (ocβ€˜πΎ)
242, 4, 5, 23oldmj1 37729 . . . . . . . 8 ((𝐾 ∈ OL ∧ (𝑋 ∧ π‘Œ) ∈ 𝐡 ∧ (𝑋 ∧ 𝑍) ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))) = (((ocβ€˜πΎ)β€˜(𝑋 ∧ π‘Œ)) ∧ ((ocβ€˜πΎ)β€˜(𝑋 ∧ 𝑍))))
2518, 20, 22, 24syl3anc 1372 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))) = (((ocβ€˜πΎ)β€˜(𝑋 ∧ π‘Œ)) ∧ ((ocβ€˜πΎ)β€˜(𝑋 ∧ 𝑍))))
262, 4, 5, 23oldmm1 37725 . . . . . . . . 9 ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∧ π‘Œ)) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)))
2718, 10, 11, 26syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∧ π‘Œ)) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)))
282, 4, 5, 23oldmm1 37725 . . . . . . . . 9 ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∧ 𝑍)) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))
2918, 10, 12, 28syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∧ 𝑍)) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))
3027, 29oveq12d 7376 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (((ocβ€˜πΎ)β€˜(𝑋 ∧ π‘Œ)) ∧ ((ocβ€˜πΎ)β€˜(𝑋 ∧ 𝑍))) = ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))))
3125, 30eqtrd 2773 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))) = ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))))
3216, 31oveq12d 7376 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)))) = (((π‘Œ ∨ 𝑍) ∧ 𝑋) ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))))
33323adant3 1133 . . . 4 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)))) = (((π‘Œ ∨ 𝑍) ∧ 𝑋) ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))))
34 omlop 37749 . . . . . . . . . . 11 (𝐾 ∈ OML β†’ 𝐾 ∈ OP)
3534adantr 482 . . . . . . . . . 10 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ OP)
362, 23opoccl 37702 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜π‘‹) ∈ 𝐡)
3735, 10, 36syl2anc 585 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜π‘‹) ∈ 𝐡)
382, 23opoccl 37702 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ π‘Œ ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡)
3935, 11, 38syl2anc 585 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡)
402, 4latjcl 18333 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((ocβ€˜πΎ)β€˜π‘‹) ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡) β†’ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∈ 𝐡)
419, 37, 39, 40syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∈ 𝐡)
422, 23opoccl 37702 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑍 ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡)
4335, 12, 42syl2anc 585 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡)
442, 4latjcl 18333 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((ocβ€˜πΎ)β€˜π‘‹) ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡) β†’ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡)
459, 37, 43, 44syl3anc 1372 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡)
462, 5latmcl 18334 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∈ 𝐡 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡) β†’ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) ∈ 𝐡)
479, 41, 45, 46syl3anc 1372 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) ∈ 𝐡)
482, 5latmassOLD 37737 . . . . . . 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 37758 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (π‘‹πΆπ‘Œ ↔ 𝑋𝐢((ocβ€˜πΎ)β€˜π‘Œ)))
53523adant3r3 1185 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (π‘‹πΆπ‘Œ ↔ 𝑋𝐢((ocβ€˜πΎ)β€˜π‘Œ)))
54 simpl 484 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ OML)
552, 4, 5, 23, 51cmtbr3N 37762 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡) β†’ (𝑋𝐢((ocβ€˜πΎ)β€˜π‘Œ) ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ))))
5654, 10, 39, 55syl3anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋𝐢((ocβ€˜πΎ)β€˜π‘Œ) ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ))))
5753, 56bitrd 279 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (π‘‹πΆπ‘Œ ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ))))
5857biimpa 478 . . . . . . . . . 10 (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) ∧ π‘‹πΆπ‘Œ) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)))
5958adantrr 716 . . . . . . . . 9 (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)))
60593impa 1111 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)))
612, 23, 51cmt2N 37758 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) β†’ (𝑋𝐢𝑍 ↔ 𝑋𝐢((ocβ€˜πΎ)β€˜π‘)))
62613adant3r2 1184 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋𝐢𝑍 ↔ 𝑋𝐢((ocβ€˜πΎ)β€˜π‘)))
632, 4, 5, 23, 51cmtbr3N 37762 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡) β†’ (𝑋𝐢((ocβ€˜πΎ)β€˜π‘) ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
6454, 10, 43, 63syl3anc 1372 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋𝐢((ocβ€˜πΎ)β€˜π‘) ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
6562, 64bitrd 279 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋𝐢𝑍 ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
6665biimpa 478 . . . . . . . . . 10 (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) ∧ 𝑋𝐢𝑍) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘)))
6766adantrl 715 . . . . . . . . 9 (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘)))
68673impa 1111 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘)))
6960, 68oveq12d 7376 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) ∧ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))) = ((𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
702, 5latmmdiN 37742 . . . . . . . . 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 37742 . . . . . . . . 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 7374 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((π‘Œ ∨ 𝑍) ∧ (𝑋 ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))))) = ((π‘Œ ∨ 𝑍) ∧ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))))
782, 5latmcl 18334 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡) β†’ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡)
799, 39, 43, 78syl3anc 1372 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡)
802, 5latm12 37738 . . . . . . 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 37729 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜(π‘Œ ∨ 𝑍)) = (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))
8518, 11, 12, 84syl3anc 1372 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜(π‘Œ ∨ 𝑍)) = (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))
8685oveq2d 7374 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((π‘Œ ∨ 𝑍) ∧ ((ocβ€˜πΎ)β€˜(π‘Œ ∨ 𝑍))) = ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘))))
87 eqid 2733 . . . . . . . . . 10 (0.β€˜πΎ) = (0.β€˜πΎ)
882, 23, 5, 87opnoncon 37716 . . . . . . . . 9 ((𝐾 ∈ OP ∧ (π‘Œ ∨ 𝑍) ∈ 𝐡) β†’ ((π‘Œ ∨ 𝑍) ∧ ((ocβ€˜πΎ)β€˜(π‘Œ ∨ 𝑍))) = (0.β€˜πΎ))
8935, 14, 88syl2anc 585 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((π‘Œ ∨ 𝑍) ∧ ((ocβ€˜πΎ)β€˜(π‘Œ ∨ 𝑍))) = (0.β€˜πΎ))
9086, 89eqtr3d 2775 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘))) = (0.β€˜πΎ))
9190oveq2d 7374 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))) = (𝑋 ∧ (0.β€˜πΎ)))
922, 5, 87olm01 37744 . . . . . . 7 ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐡) β†’ (𝑋 ∧ (0.β€˜πΎ)) = (0.β€˜πΎ))
9318, 10, 92syl2anc 585 . . . . . 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 18333 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑋 ∧ π‘Œ) ∈ 𝐡 ∧ (𝑋 ∧ 𝑍) ∈ 𝐡) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐡)
989, 20, 22, 97syl3anc 1372 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐡)
992, 5latmcl 18334 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ (π‘Œ ∨ 𝑍) ∈ 𝐡) β†’ (𝑋 ∧ (π‘Œ ∨ 𝑍)) ∈ 𝐡)
1009, 10, 14, 99syl3anc 1372 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ (π‘Œ ∨ 𝑍)) ∈ 𝐡)
1012, 3, 5, 23, 87omllaw3 37753 . . . . 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 698 . 2 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (π‘Œ ∨ 𝑍)))
105104eqcomd 2739 1 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (π‘Œ ∨ 𝑍)) = ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   class class class wbr 5106  β€˜cfv 6497  (class class class)co 7358  Basecbs 17088  lecple 17145  occoc 17146  joincjn 18205  meetcmee 18206  0.cp0 18317  Latclat 18325  OPcops 37680  cmccmtN 37681  OLcol 37682  OMLcoml 37683
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-proset 18189  df-poset 18207  df-lub 18240  df-glb 18241  df-join 18242  df-meet 18243  df-p0 18319  df-lat 18326  df-oposet 37684  df-cmtN 37685  df-ol 37686  df-oml 37687
This theorem is referenced by:  omlfh3N  37767  omlmod1i2N  37768
  Copyright terms: Public domain W3C validator