This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cmcm3

Description: Commutation with orthocomplement. Remark in Kalmbach p. 23. (Contributed by NM, 13-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion cmcm3 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝐶 ℋ B ↔ ⊥ ⁡ A 𝐶 ℋ B

Proof

Step Hyp Ref Expression
1 breq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B
2 fveq2 ⊢ A = if A ∈ C ℋ A 0 ℋ → ⊥ ⁡ A = ⊥ ⁡ if A ∈ C ℋ A 0 ℋ
3 2 breq1d ⊢ A = if A ∈ C ℋ A 0 ℋ → ⊥ ⁡ A 𝐶 ℋ B ↔ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B
4 1 3 bibi12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A 𝐶 ℋ B ↔ ⊥ ⁡ A 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B
5 breq2 ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ
6 breq2 ⊢ B = if B ∈ C ℋ B 0 ℋ → ⊥ ⁡ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ
7 5 6 bibi12d ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ ↔ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ
8 h0elch ⊢ 0 ℋ ∈ C ℋ
9 8 elimel ⊢ if A ∈ C ℋ A 0 ℋ ∈ C ℋ
10 8 elimel ⊢ if B ∈ C ℋ B 0 ℋ ∈ C ℋ
11 9 10 cmcm3i ⊢ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ ↔ ⊥ ⁡ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ
12 4 7 11 dedth2h ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝐶 ℋ B ↔ ⊥ ⁡ A 𝐶 ℋ B