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

Theorem omllaw 35031
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 35026 . . . 4 (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥))))))
76simprbi 483 . . 3 (𝐾 ∈ OML → ∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥)))))
8 breq1 4805 . . . . 5 (𝑥 = 𝑋 → (𝑥 𝑦𝑋 𝑦))
9 id 22 . . . . . . 7 (𝑥 = 𝑋𝑥 = 𝑋)
10 fveq2 6350 . . . . . . . 8 (𝑥 = 𝑋 → ( 𝑥) = ( 𝑋))
1110oveq2d 6827 . . . . . . 7 (𝑥 = 𝑋 → (𝑦 ( 𝑥)) = (𝑦 ( 𝑋)))
129, 11oveq12d 6829 . . . . . 6 (𝑥 = 𝑋 → (𝑥 (𝑦 ( 𝑥))) = (𝑋 (𝑦 ( 𝑋))))
1312eqeq2d 2768 . . . . 5 (𝑥 = 𝑋 → (𝑦 = (𝑥 (𝑦 ( 𝑥))) ↔ 𝑦 = (𝑋 (𝑦 ( 𝑋)))))
148, 13imbi12d 333 . . . 4 (𝑥 = 𝑋 → ((𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥)))) ↔ (𝑋 𝑦𝑦 = (𝑋 (𝑦 ( 𝑋))))))
15 breq2 4806 . . . . 5 (𝑦 = 𝑌 → (𝑋 𝑦𝑋 𝑌))
16 id 22 . . . . . 6 (𝑦 = 𝑌𝑦 = 𝑌)
17 oveq1 6818 . . . . . . 7 (𝑦 = 𝑌 → (𝑦 ( 𝑋)) = (𝑌 ( 𝑋)))
1817oveq2d 6827 . . . . . 6 (𝑦 = 𝑌 → (𝑋 (𝑦 ( 𝑋))) = (𝑋 (𝑌 ( 𝑋))))
1916, 18eqeq12d 2773 . . . . 5 (𝑦 = 𝑌 → (𝑦 = (𝑋 (𝑦 ( 𝑋))) ↔ 𝑌 = (𝑋 (𝑌 ( 𝑋)))))
2015, 19imbi12d 333 . . . 4 (𝑦 = 𝑌 → ((𝑋 𝑦𝑦 = (𝑋 (𝑦 ( 𝑋)))) ↔ (𝑋 𝑌𝑌 = (𝑋 (𝑌 ( 𝑋))))))
2114, 20rspc2v 3459 . . 3 ((𝑋𝐵𝑌𝐵) → (∀𝑥𝐵𝑦𝐵 (𝑥 𝑦𝑦 = (𝑥 (𝑦 ( 𝑥)))) → (𝑋 𝑌𝑌 = (𝑋 (𝑌 ( 𝑋))))))
227, 21syl5com 31 . 2 (𝐾 ∈ OML → ((𝑋𝐵𝑌𝐵) → (𝑋 𝑌𝑌 = (𝑋 (𝑌 ( 𝑋))))))
23223impib 1109 1 ((𝐾 ∈ OML ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌𝑌 = (𝑋 (𝑌 ( 𝑋)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1630  wcel 2137  wral 3048   class class class wbr 4802  cfv 6047  (class class class)co 6811  Basecbs 16057  lecple 16148  occoc 16149  joincjn 17143  meetcmee 17144  OLcol 34962  OMLcoml 34963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-iota 6010  df-fv 6055  df-ov 6814  df-oml 34967
This theorem is referenced by:  omllaw2N  35032  omllaw3  35033  omllaw4  35034
  Copyright terms: Public domain W3C validator