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