| Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HSE Home > Th. List > hoeqi | Structured version Visualization version GIF version | ||
| Description: Equality of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| hoeq.1 | ⊢ 𝑆: ℋ⟶ ℋ |
| hoeq.2 | ⊢ 𝑇: ℋ⟶ ℋ |
| Ref | Expression |
|---|---|
| hoeqi | ⊢ (∀𝑥 ∈ ℋ (𝑆‘𝑥) = (𝑇‘𝑥) ↔ 𝑆 = 𝑇) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hoeq.1 | . 2 ⊢ 𝑆: ℋ⟶ ℋ | |
| 2 | hoeq.2 | . 2 ⊢ 𝑇: ℋ⟶ ℋ | |
| 3 | hoeq 31691 | . 2 ⊢ ((𝑆: ℋ⟶ ℋ ∧ 𝑇: ℋ⟶ ℋ) → (∀𝑥 ∈ ℋ (𝑆‘𝑥) = (𝑇‘𝑥) ↔ 𝑆 = 𝑇)) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (∀𝑥 ∈ ℋ (𝑆‘𝑥) = (𝑇‘𝑥) ↔ 𝑆 = 𝑇) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 ∀wral 3044 ⟶wf 6472 ‘cfv 6476 ℋchba 30850 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5231 ax-nul 5241 ax-pr 5367 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rab 3393 df-v 3435 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4281 df-if 4473 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-br 5089 df-opab 5151 df-mpt 5170 df-id 5508 df-xp 5619 df-rel 5620 df-cnv 5621 df-co 5622 df-dm 5623 df-rn 5624 df-res 5625 df-ima 5626 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-fv 6484 |
| This theorem is referenced by: hoaddcomi 31703 hodsi 31706 hoaddassi 31707 hocadddiri 31710 hocsubdiri 31711 hoaddridi 31717 ho0coi 31719 hoid1i 31720 hoid1ri 31721 honegsubi 31727 hoddii 31920 pjsdii 32086 pjddii 32087 pjss1coi 32094 pjss2coi 32095 pjorthcoi 32100 pjscji 32101 pjtoi 32110 pjclem4 32130 pj3si 32138 pj3cor1i 32140 |
| Copyright terms: Public domain | W3C validator |