Metamath Proof Explorer

Theorem cmbr

Description: Binary relation expressing A commutes with B . Definition of commutes in Kalmbach p. 20. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cmbr 
|- ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( x = A -> ( x e. CH <-> A e. CH ) )
2 1 anbi1d 
 |-  ( x = A -> ( ( x e. CH /\ y e. CH ) <-> ( A e. CH /\ y e. CH ) ) )
3 id 
 |-  ( x = A -> x = A )
4 ineq1 
 |-  ( x = A -> ( x i^i y ) = ( A i^i y ) )
5 ineq1 
 |-  ( x = A -> ( x i^i ( _|_ ` y ) ) = ( A i^i ( _|_ ` y ) ) )
6 4 5 oveq12d 
 |-  ( x = A -> ( ( x i^i y ) vH ( x i^i ( _|_ ` y ) ) ) = ( ( A i^i y ) vH ( A i^i ( _|_ ` y ) ) ) )
7 3 6 eqeq12d 
 |-  ( x = A -> ( x = ( ( x i^i y ) vH ( x i^i ( _|_ ` y ) ) ) <-> A = ( ( A i^i y ) vH ( A i^i ( _|_ ` y ) ) ) ) )
8 2 7 anbi12d 
 |-  ( x = A -> ( ( ( x e. CH /\ y e. CH ) /\ x = ( ( x i^i y ) vH ( x i^i ( _|_ ` y ) ) ) ) <-> ( ( A e. CH /\ y e. CH ) /\ A = ( ( A i^i y ) vH ( A i^i ( _|_ ` y ) ) ) ) ) )
9 eleq1 
 |-  ( y = B -> ( y e. CH <-> B e. CH ) )
10 9 anbi2d 
 |-  ( y = B -> ( ( A e. CH /\ y e. CH ) <-> ( A e. CH /\ B e. CH ) ) )
11 ineq2 
 |-  ( y = B -> ( A i^i y ) = ( A i^i B ) )
12 fveq2 
 |-  ( y = B -> ( _|_ ` y ) = ( _|_ ` B ) )
13 12 ineq2d 
 |-  ( y = B -> ( A i^i ( _|_ ` y ) ) = ( A i^i ( _|_ ` B ) ) )
14 11 13 oveq12d 
 |-  ( y = B -> ( ( A i^i y ) vH ( A i^i ( _|_ ` y ) ) ) = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) )
15 14 eqeq2d 
 |-  ( y = B -> ( A = ( ( A i^i y ) vH ( A i^i ( _|_ ` y ) ) ) <-> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) ) )
16 10 15 anbi12d 
 |-  ( y = B -> ( ( ( A e. CH /\ y e. CH ) /\ A = ( ( A i^i y ) vH ( A i^i ( _|_ ` y ) ) ) ) <-> ( ( A e. CH /\ B e. CH ) /\ A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) ) ) )
17 df-cm 
 |-  C_H = { <. x , y >. | ( ( x e. CH /\ y e. CH ) /\ x = ( ( x i^i y ) vH ( x i^i ( _|_ ` y ) ) ) ) }
18 8 16 17 brabg 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> ( ( A e. CH /\ B e. CH ) /\ A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) ) ) )
19 18 bianabs 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_H B <-> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) ) )