Theorem pjclem4a

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

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

Proof

Step	Hyp	Ref	Expression
1		pjclem1.1	|- G e. CH
2		pjclem1.2	|- H e. CH
3		elin	|- ( A e. ( G i^i H ) <-> ( A e. G /\ A e. H ) )
4	2	cheli	|- ( A e. H -> A e. ~H )
5	4	adantl	|- ( ( A e. G /\ A e. H ) -> A e. ~H )
6	1 2	pjcoi	|- ( A e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) )
7	5 6	syl	|- ( ( A e. G /\ A e. H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) )
8		pjid	|- ( ( H e. CH /\ A e. H ) -> ( ( projh ` H ) ` A ) = A )
9	2 8	mpan	|- ( A e. H -> ( ( projh ` H ) ` A ) = A )
10		eleq1	|- ( ( ( projh ` H ) ` A ) = A -> ( ( ( projh ` H ) ` A ) e. G <-> A e. G ) )
11		pjid	|- ( ( G e. CH /\ ( ( projh ` H ) ` A ) e. G ) -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = ( ( projh ` H ) ` A ) )
12	1 11	mpan	|- ( ( ( projh ` H ) ` A ) e. G -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = ( ( projh ` H ) ` A ) )
13	10 12	syl6bir	|- ( ( ( projh ` H ) ` A ) = A -> ( A e. G -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = ( ( projh ` H ) ` A ) ) )
14		eqeq2	|- ( ( ( projh ` H ) ` A ) = A -> ( ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = ( ( projh ` H ) ` A ) <-> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = A ) )
15	13 14	sylibd	|- ( ( ( projh ` H ) ` A ) = A -> ( A e. G -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = A ) )
16	9 15	syl	|- ( A e. H -> ( A e. G -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = A ) )
17	16	impcom	|- ( ( A e. G /\ A e. H ) -> ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) = A )
18	7 17	eqtrd	|- ( ( A e. G /\ A e. H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = A )
19	3 18	sylbi	|- ( A e. ( G i^i H ) -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = A )