Theorem omllaw 38715

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 38710	. . . 4 ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))))
7	6	simprbi 496	. . 3 ⊢ (𝐾 ∈ OML → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))
8		breq1 5151	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦))
9		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
10		fveq2 6897	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑋))
11	10	oveq2d 7436	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑦 ∧ ( ⊥ ‘𝑥)) = (𝑦 ∧ ( ⊥ ‘𝑋)))
12	9, 11	oveq12d 7438	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))) = (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋))))
13	12	eqeq2d 2739	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))) ↔ 𝑦 = (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋)))))
14	8, 13	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝑋 → ((𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))) ↔ (𝑋 ≤ 𝑦 → 𝑦 = (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋))))))
15		breq2 5152	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑋 ≤ 𝑦 ↔ 𝑋 ≤ 𝑌))
16		id 22	. . . . . 6 ⊢ (𝑦 = 𝑌 → 𝑦 = 𝑌)
17		oveq1 7427	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (𝑦 ∧ ( ⊥ ‘𝑋)) = (𝑌 ∧ ( ⊥ ‘𝑋)))
18	17	oveq2d 7436	. . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋))) = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))
19	16, 18	eqeq12d 2744	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑦 = (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋))) ↔ 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋)))))
20	15, 19	imbi12d 344	. . . 4 ⊢ (𝑦 = 𝑌 → ((𝑋 ≤ 𝑦 → 𝑦 = (𝑋 ∨ (𝑦 ∧ ( ⊥ ‘𝑋)))) ↔ (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))))
21	14, 20	rspc2v 3620	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))))
22	7, 21	syl5com 31	. 2 ⊢ (𝐾 ∈ OML → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))))
23	22	3impib 1114	1 ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋)))))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  ∀wral 3058   class class class wbr 5148  ‘cfv 6548  (class class class)co 7420  Basecbs 17180  lecple 17240  occoc 17241  joincjn 18303  meetcmee 18304  OLcol 38646  OMLcoml 38647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-oml 38651

This theorem is referenced by:  omllaw2N  38716  omllaw3  38717  omllaw4  38718