![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > HSE Home > Th. List > hocoi | Unicode version |
Description: Composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
Ref | Expression |
---|---|
hoeq.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
hoeq.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
hocoi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hoeq.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fvco3 5767 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpan 652 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: hococli 23229 hocadddiri 23243 hocsubdiri 23244 ho2coi 23245 ho0coi 23252 hoid1i 23253 hoid1ri 23254 hoddii 23453 lnopcoi 23467 lnopco0i 23468 nmopcoi 23559 adjcoi 23564 nmopcoadji 23565 hmopidmchi 23615 hmopidmpji 23616 pjsdii 23619 pjddii 23620 pjcoi 23622 pjcohocli 23667 pjadj2coi 23668 pj3lem1 23670 |
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 2393 ax-sep 4298 ax-nul 4306 ax-pow 4345 ax-pr 4371 |
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 2266 df-mo 2267 df-clab 2399 df-cleq 2405 df-clel 2408 df-nfc 2537 df-ne 2577 df-ral 2679 df-rex 2680 df-rab 2683 df-v 2926 df-sbc 3130 df-dif 3291 df-un 3293 df-in 3295 df-ss 3302 df-nul 3597 df-if 3708 df-sn 3788 df-pr 3789 df-op 3791 df-uni 3984 df-br 4181 df-opab 4235 df-id 4466 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5385 df-fun 5423 df-fn 5424 df-f 5425 df-fv 5429 |
Copyright terms: Public domain | W3C validator |