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 38431
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 31138 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 38415 . . . . 5 (𝐾 ∈ OML β†’ 𝐾 ∈ Lat)
2 omlfh1.b . . . . . 6 𝐡 = (Baseβ€˜πΎ)
3 eqid 2730 . . . . . 6 (leβ€˜πΎ) = (leβ€˜πΎ)
4 omlfh1.j . . . . . 6 ∨ = (joinβ€˜πΎ)
5 omlfh1.m . . . . . 6 ∧ = (meetβ€˜πΎ)
62, 3, 4, 5latledi 18434 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))(leβ€˜πΎ)(𝑋 ∧ (π‘Œ ∨ 𝑍)))
71, 6sylan 578 . . . 4 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))(leβ€˜πΎ)(𝑋 ∧ (π‘Œ ∨ 𝑍)))
873adant3 1130 . . 3 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))(leβ€˜πΎ)(𝑋 ∧ (π‘Œ ∨ 𝑍)))
91adantr 479 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ Lat)
10 simpr1 1192 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝑋 ∈ 𝐡)
11 simpr2 1193 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ π‘Œ ∈ 𝐡)
12 simpr3 1194 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝑍 ∈ 𝐡)
132, 4latjcl 18396 . . . . . . . 8 ((𝐾 ∈ Lat ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) β†’ (π‘Œ ∨ 𝑍) ∈ 𝐡)
149, 11, 12, 13syl3anc 1369 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (π‘Œ ∨ 𝑍) ∈ 𝐡)
152, 5latmcom 18420 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ (π‘Œ ∨ 𝑍) ∈ 𝐡) β†’ (𝑋 ∧ (π‘Œ ∨ 𝑍)) = ((π‘Œ ∨ 𝑍) ∧ 𝑋))
169, 10, 14, 15syl3anc 1369 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ (π‘Œ ∨ 𝑍)) = ((π‘Œ ∨ 𝑍) ∧ 𝑋))
17 omlol 38413 . . . . . . . . 9 (𝐾 ∈ OML β†’ 𝐾 ∈ OL)
1817adantr 479 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ OL)
192, 5latmcl 18397 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (𝑋 ∧ π‘Œ) ∈ 𝐡)
209, 10, 11, 19syl3anc 1369 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ π‘Œ) ∈ 𝐡)
212, 5latmcl 18397 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) β†’ (𝑋 ∧ 𝑍) ∈ 𝐡)
229, 10, 12, 21syl3anc 1369 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ 𝑍) ∈ 𝐡)
23 eqid 2730 . . . . . . . . 9 (ocβ€˜πΎ) = (ocβ€˜πΎ)
242, 4, 5, 23oldmj1 38394 . . . . . . . 8 ((𝐾 ∈ OL ∧ (𝑋 ∧ π‘Œ) ∈ 𝐡 ∧ (𝑋 ∧ 𝑍) ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))) = (((ocβ€˜πΎ)β€˜(𝑋 ∧ π‘Œ)) ∧ ((ocβ€˜πΎ)β€˜(𝑋 ∧ 𝑍))))
2518, 20, 22, 24syl3anc 1369 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))) = (((ocβ€˜πΎ)β€˜(𝑋 ∧ π‘Œ)) ∧ ((ocβ€˜πΎ)β€˜(𝑋 ∧ 𝑍))))
262, 4, 5, 23oldmm1 38390 . . . . . . . . 9 ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∧ π‘Œ)) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)))
2718, 10, 11, 26syl3anc 1369 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∧ π‘Œ)) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)))
282, 4, 5, 23oldmm1 38390 . . . . . . . . 9 ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∧ 𝑍)) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))
2918, 10, 12, 28syl3anc 1369 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜(𝑋 ∧ 𝑍)) = (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))
3027, 29oveq12d 7429 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (((ocβ€˜πΎ)β€˜(𝑋 ∧ π‘Œ)) ∧ ((ocβ€˜πΎ)β€˜(𝑋 ∧ 𝑍))) = ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))))
3125, 30eqtrd 2770 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))) = ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))))
3216, 31oveq12d 7429 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)))) = (((π‘Œ ∨ 𝑍) ∧ 𝑋) ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))))
33323adant3 1130 . . . 4 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)))) = (((π‘Œ ∨ 𝑍) ∧ 𝑋) ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))))
34 omlop 38414 . . . . . . . . . . 11 (𝐾 ∈ OML β†’ 𝐾 ∈ OP)
3534adantr 479 . . . . . . . . . 10 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ OP)
362, 23opoccl 38367 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜π‘‹) ∈ 𝐡)
3735, 10, 36syl2anc 582 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜π‘‹) ∈ 𝐡)
382, 23opoccl 38367 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ π‘Œ ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡)
3935, 11, 38syl2anc 582 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡)
402, 4latjcl 18396 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((ocβ€˜πΎ)β€˜π‘‹) ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡) β†’ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∈ 𝐡)
419, 37, 39, 40syl3anc 1369 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∈ 𝐡)
422, 23opoccl 38367 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑍 ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡)
4335, 12, 42syl2anc 582 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡)
442, 4latjcl 18396 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ ((ocβ€˜πΎ)β€˜π‘‹) ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡) β†’ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡)
459, 37, 43, 44syl3anc 1369 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡)
462, 5latmcl 18397 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∈ 𝐡 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡) β†’ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) ∈ 𝐡)
479, 41, 45, 46syl3anc 1369 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) ∈ 𝐡)
482, 5latmassOLD 38402 . . . . . . 7 ((𝐾 ∈ OL ∧ ((π‘Œ ∨ 𝑍) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) ∈ 𝐡)) β†’ (((π‘Œ ∨ 𝑍) ∧ 𝑋) ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))) = ((π‘Œ ∨ 𝑍) ∧ (𝑋 ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))))))
4918, 14, 10, 47, 48syl13anc 1370 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (((π‘Œ ∨ 𝑍) ∧ 𝑋) ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))) = ((π‘Œ ∨ 𝑍) ∧ (𝑋 ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))))))
50493adant3 1130 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (((π‘Œ ∨ 𝑍) ∧ 𝑋) ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))) = ((π‘Œ ∨ 𝑍) ∧ (𝑋 ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))))))
51 omlfh1.c . . . . . . . . . . . . . 14 𝐢 = (cmβ€˜πΎ)
522, 23, 51cmt2N 38423 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (π‘‹πΆπ‘Œ ↔ 𝑋𝐢((ocβ€˜πΎ)β€˜π‘Œ)))
53523adant3r3 1182 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (π‘‹πΆπ‘Œ ↔ 𝑋𝐢((ocβ€˜πΎ)β€˜π‘Œ)))
54 simpl 481 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ OML)
552, 4, 5, 23, 51cmtbr3N 38427 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡) β†’ (𝑋𝐢((ocβ€˜πΎ)β€˜π‘Œ) ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ))))
5654, 10, 39, 55syl3anc 1369 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋𝐢((ocβ€˜πΎ)β€˜π‘Œ) ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ))))
5753, 56bitrd 278 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (π‘‹πΆπ‘Œ ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ))))
5857biimpa 475 . . . . . . . . . 10 (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) ∧ π‘‹πΆπ‘Œ) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)))
5958adantrr 713 . . . . . . . . 9 (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)))
60593impa 1108 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)))
612, 23, 51cmt2N 38423 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) β†’ (𝑋𝐢𝑍 ↔ 𝑋𝐢((ocβ€˜πΎ)β€˜π‘)))
62613adant3r2 1181 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋𝐢𝑍 ↔ 𝑋𝐢((ocβ€˜πΎ)β€˜π‘)))
632, 4, 5, 23, 51cmtbr3N 38427 . . . . . . . . . . . . 13 ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡) β†’ (𝑋𝐢((ocβ€˜πΎ)β€˜π‘) ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
6454, 10, 43, 63syl3anc 1369 . . . . . . . . . . . 12 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋𝐢((ocβ€˜πΎ)β€˜π‘) ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
6562, 64bitrd 278 . . . . . . . . . . 11 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋𝐢𝑍 ↔ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
6665biimpa 475 . . . . . . . . . 10 (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) ∧ 𝑋𝐢𝑍) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘)))
6766adantrl 712 . . . . . . . . 9 (((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘)))
68673impa 1108 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))) = (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘)))
6960, 68oveq12d 7429 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) ∧ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))) = ((𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
702, 5latmmdiN 38407 . . . . . . . . 9 ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐡 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∈ 𝐡 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡)) β†’ (𝑋 ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))) = ((𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) ∧ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))))
7118, 10, 41, 45, 70syl13anc 1370 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))) = ((𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) ∧ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))))
72713adant3 1130 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))) = ((𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ))) ∧ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))))
732, 5latmmdiN 38407 . . . . . . . . 9 ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘))) = ((𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
7418, 10, 39, 43, 73syl13anc 1370 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘))) = ((𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
75743adant3 1130 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘))) = ((𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (𝑋 ∧ ((ocβ€˜πΎ)β€˜π‘))))
7669, 72, 753eqtr4d 2780 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))) = (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘))))
7776oveq2d 7427 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((π‘Œ ∨ 𝑍) ∧ (𝑋 ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘))))) = ((π‘Œ ∨ 𝑍) ∧ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))))
782, 5latmcl 18397 . . . . . . . 8 ((𝐾 ∈ Lat ∧ ((ocβ€˜πΎ)β€˜π‘Œ) ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜π‘) ∈ 𝐡) β†’ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡)
799, 39, 43, 78syl3anc 1369 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡)
802, 5latm12 38403 . . . . . . 7 ((𝐾 ∈ OL ∧ ((π‘Œ ∨ 𝑍) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)) ∈ 𝐡)) β†’ ((π‘Œ ∨ 𝑍) ∧ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))) = (𝑋 ∧ ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))))
8118, 14, 10, 79, 80syl13anc 1370 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((π‘Œ ∨ 𝑍) ∧ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))) = (𝑋 ∧ ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))))
82813adant3 1130 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((π‘Œ ∨ 𝑍) ∧ (𝑋 ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))) = (𝑋 ∧ ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))))
8350, 77, 823eqtrd 2774 . . . 4 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (((π‘Œ ∨ 𝑍) ∧ 𝑋) ∧ ((((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘Œ)) ∧ (((ocβ€˜πΎ)β€˜π‘‹) ∨ ((ocβ€˜πΎ)β€˜π‘)))) = (𝑋 ∧ ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))))
842, 4, 5, 23oldmj1 38394 . . . . . . . . . 10 ((𝐾 ∈ OL ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜(π‘Œ ∨ 𝑍)) = (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))
8518, 11, 12, 84syl3anc 1369 . . . . . . . . 9 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((ocβ€˜πΎ)β€˜(π‘Œ ∨ 𝑍)) = (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))
8685oveq2d 7427 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((π‘Œ ∨ 𝑍) ∧ ((ocβ€˜πΎ)β€˜(π‘Œ ∨ 𝑍))) = ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘))))
87 eqid 2730 . . . . . . . . . 10 (0.β€˜πΎ) = (0.β€˜πΎ)
882, 23, 5, 87opnoncon 38381 . . . . . . . . 9 ((𝐾 ∈ OP ∧ (π‘Œ ∨ 𝑍) ∈ 𝐡) β†’ ((π‘Œ ∨ 𝑍) ∧ ((ocβ€˜πΎ)β€˜(π‘Œ ∨ 𝑍))) = (0.β€˜πΎ))
8935, 14, 88syl2anc 582 . . . . . . . 8 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((π‘Œ ∨ 𝑍) ∧ ((ocβ€˜πΎ)β€˜(π‘Œ ∨ 𝑍))) = (0.β€˜πΎ))
9086, 89eqtr3d 2772 . . . . . . 7 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘))) = (0.β€˜πΎ))
9190oveq2d 7427 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))) = (𝑋 ∧ (0.β€˜πΎ)))
922, 5, 87olm01 38409 . . . . . . 7 ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐡) β†’ (𝑋 ∧ (0.β€˜πΎ)) = (0.β€˜πΎ))
9318, 10, 92syl2anc 582 . . . . . 6 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ (0.β€˜πΎ)) = (0.β€˜πΎ))
9491, 93eqtrd 2770 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))) = (0.β€˜πΎ))
95943adant3 1130 . . . 4 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ ((π‘Œ ∨ 𝑍) ∧ (((ocβ€˜πΎ)β€˜π‘Œ) ∧ ((ocβ€˜πΎ)β€˜π‘)))) = (0.β€˜πΎ))
9633, 83, 953eqtrd 2774 . . 3 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)))) = (0.β€˜πΎ))
972, 4latjcl 18396 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑋 ∧ π‘Œ) ∈ 𝐡 ∧ (𝑋 ∧ 𝑍) ∈ 𝐡) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐡)
989, 20, 22, 97syl3anc 1369 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐡)
992, 5latmcl 18397 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ (π‘Œ ∨ 𝑍) ∈ 𝐡) β†’ (𝑋 ∧ (π‘Œ ∨ 𝑍)) ∈ 𝐡)
1009, 10, 14, 99syl3anc 1369 . . . . 5 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (𝑋 ∧ (π‘Œ ∨ 𝑍)) ∈ 𝐡)
1012, 3, 5, 23, 87omllaw3 38418 . . . . 5 ((𝐾 ∈ OML ∧ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)) ∈ 𝐡 ∧ (𝑋 ∧ (π‘Œ ∨ 𝑍)) ∈ 𝐡) β†’ ((((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))(leβ€˜πΎ)(𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)))) = (0.β€˜πΎ)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (π‘Œ ∨ 𝑍))))
10254, 98, 100, 101syl3anc 1369 . . . 4 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))(leβ€˜πΎ)(𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)))) = (0.β€˜πΎ)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (π‘Œ ∨ 𝑍))))
1031023adant3 1130 . . 3 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍))(leβ€˜πΎ)(𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((𝑋 ∧ (π‘Œ ∨ 𝑍)) ∧ ((ocβ€˜πΎ)β€˜((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)))) = (0.β€˜πΎ)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (π‘Œ ∨ 𝑍))))
1048, 96, 103mp2and 695 . 2 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)) = (𝑋 ∧ (π‘Œ ∨ 𝑍)))
105104eqcomd 2736 1 ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡) ∧ (π‘‹πΆπ‘Œ ∧ 𝑋𝐢𝑍)) β†’ (𝑋 ∧ (π‘Œ ∨ 𝑍)) = ((𝑋 ∧ π‘Œ) ∨ (𝑋 ∧ 𝑍)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   class class class wbr 5147  β€˜cfv 6542  (class class class)co 7411  Basecbs 17148  lecple 17208  occoc 17209  joincjn 18268  meetcmee 18269  0.cp0 18380  Latclat 18388  OPcops 38345  cmccmtN 38346  OLcol 38347  OMLcoml 38348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-proset 18252  df-poset 18270  df-lub 18303  df-glb 18304  df-join 18305  df-meet 18306  df-p0 18382  df-lat 18389  df-oposet 38349  df-cmtN 38350  df-ol 38351  df-oml 38352
This theorem is referenced by:  omlfh3N  38432  omlmod1i2N  38433
  Copyright terms: Public domain W3C validator