Theorem pjin3i

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

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

Proof

Step	Hyp	Ref	Expression
1		pjin3.1	⊢ 𝐹 ∈ Cℋ
2		pjin3.2	⊢ 𝐺 ∈ Cℋ
3		pjin3.3	⊢ 𝐻 ∈ Cℋ
4		ssin	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐹 ⊆ 𝐻 ) ↔ 𝐹 ⊆ ( 𝐺 ∩ 𝐻 ) )
5	1 2	pjss2coi	⊢ ( 𝐹 ⊆ 𝐺 ↔ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐹 ) )
6		eqcom	⊢ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) = ( projℎ ‘ 𝐹 ) ↔ ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) )
7	5 6	bitri	⊢ ( 𝐹 ⊆ 𝐺 ↔ ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) )
8	1 3	pjss2coi	⊢ ( 𝐹 ⊆ 𝐻 ↔ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐹 ) )
9		eqcom	⊢ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) = ( projℎ ‘ 𝐹 ) ↔ ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) )
10	8 9	bitri	⊢ ( 𝐹 ⊆ 𝐻 ↔ ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) )
11	7 10	anbi12i	⊢ ( ( 𝐹 ⊆ 𝐺 ∧ 𝐹 ⊆ 𝐻 ) ↔ ( ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) ) )
12	2 3	chincli	⊢ ( 𝐺 ∩ 𝐻 ) ∈ Cℋ
13	1 12	pjss2coi	⊢ ( 𝐹 ⊆ ( 𝐺 ∩ 𝐻 ) ↔ ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ) = ( projℎ ‘ 𝐹 ) )
14		eqcom	⊢ ( ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ) = ( projℎ ‘ 𝐹 ) ↔ ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ) )
15	13 14	bitri	⊢ ( 𝐹 ⊆ ( 𝐺 ∩ 𝐻 ) ↔ ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ) )
16	4 11 15	3bitr3i	⊢ ( ( ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐺 ) ) ∧ ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ 𝐻 ) ) ) ↔ ( projℎ ‘ 𝐹 ) = ( ( projℎ ‘ 𝐹 ) ∘ ( projℎ ‘ ( 𝐺 ∩ 𝐻 ) ) ) )