# Metamath Proof Explorer

## 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}}_{ℋ}$
pjin3.2 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjin3.3 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
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)↔{\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}}_{ℋ}$
2 pjin3.2 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
3 pjin3.3 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
4 ssin ${⊢}\left({F}\subseteq {G}\wedge {F}\subseteq {H}\right)↔{F}\subseteq {G}\cap {H}$
5 1 2 pjss2coi ${⊢}{F}\subseteq {G}↔{\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)↔{\mathrm{proj}}_{ℎ}\left({F}\right)={\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)$
7 5 6 bitri ${⊢}{F}\subseteq {G}↔{\mathrm{proj}}_{ℎ}\left({F}\right)={\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)$
8 1 3 pjss2coi ${⊢}{F}\subseteq {H}↔{\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)↔{\mathrm{proj}}_{ℎ}\left({F}\right)={\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)$
10 8 9 bitri ${⊢}{F}\subseteq {H}↔{\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)↔\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}}_{ℋ}$
13 1 12 pjss2coi ${⊢}{F}\subseteq {G}\cap {H}↔{\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)↔{\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}↔{\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)↔{\mathrm{proj}}_{ℎ}\left({F}\right)={\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)$