Theorem pjclem2

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

	Ref	Expression
Hypotheses	pjclem1.1	⊢ 𝐺 ∈ Cℋ
	pjclem1.2	⊢ 𝐻 ∈ Cℋ
Assertion	pjclem2	⊢ ( 𝐺 𝐶ℋ 𝐻 → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjclem1.1	⊢ 𝐺 ∈ Cℋ
2		pjclem1.2	⊢ 𝐻 ∈ Cℋ
3		incom	⊢ ( 𝐺 ∩ 𝐻 ) = ( 𝐻 ∩ 𝐺 )
4	3	fveq2i	⊢ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) = ( projℎ ‘ ( 𝐻 ∩ 𝐺 ) )
5	1 2	pjclem1	⊢ ( 𝐺 𝐶ℋ 𝐻 → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) )
6	1 2	cmcmi	⊢ ( 𝐺 𝐶ℋ 𝐻 ↔ 𝐻 𝐶ℋ 𝐺 )
7	2 1	pjclem1	⊢ ( 𝐻 𝐶ℋ 𝐺 → ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ 𝐺 ) ) )
8	6 7	sylbi	⊢ ( 𝐺 𝐶ℋ 𝐻 → ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ ( 𝐻 ∩ 𝐺 ) ) )
9	4 5 8	3eqtr4a	⊢ ( 𝐺 𝐶ℋ 𝐻 → ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) )