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	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
	pjin3.2	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjin3.3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjin3i	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjin3.1	$$⊢F\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjin3.2	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
3		pjin3.3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
4		ssin	$$⊢\left(F\subseteq G\wedge F\subseteq H\right)\leftrightarrow F\subseteq G\cap H$$
5	1 2	pjss2coi	$$⊢F\subseteq G\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(F\right)$$
6		eqcom	$$⊢{\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(F\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
7	5 6	bitri	$$⊢F\subseteq G\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
8	1 3	pjss2coi	$$⊢F\subseteq H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(F\right)$$
9		eqcom	$$⊢{\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(F\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)$$
10	8 9	bitri	$$⊢F\subseteq H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)$$
11	7 10	anbi12i	$$⊢\left(F\subseteq G\wedge F\subseteq H\right)\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
12	2 3	chincli	$$⊢G\cap H\in {\mathbf{C}}_{\mathscr{H}}$$
13	1 12	pjss2coi	$$⊢F\subseteq G\cap H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\cap H\right)={\mathrm{proj}}_{ℎ}\left(F\right)$$
14		eqcom	$$⊢{\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\cap H\right)={\mathrm{proj}}_{ℎ}\left(F\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$
15	13 14	bitri	$$⊢F\subseteq G\cap H\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$
16	4 11 15	3bitr3i	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\wedge {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(F\right)={\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$