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

Proof

Step Hyp Ref Expression
1 breq1 ( 𝐴 = if ( 𝐴C , 𝐴 , 0 ) → ( 𝐴 𝐶 𝐵 ↔ if ( 𝐴C , 𝐴 , 0 ) 𝐶 𝐵 ) )
2 fveq2 ( 𝐴 = if ( 𝐴C , 𝐴 , 0 ) → ( ⊥ ‘ 𝐴 ) = ( ⊥ ‘ if ( 𝐴C , 𝐴 , 0 ) ) )
3 2 breq1d ( 𝐴 = if ( 𝐴C , 𝐴 , 0 ) → ( ( ⊥ ‘ 𝐴 ) 𝐶 𝐵 ↔ ( ⊥ ‘ if ( 𝐴C , 𝐴 , 0 ) ) 𝐶 𝐵 ) )
4 1 3 bibi12d ( 𝐴 = if ( 𝐴C , 𝐴 , 0 ) → ( ( 𝐴 𝐶 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝐶 𝐵 ) ↔ ( if ( 𝐴C , 𝐴 , 0 ) 𝐶 𝐵 ↔ ( ⊥ ‘ if ( 𝐴C , 𝐴 , 0 ) ) 𝐶 𝐵 ) ) )
5 breq2 ( 𝐵 = if ( 𝐵C , 𝐵 , 0 ) → ( if ( 𝐴C , 𝐴 , 0 ) 𝐶 𝐵 ↔ if ( 𝐴C , 𝐴 , 0 ) 𝐶 if ( 𝐵C , 𝐵 , 0 ) ) )
6 breq2 ( 𝐵 = if ( 𝐵C , 𝐵 , 0 ) → ( ( ⊥ ‘ if ( 𝐴C , 𝐴 , 0 ) ) 𝐶 𝐵 ↔ ( ⊥ ‘ if ( 𝐴C , 𝐴 , 0 ) ) 𝐶 if ( 𝐵C , 𝐵 , 0 ) ) )
7 5 6 bibi12d ( 𝐵 = if ( 𝐵C , 𝐵 , 0 ) → ( ( if ( 𝐴C , 𝐴 , 0 ) 𝐶 𝐵 ↔ ( ⊥ ‘ if ( 𝐴C , 𝐴 , 0 ) ) 𝐶 𝐵 ) ↔ ( if ( 𝐴C , 𝐴 , 0 ) 𝐶 if ( 𝐵C , 𝐵 , 0 ) ↔ ( ⊥ ‘ if ( 𝐴C , 𝐴 , 0 ) ) 𝐶 if ( 𝐵C , 𝐵 , 0 ) ) ) )
8 h0elch 0C
9 8 elimel if ( 𝐴C , 𝐴 , 0 ) ∈ C
10 8 elimel if ( 𝐵C , 𝐵 , 0 ) ∈ C
11 9 10 cmcm3i ( if ( 𝐴C , 𝐴 , 0 ) 𝐶 if ( 𝐵C , 𝐵 , 0 ) ↔ ( ⊥ ‘ if ( 𝐴C , 𝐴 , 0 ) ) 𝐶 if ( 𝐵C , 𝐵 , 0 ) )
12 4 7 11 dedth2h ( ( 𝐴C𝐵C ) → ( 𝐴 𝐶 𝐵 ↔ ( ⊥ ‘ 𝐴 ) 𝐶 𝐵 ) )