Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  pjcmul1i Unicode version

Theorem pjcmul1i 23624
 Description: A necessary and sufficient condition for the product of two projectors to be a projector is that the projectors commute. Part 1 of Theorem 1 of [AkhiezerGlazman] p. 65. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
pjclem1.1
pjclem1.2
Assertion
Ref Expression
pjcmul1i

Proof of Theorem pjcmul1i
StepHypRef Expression
1 pjclem1.1 . . . 4
2 pjclem1.2 . . . 4
31, 2pjclem4 23622 . . 3
4 pjmfn 23137 . . . 4
51, 2chincli 22882 . . . 4
6 fnfvelrn 5820 . . . 4
74, 5, 6mp2an 654 . . 3
83, 7syl6eqel 2489 . 2
91pjbdlni 23572 . . . . 5
102pjbdlni 23572 . . . . 5
119, 10adjcoi 23523 . . . 4
12 pjadj3 23611 . . . . . 6
132, 12ax-mp 8 . . . . 5
14 pjadj3 23611 . . . . . 6
151, 14ax-mp 8 . . . . 5
1613, 15coeq12i 4990 . . . 4
1711, 16eqtri 2421 . . 3
18 pjadj2 23610 . . 3
1917, 18syl5reqr 2448 . 2
208, 19impbii 181 1