Metamath Proof Explorer

Theorem dmdsym

Description: Dual M-symmetry of the Hilbert lattice. (Contributed by NM, 25-Jul-2007) (New usage is discouraged.)

Ref Expression
Assertion dmdsym ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝑀 ℋ * B ↔ B 𝑀 ℋ * A

Proof

Step Hyp Ref Expression
1 choccl ⊢ A ∈ C ℋ → ⊥ ⁡ A ∈ C ℋ
2 choccl ⊢ B ∈ C ℋ → ⊥ ⁡ B ∈ C ℋ
3 mdsym ⊢ ⊥ ⁡ A ∈ C ℋ ∧ ⊥ ⁡ B ∈ C ℋ → ⊥ ⁡ A 𝑀 ℋ ⊥ ⁡ B ↔ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ A
4 1 2 3 syl2an ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ A 𝑀 ℋ ⊥ ⁡ B ↔ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ A
5 dmdmd ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝑀 ℋ * B ↔ ⊥ ⁡ A 𝑀 ℋ ⊥ ⁡ B
6 dmdmd ⊢ B ∈ C ℋ ∧ A ∈ C ℋ → B 𝑀 ℋ * A ↔ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ A
7 6 ancoms ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → B 𝑀 ℋ * A ↔ ⊥ ⁡ B 𝑀 ℋ ⊥ ⁡ A
8 4 5 7 3bitr4d ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝑀 ℋ * B ↔ B 𝑀 ℋ * A