This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )