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

Metamath Proof Explorer

Theorem lecm

Description: Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of Beran p. 40. (Contributed by NM, 13-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion lecm ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → A 𝐶 ℋ B

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A ⊆ B ↔ if A ∈ C ℋ A 0 ℋ ⊆ B
2 breq1 ⊢ A = if A ∈ C ℋ A 0 ℋ → A 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B
3 1 2 imbi12d ⊢ A = if A ∈ C ℋ A 0 ℋ → A ⊆ B → A 𝐶 ℋ B ↔ if A ∈ C ℋ A 0 ℋ ⊆ B → if A ∈ C ℋ A 0 ℋ 𝐶 ℋ B
4 sseq2 ⊢ B = if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ ⊆ B ↔ if A ∈ C ℋ A 0 ℋ ⊆ if B ∈ C ℋ B 0 ℋ
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 4 5 imbi12d ⊢ 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 ℋ
7 h0elch ⊢ 0 ℋ ∈ C ℋ
8 7 elimel ⊢ if A ∈ C ℋ A 0 ℋ ∈ C ℋ
9 7 elimel ⊢ if B ∈ C ℋ B 0 ℋ ∈ C ℋ
10 8 9 lecmi ⊢ if A ∈ C ℋ A 0 ℋ ⊆ if B ∈ C ℋ B 0 ℋ → if A ∈ C ℋ A 0 ℋ 𝐶 ℋ if B ∈ C ℋ B 0 ℋ
11 3 6 10 dedth2h ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⊆ B → A 𝐶 ℋ B
12 11 3impia ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → A 𝐶 ℋ B