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

Theorem pjcmul1i 28444
 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 𝐺C
pjclem1.2 𝐻C
Assertion
Ref Expression
pjcmul1i (((proj𝐺) ∘ (proj𝐻)) = ((proj𝐻) ∘ (proj𝐺)) ↔ ((proj𝐺) ∘ (proj𝐻)) ∈ ran proj)

Proof of Theorem pjcmul1i
StepHypRef Expression
1 pjclem1.1 . . . 4 𝐺C
2 pjclem1.2 . . . 4 𝐻C
31, 2pjclem4 28442 . . 3 (((proj𝐺) ∘ (proj𝐻)) = ((proj𝐻) ∘ (proj𝐺)) → ((proj𝐺) ∘ (proj𝐻)) = (proj‘(𝐺𝐻)))
4 pjmfn 27958 . . . 4 proj Fn C
51, 2chincli 27703 . . . 4 (𝐺𝐻) ∈ C
6 fnfvelrn 6264 . . . 4 ((proj Fn C ∧ (𝐺𝐻) ∈ C ) → (proj‘(𝐺𝐻)) ∈ ran proj)
74, 5, 6mp2an 704 . . 3 (proj‘(𝐺𝐻)) ∈ ran proj
83, 7syl6eqel 2696 . 2 (((proj𝐺) ∘ (proj𝐻)) = ((proj𝐻) ∘ (proj𝐺)) → ((proj𝐺) ∘ (proj𝐻)) ∈ ran proj)
91pjbdlni 28392 . . . . 5 (proj𝐺) ∈ BndLinOp
102pjbdlni 28392 . . . . 5 (proj𝐻) ∈ BndLinOp
119, 10adjcoi 28343 . . . 4 (adj‘((proj𝐺) ∘ (proj𝐻))) = ((adj‘(proj𝐻)) ∘ (adj‘(proj𝐺)))
12 pjadj3 28431 . . . . . 6 (𝐻C → (adj‘(proj𝐻)) = (proj𝐻))
132, 12ax-mp 5 . . . . 5 (adj‘(proj𝐻)) = (proj𝐻)
14 pjadj3 28431 . . . . . 6 (𝐺C → (adj‘(proj𝐺)) = (proj𝐺))
151, 14ax-mp 5 . . . . 5 (adj‘(proj𝐺)) = (proj𝐺)
1613, 15coeq12i 5207 . . . 4 ((adj‘(proj𝐻)) ∘ (adj‘(proj𝐺))) = ((proj𝐻) ∘ (proj𝐺))
1711, 16eqtri 2632 . . 3 (adj‘((proj𝐺) ∘ (proj𝐻))) = ((proj𝐻) ∘ (proj𝐺))
18 pjadj2 28430 . . 3 (((proj𝐺) ∘ (proj𝐻)) ∈ ran proj → (adj‘((proj𝐺) ∘ (proj𝐻))) = ((proj𝐺) ∘ (proj𝐻)))
1917, 18syl5reqr 2659 . 2 (((proj𝐺) ∘ (proj𝐻)) ∈ ran proj → ((proj𝐺) ∘ (proj𝐻)) = ((proj𝐻) ∘ (proj𝐺)))
208, 19impbii 198 1 (((proj𝐺) ∘ (proj𝐻)) = ((proj𝐻) ∘ (proj𝐺)) ↔ ((proj𝐺) ∘ (proj𝐻)) ∈ ran proj)