Metamath Proof Explorer

Theorem pjcmul2i

Description: The projection subspace of the difference between two projectors. Part 2 of Theorem 1 of AkhiezerGlazman p. 65. (Contributed by NM, 3-Jun-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjclem1.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
2 pjclem1.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 1 2 pjclem4 ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)$
4 pjmfn ${⊢}{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{ℋ}$
5 1 2 chincli ${⊢}{G}\cap {H}\in {\mathbf{C}}_{ℋ}$
6 fnfvelrn ${⊢}\left({\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{ℋ}\wedge {G}\cap {H}\in {\mathbf{C}}_{ℋ}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$
7 4 5 6 mp2an ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$
8 eleq1 ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}↔{\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\right)$
9 7 8 mpbiri ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$
10 1 2 pjcmul1i ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)↔{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$
11 9 10 sylibr ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)\to {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)$
12 3 11 impbii ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)↔{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)$