Metamath Proof Explorer

Theorem opoccl

Description: Closure of orthocomplement operation. ( choccl analog.) (Contributed by NM, 20-Oct-2011)

Ref Expression
Hypotheses opoccl.b ⊢ B = Base K
opoccl.o ⊢ ⊥ ˙ = oc ⁡ K
Assertion opoccl ⊢ K ∈ OP ∧ X ∈ B → ⊥ ˙ ⁡ X ∈ B

Proof

Step Hyp Ref Expression
1 opoccl.b ⊢ B = Base K
2 opoccl.o ⊢ ⊥ ˙ = oc ⁡ K
3 eqid ⊢ ≤ K = ≤ K
4 eqid ⊢ join ⁡ K = join ⁡ K
5 eqid ⊢ meet ⁡ K = meet ⁡ K
6 eqid ⊢ 0. ⁡ K = 0. ⁡ K
7 eqid ⊢ 1. ⁡ K = 1. ⁡ K
8 1 3 2 4 5 6 7 oposlem ⊢ K ∈ OP ∧ X ∈ B ∧ X ∈ B → ⊥ ˙ ⁡ X ∈ B ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X ∧ X ≤ K X → ⊥ ˙ ⁡ X ≤ K ⊥ ˙ ⁡ X ∧ X join ⁡ K ⊥ ˙ ⁡ X = 1. ⁡ K ∧ X meet ⁡ K ⊥ ˙ ⁡ X = 0. ⁡ K
9 8 3anidm23 ⊢ K ∈ OP ∧ X ∈ B → ⊥ ˙ ⁡ X ∈ B ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X ∧ X ≤ K X → ⊥ ˙ ⁡ X ≤ K ⊥ ˙ ⁡ X ∧ X join ⁡ K ⊥ ˙ ⁡ X = 1. ⁡ K ∧ X meet ⁡ K ⊥ ˙ ⁡ X = 0. ⁡ K
10 9 simp1d ⊢ K ∈ OP ∧ X ∈ B → ⊥ ˙ ⁡ X ∈ B ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X ∧ X ≤ K X → ⊥ ˙ ⁡ X ≤ K ⊥ ˙ ⁡ X
11 10 simp1d ⊢ K ∈ OP ∧ X ∈ B → ⊥ ˙ ⁡ X ∈ B