Theorem pjclem2

Description: Lemma for projection commutation theorem. (Contributed by NM, 17-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjclem1.1	|- G e. CH
	pjclem1.2	|- H e. CH
Assertion	pjclem2	|- ( G C_H H -> ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjclem1.1	|- G e. CH
2		pjclem1.2	|- H e. CH
3		incom	|- ( G i^i H ) = ( H i^i G )
4	3	fveq2i	|- ( projh ` ( G i^i H ) ) = ( projh ` ( H i^i G ) )
5	1 2	pjclem1	|- ( G C_H H -> ( ( projh ` G ) o. ( projh ` H ) ) = ( projh ` ( G i^i H ) ) )
6	1 2	cmcmi	|- ( G C_H H <-> H C_H G )
7	2 1	pjclem1	|- ( H C_H G -> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` ( H i^i G ) ) )
8	6 7	sylbi	|- ( G C_H H -> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` ( H i^i G ) ) )
9	4 5 8	3eqtr4a	|- ( G C_H H -> ( ( projh ` G ) o. ( projh ` H ) ) = ( ( projh ` H ) o. ( projh ` G ) ) )