# Metamath Proof Explorer

## Theorem pj3lem1

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

Ref Expression
Hypotheses pjadj2co.1 ${⊢}{F}\in {\mathbf{C}}_{ℋ}$
pjadj2co.2 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjadj2co.3 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pj3lem1 ${⊢}{A}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={A}$

### Proof

Step Hyp Ref Expression
1 pjadj2co.1 ${⊢}{F}\in {\mathbf{C}}_{ℋ}$
2 pjadj2co.2 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
3 pjadj2co.3 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
4 coass ${⊢}\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({F}\right)\circ \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)$
5 4 fveq1i ${⊢}\left(\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)=\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\right)\left({A}\right)$
6 elin ${⊢}{A}\in \left({F}\cap \left({G}\cap {H}\right)\right)↔\left({A}\in {F}\wedge {A}\in \left({G}\cap {H}\right)\right)$
7 1 cheli ${⊢}{A}\in {F}\to {A}\in ℋ$
8 7 adantr ${⊢}\left({A}\in {F}\wedge {A}\in \left({G}\cap {H}\right)\right)\to {A}\in ℋ$
9 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({F}\right):ℋ⟶ℋ$
10 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
11 3 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
12 10 11 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right):ℋ⟶ℋ$
13 9 12 hocoi ${⊢}{A}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({F}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)$
14 8 13 syl ${⊢}\left({A}\in {F}\wedge {A}\in \left({G}\cap {H}\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({F}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)$
15 2 3 pjclem4a ${⊢}{A}\in \left({G}\cap {H}\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={A}$
16 eleq1 ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={A}\to \left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\in {F}↔{A}\in {F}\right)$
17 pjid ${⊢}\left({F}\in {\mathbf{C}}_{ℋ}\wedge \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\in {F}\right)\to {\mathrm{proj}}_{ℎ}\left({F}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)$
18 1 17 mpan ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\in {F}\to {\mathrm{proj}}_{ℎ}\left({F}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)$
19 16 18 syl6bir ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={A}\to \left({A}\in {F}\to {\mathrm{proj}}_{ℎ}\left({F}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)$
20 eqeq2 ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={A}\to \left({\mathrm{proj}}_{ℎ}\left({F}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)↔{\mathrm{proj}}_{ℎ}\left({F}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)={A}\right)$
21 19 20 sylibd ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={A}\to \left({A}\in {F}\to {\mathrm{proj}}_{ℎ}\left({F}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)={A}\right)$
22 15 21 syl ${⊢}{A}\in \left({G}\cap {H}\right)\to \left({A}\in {F}\to {\mathrm{proj}}_{ℎ}\left({F}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)={A}\right)$
23 22 impcom ${⊢}\left({A}\in {F}\wedge {A}\in \left({G}\cap {H}\right)\right)\to {\mathrm{proj}}_{ℎ}\left({F}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\right)={A}$
24 14 23 eqtrd ${⊢}\left({A}\in {F}\wedge {A}\in \left({G}\cap {H}\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\right)\left({A}\right)={A}$
25 6 24 sylbi ${⊢}{A}\in \left({F}\cap \left({G}\cap {H}\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\right)\left({A}\right)={A}$
26 inass ${⊢}\left({F}\cap {G}\right)\cap {H}={F}\cap \left({G}\cap {H}\right)$
27 25 26 eleq2s ${⊢}{A}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\to \left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\right)\left({A}\right)={A}$
28 5 27 syl5eq ${⊢}{A}\in \left(\left({F}\cap {G}\right)\cap {H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={A}$