Theorem pj3i

Description: Projection triplet theorem. (Contributed by NM, 2-Dec-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjadj2co.1	⊢ 𝐹 ∈ Cℋ
	pjadj2co.2	⊢ 𝐺 ∈ Cℋ
	pjadj2co.3	⊢ 𝐻 ∈ Cℋ
Assertion	pj3i	⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjadj2co.1	⊢ 𝐹 ∈ Cℋ
2		pjadj2co.2	⊢ 𝐺 ∈ Cℋ
3		pjadj2co.3	⊢ 𝐻 ∈ Cℋ
4		coass	⊢ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) )
5		eqeq1	⊢ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) → ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) ) ↔ ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) ) ) )
6	4 5	mpbiri	⊢ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) → ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) ) )
7	6	rneqd	⊢ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) → ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ran ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) ) )
8		rncoss	⊢ ran ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) ) ⊆ ran ( projℎ ‘ 𝐺 )
9	2	pjrni	⊢ ran ( projℎ ‘ 𝐺 ) = 𝐺
10	8 9	sseqtri	⊢ ran ( ( projℎ ‘ 𝐺 ) ∘ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) ) ⊆ 𝐺
11	7 10	eqsstrdi	⊢ ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) → ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 )
12	1 2 3	pj3si	⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ran ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ⊆ 𝐺 ) → ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) )
13	11 12	sylan2	⊢ ( ( ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐻 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐹 ) ) ∧ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( ( ( projℎ ‘ 𝐺 ) ∘ ( projℎ ‘ 𝐹 ) ) ∘ ( projℎ ‘ 𝐻 ) ) ) → ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ ( ( 𝐹 ∩ 𝐺 ) ∩ 𝐻 ) ) )