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 → 0 hop ≤ op T ∘ 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 ⋅ ih T ⁡ x
4 2 3 syl ⊢ T ∈ HrmOp ∧ x ∈ ℋ → 0 ≤ T ⁡ x ⋅ ih T ⁡ x
5 simpl ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ∈ HrmOp
6 simpr ⊢ T ∈ HrmOp ∧ x ∈ ℋ → x ∈ ℋ
7 hmop ⊢ T ∈ HrmOp ∧ T ⁡ x ∈ ℋ ∧ x ∈ ℋ → T ⁡ x ⋅ ih T ⁡ x = T ⁡ T ⁡ x ⋅ ih x
8 5 2 6 7 syl3anc ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ⁡ x ⋅ ih T ⁡ x = T ⁡ T ⁡ x ⋅ ih x
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 ⋅ ih x = T ⁡ T ⁡ x ⋅ ih x
12 8 11 eqtr4d ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ⁡ x ⋅ ih T ⁡ x = T ∘ T ⁡ x ⋅ ih x
13 4 12 breqtrd ⊢ T ∈ HrmOp ∧ x ∈ ℋ → 0 ≤ T ∘ T ⁡ x ⋅ ih x
14 13 ralrimiva ⊢ T ∈ HrmOp → ∀ x ∈ ℋ 0 ≤ T ∘ T ⁡ x ⋅ ih x
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 → 0 hop ≤ op T ∘ T ↔ ∀ x ∈ ℋ 0 ≤ T ∘ T ⁡ x ⋅ ih x
20 18 19 syl ⊢ T ∈ HrmOp → 0 hop ≤ op T ∘ T ↔ ∀ x ∈ ℋ 0 ≤ T ∘ T ⁡ x ⋅ ih x
21 14 20 mpbird ⊢ T ∈ HrmOp → 0 hop ≤ op T ∘ T