Description: Properties that determine an orthomodular lattice. (Contributed by NM, 18-Sep-2011) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | isomli.0 | ⊢ 𝐾 ∈ OL | |
| isomli.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | ||
| isomli.l | ⊢ ≤ = ( le ‘ 𝐾 ) | ||
| isomli.j | ⊢ ∨ = ( join ‘ 𝐾 ) | ||
| isomli.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | ||
| isomli.o | ⊢ ⊥ = ( oc ‘ 𝐾 ) | ||
| isomli.7 | ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) ) | ||
| Assertion | isomliN | ⊢ 𝐾 ∈ OML |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isomli.0 | ⊢ 𝐾 ∈ OL | |
| 2 | isomli.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
| 3 | isomli.l | ⊢ ≤ = ( le ‘ 𝐾 ) | |
| 4 | isomli.j | ⊢ ∨ = ( join ‘ 𝐾 ) | |
| 5 | isomli.m | ⊢ ∧ = ( meet ‘ 𝐾 ) | |
| 6 | isomli.o | ⊢ ⊥ = ( oc ‘ 𝐾 ) | |
| 7 | isomli.7 | ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) ) | |
| 8 | 7 | rgen2 | ⊢ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) |
| 9 | 2 3 4 5 6 | isoml | ⊢ ( 𝐾 ∈ OML ↔ ( 𝐾 ∈ OL ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 → 𝑦 = ( 𝑥 ∨ ( 𝑦 ∧ ( ⊥ ‘ 𝑥 ) ) ) ) ) ) |
| 10 | 1 8 9 | mpbir2an | ⊢ 𝐾 ∈ OML |