Metamath Proof Explorer

Theorem omllaw

Description: The orthomodular law. (Contributed by NM, 18-Sep-2011)

Ref Expression
Hypotheses omllaw.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
omllaw.l ⊢ ≤ = ( le ‘ 𝐾 )
omllaw.j ⊢ ∨ = ( join ‘ 𝐾 )
omllaw.m ⊢ ∧ = ( meet ‘ 𝐾 )
omllaw.o ⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion omllaw ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → 𝑌 = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 omllaw.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 omllaw.l ⊢ ≤ = ( le ‘ 𝐾 )
3 omllaw.j ⊢ ∨ = ( join ‘ 𝐾 )
4 omllaw.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 omllaw.o ⊢ ⊥ = ( oc ‘ 𝐾 )
6 1 2 3 4 5 isoml ⊢ ( 𝐾 ∈ OML ↔ ( 𝐾 ∈ OL ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) ) )
7 6 simprbi ⊢ ( 𝐾 ∈ OML → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) )
8 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦 ) )
9 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
10 fveq2 ⊢ ( 𝑥 = 𝑋 → ( ⊥ ‘ 𝑥 ) = ( ⊥ ‘ 𝑋 ) )
11 10 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) = ( 𝑦 ∧ ( ⊥ ‘ 𝑋 ) ) )
12 9 11 oveq12d ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) = ( 𝑋 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑋 ) ) ) )
13 12 eqeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ↔ 𝑦 = ( 𝑋 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) )
14 8 13 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) ↔ ( 𝑋 ≤ 𝑦 → 𝑦 = ( 𝑋 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) ) )
15 breq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ≤ 𝑦 ↔ 𝑋 ≤ 𝑌 ) )
16 id ⊢ ( 𝑦 = 𝑌 → 𝑦 = 𝑌 )
17 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∧ ( ⊥ ‘ 𝑋 ) ) = ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) )
18 17 oveq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑋 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑋 ) ) ) = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) )
19 16 18 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( 𝑦 = ( 𝑋 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑋 ) ) ) ↔ 𝑌 = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) )
20 15 19 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ≤ 𝑦 → 𝑦 = ( 𝑋 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) ↔ ( 𝑋 ≤ 𝑌 → 𝑌 = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) ) )
21 14 20 rspc2v ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) → ( 𝑋 ≤ 𝑌 → 𝑌 = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) ) )
22 7 21 syl5com ⊢ ( 𝐾 ∈ OML → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → 𝑌 = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) ) )
23 22 3impib ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → 𝑌 = ( 𝑋 ∨ ( 𝑌 ∧ ( ⊥ ‘ 𝑋 ) ) ) ) )