Metamath Proof Explorer

Theorem cmbr2i

Description: Alternate definition of the commutes relation. Remark in Kalmbach p. 23. (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 
|- A e. CH
pjoml2.2 
|- B e. CH
Assertion cmbr2i 
|- ( A C_H B <-> A = ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 pjoml2.1 
 |-  A e. CH
2 pjoml2.2 
 |-  B e. CH
3 1 2 cmcm4i 
 |-  ( A C_H B <-> ( _|_ ` A ) C_H ( _|_ ` B ) )
4 1 choccli 
 |-  ( _|_ ` A ) e. CH
5 2 choccli 
 |-  ( _|_ ` B ) e. CH
6 4 5 cmbri 
 |-  ( ( _|_ ` A ) C_H ( _|_ ` B ) <-> ( _|_ ` A ) = ( ( ( _|_ ` A ) i^i ( _|_ ` B ) ) vH ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` B ) ) ) ) )
7 eqcom 
 |-  ( A = ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) <-> ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) = A )
8 1 2 chjcli 
 |-  ( A vH B ) e. CH
9 1 5 chjcli 
 |-  ( A vH ( _|_ ` B ) ) e. CH
10 8 9 chincli 
 |-  ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) e. CH
11 10 1 chcon3i 
 |-  ( ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) = A <-> ( _|_ ` A ) = ( _|_ ` ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) ) )
12 8 9 chdmm1i 
 |-  ( _|_ ` ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) ) = ( ( _|_ ` ( A vH B ) ) vH ( _|_ ` ( A vH ( _|_ ` B ) ) ) )
13 1 2 chdmj1i 
 |-  ( _|_ ` ( A vH B ) ) = ( ( _|_ ` A ) i^i ( _|_ ` B ) )
14 1 5 chdmj1i 
 |-  ( _|_ ` ( A vH ( _|_ ` B ) ) ) = ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` B ) ) )
15 13 14 oveq12i 
 |-  ( ( _|_ ` ( A vH B ) ) vH ( _|_ ` ( A vH ( _|_ ` B ) ) ) ) = ( ( ( _|_ ` A ) i^i ( _|_ ` B ) ) vH ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` B ) ) ) )
16 12 15 eqtri 
 |-  ( _|_ ` ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) ) = ( ( ( _|_ ` A ) i^i ( _|_ ` B ) ) vH ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` B ) ) ) )
17 16 eqeq2i 
 |-  ( ( _|_ ` A ) = ( _|_ ` ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) ) <-> ( _|_ ` A ) = ( ( ( _|_ ` A ) i^i ( _|_ ` B ) ) vH ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` B ) ) ) ) )
18 7 11 17 3bitrri 
 |-  ( ( _|_ ` A ) = ( ( ( _|_ ` A ) i^i ( _|_ ` B ) ) vH ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` B ) ) ) ) <-> A = ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) )
19 3 6 18 3bitri 
 |-  ( A C_H B <-> A = ( ( A vH B ) i^i ( A vH ( _|_ ` B ) ) ) )