Theorem pjin1i

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

	Ref	Expression
Hypotheses	pjin1.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjin1.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjin1i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap H\right)={\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjin1.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjin1.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3		inss1	$$⊢G\cap H\subseteq G$$
4	1 2	chincli	$$⊢G\cap H\in {\mathbf{C}}_{\mathscr{H}}$$
5	4 1	pjss1coi	$$⊢G\cap H\subseteq G\leftrightarrow {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(G\cap H\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$
6	3 5	mpbi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(G\cap H\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$
7	6	eqcomi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap H\right)={\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$