Theorem pjcmul2i

Description: The projection subspace of the difference between two projectors. Part 2 of Theorem 1 of AkhiezerGlazman p. 65. (Contributed by NM, 3-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjclem1.1	|- G e. CH
	pjclem1.2	|- H e. CH
Assertion	pjcmul2i	|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) <-> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjclem1.1	|- G e. CH
2		pjclem1.2	|- H e. CH
3	1 2	pjclem4	|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) -> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) )
4		pjmfn	|- projh Fn CH
5	1 2	chincli	|- ( G i^i H ) e. CH
6		fnfvelrn	|- ( ( projh Fn CH /\ ( G i^i H ) e. CH ) -> ( projh ` ( G i^i H ) ) e. ran projh )
7	4 5 6	mp2an	|- ( projh ` ( G i^i H ) ) e. ran projh
8		eleq1	|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) e. ran projh <-> ( projh ` ( G i^i H ) ) e. ran projh ) )
9	7 8	mpbiri	|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) -> ( ( projh ` G ) o. ( projh ` H ) ) e. ran projh )
10	1 2	pjcmul1i	|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) <-> ( ( projh ` G ) o. ( projh ` H ) ) e. ran projh )
11	9 10	sylibr	|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) -> ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) )
12	3 11	impbii	|- ( ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) <-> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) )