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 ( ( 𝐴C𝐵C𝐴𝐵 ) → 𝐴 𝐶 𝐵 )

Proof

Step Hyp Ref Expression
1 sseq1 ( 𝐴 = if ( 𝐴C , 𝐴 , 0 ) → ( 𝐴𝐵 ↔ if ( 𝐴C , 𝐴 , 0 ) ⊆ 𝐵 ) )
2 breq1 ( 𝐴 = if ( 𝐴C , 𝐴 , 0 ) → ( 𝐴 𝐶 𝐵 ↔ if ( 𝐴C , 𝐴 , 0 ) 𝐶 𝐵 ) )
3 1 2 imbi12d ( 𝐴 = if ( 𝐴C , 𝐴 , 0 ) → ( ( 𝐴𝐵𝐴 𝐶 𝐵 ) ↔ ( if ( 𝐴C , 𝐴 , 0 ) ⊆ 𝐵 → if ( 𝐴C , 𝐴 , 0 ) 𝐶 𝐵 ) ) )
4 sseq2 ( 𝐵 = if ( 𝐵C , 𝐵 , 0 ) → ( if ( 𝐴C , 𝐴 , 0 ) ⊆ 𝐵 ↔ if ( 𝐴C , 𝐴 , 0 ) ⊆ if ( 𝐵C , 𝐵 , 0 ) ) )
5 breq2 ( 𝐵 = if ( 𝐵C , 𝐵 , 0 ) → ( if ( 𝐴C , 𝐴 , 0 ) 𝐶 𝐵 ↔ if ( 𝐴C , 𝐴 , 0 ) 𝐶 if ( 𝐵C , 𝐵 , 0 ) ) )
6 4 5 imbi12d ( 𝐵 = if ( 𝐵C , 𝐵 , 0 ) → ( ( if ( 𝐴C , 𝐴 , 0 ) ⊆ 𝐵 → if ( 𝐴C , 𝐴 , 0 ) 𝐶 𝐵 ) ↔ ( if ( 𝐴C , 𝐴 , 0 ) ⊆ if ( 𝐵C , 𝐵 , 0 ) → if ( 𝐴C , 𝐴 , 0 ) 𝐶 if ( 𝐵C , 𝐵 , 0 ) ) ) )
7 h0elch 0C
8 7 elimel if ( 𝐴C , 𝐴 , 0 ) ∈ C
9 7 elimel if ( 𝐵C , 𝐵 , 0 ) ∈ C
10 8 9 lecmi ( if ( 𝐴C , 𝐴 , 0 ) ⊆ if ( 𝐵C , 𝐵 , 0 ) → if ( 𝐴C , 𝐴 , 0 ) 𝐶 if ( 𝐵C , 𝐵 , 0 ) )
11 3 6 10 dedth2h ( ( 𝐴C𝐵C ) → ( 𝐴𝐵𝐴 𝐶 𝐵 ) )
12 11 3impia ( ( 𝐴C𝐵C𝐴𝐵 ) → 𝐴 𝐶 𝐵 )