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

Theorem omllaw 36498
 Description: The orthomodular law. (Contributed by NM, 18-Sep-2011.)
Hypotheses
Ref Expression
omllaw.b 𝐵 = (Base‘𝐾)
omllaw.l = (le‘𝐾)
omllaw.j = (join‘𝐾)
omllaw.m = (meet‘𝐾)
omllaw.o = (oc‘𝐾)
Assertion
Ref Expression
omllaw ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌𝑌 = (𝑋 (𝑌 ( 𝑋)))))

Proof of Theorem omllaw
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omllaw.b . . . . 5 𝐵 = (Base‘𝐾)
2 omllaw.l . . . . 5 = (le‘𝐾)
3 omllaw.j . . . . 5 = (join‘𝐾)
4 omllaw.m . . . . 5 = (meet‘𝐾)
5 omllaw.o . . . . 5 = (oc‘𝐾)
61, 2, 3, 4, 5isoml 36493 . . . 4 (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥))))))
76simprbi 500 . . 3 (𝐾 ∈ OML → ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥)))))
8 breq1 5045 . . . . 5 (𝑥 = 𝑋 → (𝑥 𝑦𝑋 𝑦))
9 id 22 . . . . . . 7 (𝑥 = 𝑋𝑥 = 𝑋)
10 fveq2 6652 . . . . . . . 8 (𝑥 = 𝑋 → ( 𝑥) = ( 𝑋))
1110oveq2d 7156 . . . . . . 7 (𝑥 = 𝑋 → (𝑦 ( 𝑥)) = (𝑦 ( 𝑋)))
129, 11oveq12d 7158 . . . . . 6 (𝑥 = 𝑋 → (𝑥 (𝑦 ( 𝑥))) = (𝑋 (𝑦 ( 𝑋))))
1312eqeq2d 2833 . . . . 5 (𝑥 = 𝑋 → (𝑦 = (𝑥 (𝑦 ( 𝑥))) ↔ 𝑦 = (𝑋 (𝑦 ( 𝑋)))))
148, 13imbi12d 348 . . . 4 (𝑥 = 𝑋 → ((𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥)))) ↔ (𝑋 𝑦𝑦 = (𝑋 (𝑦 ( 𝑋))))))
15 breq2 5046 . . . . 5 (𝑦 = 𝑌 → (𝑋 𝑦𝑋 𝑌))
16 id 22 . . . . . 6 (𝑦 = 𝑌𝑦 = 𝑌)
17 oveq1 7147 . . . . . . 7 (𝑦 = 𝑌 → (𝑦 ( 𝑋)) = (𝑌 ( 𝑋)))
1817oveq2d 7156 . . . . . 6 (𝑦 = 𝑌 → (𝑋 (𝑦 ( 𝑋))) = (𝑋 (𝑌 ( 𝑋))))
1916, 18eqeq12d 2838 . . . . 5 (𝑦 = 𝑌 → (𝑦 = (𝑋 (𝑦 ( 𝑋))) ↔ 𝑌 = (𝑋 (𝑌 ( 𝑋)))))
2015, 19imbi12d 348 . . . 4 (𝑦 = 𝑌 → ((𝑋 𝑦𝑦 = (𝑋 (𝑦 ( 𝑋)))) ↔ (𝑋 𝑌𝑌 = (𝑋 (𝑌 ( 𝑋))))))
2114, 20rspc2v 3608 . . 3 ((𝑋𝐵𝑌𝐵) → (∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥)))) → (𝑋 𝑌𝑌 = (𝑋 (𝑌 ( 𝑋))))))
227, 21syl5com 31 . 2 (𝐾 ∈ OML → ((𝑋𝐵𝑌𝐵) → (𝑋 𝑌𝑌 = (𝑋 (𝑌 ( 𝑋))))))
23223impib 1113 1 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌𝑌 = (𝑋 (𝑌 ( 𝑋)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2114  ∀wral 3130   class class class wbr 5042  ‘cfv 6334  (class class class)co 7140  Basecbs 16474  lecple 16563  occoc 16564  joincjn 17545  meetcmee 17546  OLcol 36429  OMLcoml 36430 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rab 3139  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-iota 6293  df-fv 6342  df-ov 7143  df-oml 36434 This theorem is referenced by:  omllaw2N  36499  omllaw3  36500  omllaw4  36501
 Copyright terms: Public domain W3C validator