Description: Mapping of difference of Hilbert space operators. (Contributed by NM, 14-Nov-2000) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hoeq.1 | ⊢ 𝑆 : ℋ ⟶ ℋ | |
| hoeq.2 | ⊢ 𝑇 : ℋ ⟶ ℋ | ||
| Assertion | hosubcli | ⊢ ( 𝑆 −op 𝑇 ) : ℋ ⟶ ℋ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hoeq.1 | ⊢ 𝑆 : ℋ ⟶ ℋ | |
| 2 | hoeq.2 | ⊢ 𝑇 : ℋ ⟶ ℋ | |
| 3 | hodmval | ⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 −op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) ) | |
| 4 | 1 2 3 | mp2an | ⊢ ( 𝑆 −op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ) |
| 5 | 1 | ffvelrni | ⊢ ( 𝑥 ∈ ℋ → ( 𝑆 ‘ 𝑥 ) ∈ ℋ ) |
| 6 | 2 | ffvelrni | ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) |
| 7 | hvsubcl | ⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ ) | |
| 8 | 5 6 7 | syl2anc | ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ ) |
| 9 | 4 8 | fmpti | ⊢ ( 𝑆 −op 𝑇 ) : ℋ ⟶ ℋ |