Theorem omllaw 40566

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.

Step	Hyp	Ref	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‘𝐾)
6	1, 2, 3, 4, 5	isoml 40561	. . . 4 ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
7	6	simprbi 503	. . 3 ⊢ (𝐾 ∈ OML → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))
8		breq1 5111	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦))
9		id 23	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
10		fveq2 6916	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑋))
11	10	oveq2d 7467	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑦 ∧ ( ⊥ ‘𝑥)) = (𝑦 ∧ ( ⊥ ‘𝑋)))
12	9, 11	oveq12d 7469	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))) = (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋))))
13	12	eqeq2d 2774	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))) ↔ 𝑦 = (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋)))))
14	8, 13	imbi12d 347	. . . 4 ⊢ (𝑥 = 𝑋 → ((𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))) ↔ (𝑋 ≤ 𝑦 → 𝑦 = (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋))))))
15		breq2 5112	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑋 ≤ 𝑦 ↔ 𝑋 ≤ 𝑌))
16		id 23	. . . . . 6 ⊢ (𝑦 = 𝑌 → 𝑦 = 𝑌)
17		oveq1 7458	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (𝑦 ∧ ( ⊥ ‘𝑋)) = (𝑌 ∧ ( ⊥ ‘𝑋)))
18	17	oveq2d 7467	. . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋))) = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))
19	16, 18	eqeq12d 2779	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑦 = (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋))) ↔ 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋)))))
20	15, 19	imbi12d 347	. . . 4 ⊢ (𝑦 = 𝑌 → ((𝑋 ≤ 𝑦 → 𝑦 = (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋)))) ↔ (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))))
21	14, 20	rspc2v 3590	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))))
22	7, 21	syl5com 32	. 2 ⊢ (𝐾 ∈ OML → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))))
23	22	3impib 1134	1 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋)))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∀wral 3080   class class class wbr 5108  ‘cfv 6566  (class class class)co 7451  Basecbs 17431  lecple 17479  occoc 17480  joincjn 18535  meetcmee 18536  OLcol 40497  OMLcoml 40498

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-oml 40502

This theorem is used by:  omllaw2N  40567  omllaw3  40568  omllaw4  40569