Theorem pjin1i

Description: Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjin1.1	|- G e. CH
	pjin1.2	|- H e. CH
Assertion	pjin1i	|- ( projh ` ( G i^i H ) ) = ( ( projh ` G ) o. ( projh ` ( G i^i H ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjin1.1	|- G e. CH
2		pjin1.2	|- H e. CH
3		inss1	|- ( G i^i H ) C_ G
4	1 2	chincli	|- ( G i^i H ) e. CH
5	4 1	pjss1coi	|- ( ( G i^i H ) C_ G <-> ( ( projh ` G ) o. ( projh ` ( G i^i H ) ) ) = ( projh ` ( G i^i H ) ) )
6	3 5	mpbi	|- ( ( projh ` G ) o. ( projh ` ( G i^i H ) ) ) = ( projh ` ( G i^i H ) )
7	6	eqcomi	|- ( projh ` ( G i^i H ) ) = ( ( projh ` G ) o. ( projh ` ( G i^i H ) ) )