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 GC
pjclem1.2 HC
Assertion pjcmul2i projGprojH=projHprojGprojGprojH=projGH

Proof

Step Hyp Ref Expression
1 pjclem1.1 GC
2 pjclem1.2 HC
3 1 2 pjclem4 projGprojH=projHprojGprojGprojH=projGH
4 pjmfn projFnC
5 1 2 chincli GHC
6 fnfvelrn projFnCGHCprojGHranproj
7 4 5 6 mp2an projGHranproj
8 eleq1 projGprojH=projGHprojGprojHranprojprojGHranproj
9 7 8 mpbiri projGprojH=projGHprojGprojHranproj
10 1 2 pjcmul1i projGprojH=projHprojGprojGprojHranproj
11 9 10 sylibr projGprojH=projGHprojGprojH=projHprojG
12 3 11 impbii projGprojH=projHprojGprojGprojH=projGH