![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > HSE Home > Th. List > hoeqi | Unicode 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 23216 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 654 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: hoaddcomi 23228 hodsi 23231 hoaddassi 23232 hocadddiri 23235 hocsubdiri 23236 hoaddid1i 23242 ho0coi 23244 hoid1i 23245 hoid1ri 23246 honegsubi 23252 hoddii 23445 pjsdii 23611 pjddii 23612 pjss1coi 23619 pjss2coi 23620 pjorthcoi 23625 pjscji 23626 pjtoi 23635 pjclem4 23655 pj3si 23663 pj3cor1i 23665 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-ral 2671 df-rex 2672 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-nul 3589 df-if 3700 df-sn 3780 df-pr 3781 df-op 3783 df-uni 3976 df-br 4173 df-opab 4227 df-mpt 4228 df-id 4458 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-fv 5421 |
Copyright terms: Public domain | W3C validator |