Metamath Proof Explorer


Theorem cmcm2i

Description: Commutation with orthocomplement. Theorem 2.3(i) of Beran p. 39. (Contributed by NM, 4-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1
|- A e. CH
pjoml2.2
|- B e. CH
Assertion cmcm2i
|- ( A C_H B <-> A C_H ( _|_ ` B ) )

Proof

Step Hyp Ref Expression
1 pjoml2.1
 |-  A e. CH
2 pjoml2.2
 |-  B e. CH
3 1 2 chincli
 |-  ( A i^i B ) e. CH
4 2 choccli
 |-  ( _|_ ` B ) e. CH
5 1 4 chincli
 |-  ( A i^i ( _|_ ` B ) ) e. CH
6 3 5 chjcomi
 |-  ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i ( _|_ ` B ) ) vH ( A i^i B ) )
7 2 pjococi
 |-  ( _|_ ` ( _|_ ` B ) ) = B
8 7 ineq2i
 |-  ( A i^i ( _|_ ` ( _|_ ` B ) ) ) = ( A i^i B )
9 8 oveq2i
 |-  ( ( A i^i ( _|_ ` B ) ) vH ( A i^i ( _|_ ` ( _|_ ` B ) ) ) ) = ( ( A i^i ( _|_ ` B ) ) vH ( A i^i B ) )
10 6 9 eqtr4i
 |-  ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i ( _|_ ` B ) ) vH ( A i^i ( _|_ ` ( _|_ ` B ) ) ) )
11 10 eqeq2i
 |-  ( A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) <-> A = ( ( A i^i ( _|_ ` B ) ) vH ( A i^i ( _|_ ` ( _|_ ` B ) ) ) ) )
12 1 2 cmbri
 |-  ( A C_H B <-> A = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) )
13 1 4 cmbri
 |-  ( A C_H ( _|_ ` B ) <-> A = ( ( A i^i ( _|_ ` B ) ) vH ( A i^i ( _|_ ` ( _|_ ` B ) ) ) ) )
14 11 12 13 3bitr4i
 |-  ( A C_H B <-> A C_H ( _|_ ` B ) )