Metamath Proof Explorer

Theorem cmcm2i

Description: Commutation with orthocomplement. Theorem 2.3(i) of Beran p. 39. (Contributed by NM, 4-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 ⊢ A ∈ C ℋ
pjoml2.2 ⊢ B ∈ C ℋ
Assertion cmcm2i ⊢ A 𝐶 ℋ B ↔ A 𝐶 ℋ ⊥ ⁡ B

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ A ∈ C ℋ
2 pjoml2.2 ⊢ B ∈ C ℋ
3 1 2 chincli ⊢ A ∩ B ∈ C ℋ
4 2 choccli ⊢ ⊥ ⁡ B ∈ C ℋ
5 1 4 chincli ⊢ A ∩ ⊥ ⁡ B ∈ C ℋ
6 3 5 chjcomi ⊢ A ∩ B ∨ ℋ A ∩ ⊥ ⁡ B = A ∩ ⊥ ⁡ B ∨ ℋ A ∩ B
7 2 pjococi ⊢ ⊥ ⁡ ⊥ ⁡ B = B
8 7 ineq2i ⊢ A ∩ ⊥ ⁡ ⊥ ⁡ B = A ∩ B
9 8 oveq2i ⊢ A ∩ ⊥ ⁡ B ∨ ℋ A ∩ ⊥ ⁡ ⊥ ⁡ B = A ∩ ⊥ ⁡ B ∨ ℋ A ∩ B
10 6 9 eqtr4i ⊢ A ∩ B ∨ ℋ A ∩ ⊥ ⁡ B = A ∩ ⊥ ⁡ B ∨ ℋ A ∩ ⊥ ⁡ ⊥ ⁡ B
11 10 eqeq2i ⊢ A = A ∩ B ∨ ℋ A ∩ ⊥ ⁡ B ↔ A = A ∩ ⊥ ⁡ B ∨ ℋ A ∩ ⊥ ⁡ ⊥ ⁡ B
12 1 2 cmbri ⊢ A 𝐶 ℋ B ↔ A = A ∩ B ∨ ℋ A ∩ ⊥ ⁡ B
13 1 4 cmbri ⊢ A 𝐶 ℋ ⊥ ⁡ B ↔ A = A ∩ ⊥ ⁡ B ∨ ℋ A ∩ ⊥ ⁡ ⊥ ⁡ B
14 11 12 13 3bitr4i ⊢ A 𝐶 ℋ B ↔ A 𝐶 ℋ ⊥ ⁡ B