Metamath Proof Explorer

Theorem pjclem4a

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

Ref Expression
Hypotheses pjclem1.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjclem1.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion 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}$

Proof

Step Hyp Ref Expression
1 pjclem1.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
2 pjclem1.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 elin ${⊢}{A}\in \left({G}\cap {H}\right)↔\left({A}\in {G}\wedge {A}\in {H}\right)$
4 2 cheli ${⊢}{A}\in {H}\to {A}\in ℋ$
5 4 adantl ${⊢}\left({A}\in {G}\wedge {A}\in {H}\right)\to {A}\in ℋ$
6 1 2 pjcoi ${⊢}{A}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)$
7 5 6 syl ${⊢}\left({A}\in {G}\wedge {A}\in {H}\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)$
8 pjid ${⊢}\left({H}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {H}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}$
9 2 8 mpan ${⊢}{A}\in {H}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}$
10 eleq1 ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}↔{A}\in {G}\right)$
11 pjid ${⊢}\left({G}\in {\mathbf{C}}_{ℋ}\wedge {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)$
12 1 11 mpan ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in {G}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)$
13 10 12 syl6bir ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}\to \left({A}\in {G}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)$
14 eqeq2 ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)↔{\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={A}\right)$
15 13 14 sylibd ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={A}\to \left({A}\in {G}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={A}\right)$
16 9 15 syl ${⊢}{A}\in {H}\to \left({A}\in {G}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={A}\right)$
17 16 impcom ${⊢}\left({A}\in {G}\wedge {A}\in {H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)={A}$
18 7 17 eqtrd ${⊢}\left({A}\in {G}\wedge {A}\in {H}\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={A}$
19 3 18 sylbi ${⊢}{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}$