Metamath Proof Explorer


Theorem cmbri

Description: Binary relation expressing the commutes relation. Definition of commutes in Kalmbach p. 20. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 𝐴C
pjoml2.2 𝐵C
Assertion cmbri ( 𝐴 𝐶 𝐵𝐴 = ( ( 𝐴𝐵 ) ∨ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 pjoml2.1 𝐴C
2 pjoml2.2 𝐵C
3 cmbr ( ( 𝐴C𝐵C ) → ( 𝐴 𝐶 𝐵𝐴 = ( ( 𝐴𝐵 ) ∨ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
4 1 2 3 mp2an ( 𝐴 𝐶 𝐵𝐴 = ( ( 𝐴𝐵 ) ∨ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )