Metamath Proof Explorer

Theorem leopsq

Description: The square of a Hermitian operator is positive. (Contributed by NM, 23-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion leopsq ⊢T∈HrmOp→0hop≤opT∘T

Proof

Step Hyp Ref Expression
1 hmopf ⊢T∈HrmOp→T:ℋ⟶ℋ
2 1 ffvelcdmda ⊢T∈HrmOp∧x∈ℋ→T⁡x∈ℋ
3 hiidge0 ⊢T⁡x∈ℋ→0≤T⁡x⋅ihT⁡x
4 2 3 syl ⊢T∈HrmOp∧x∈ℋ→0≤T⁡x⋅ihT⁡x
5 simpl ⊢T∈HrmOp∧x∈ℋ→T∈HrmOp
6 simpr ⊢T∈HrmOp∧x∈ℋ→x∈ℋ
7 hmop ⊢T∈HrmOp∧T⁡x∈ℋ∧x∈ℋ→T⁡x⋅ihT⁡x=T⁡T⁡x⋅ihx
8 5 2 6 7 syl3anc ⊢T∈HrmOp∧x∈ℋ→T⁡x⋅ihT⁡x=T⁡T⁡x⋅ihx
9 fvco3 ⊢T:ℋ⟶ℋ∧x∈ℋ→T∘T⁡x=T⁡T⁡x
10 1 9 sylan ⊢T∈HrmOp∧x∈ℋ→T∘T⁡x=T⁡T⁡x
11 10 oveq1d ⊢T∈HrmOp∧x∈ℋ→T∘T⁡x⋅ihx=T⁡T⁡x⋅ihx
12 8 11 eqtr4d ⊢T∈HrmOp∧x∈ℋ→T⁡x⋅ihT⁡x=T∘T⁡x⋅ihx
13 4 12 breqtrd ⊢T∈HrmOp∧x∈ℋ→0≤T∘T⁡x⋅ihx
14 13 ralrimiva ⊢T∈HrmOp→∀x∈ℋ0≤T∘T⁡x⋅ihx
15 eqid ⊢T∘T=T∘T
16 hmopco ⊢T∈HrmOp∧T∈HrmOp∧T∘T=T∘T→T∘T∈HrmOp
17 15 16 mp3an3 ⊢T∈HrmOp∧T∈HrmOp→T∘T∈HrmOp
18 17 anidms ⊢T∈HrmOp→T∘T∈HrmOp
19 leoppos ⊢T∘T∈HrmOp→0hop≤opT∘T↔∀x∈ℋ0≤T∘T⁡x⋅ihx
20 18 19 syl ⊢T∈HrmOp→0hop≤opT∘T↔∀x∈ℋ0≤T∘T⁡x⋅ihx
21 14 20 mpbird ⊢T∈HrmOp→0hop≤opT∘T