HomeRelated theorems
GIF version
| Home |
Hilbert Space Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Law for sum and difference of Hilbert space operators. |
| Ref | Expression |
|---|---|
| hosdass.1 | ⊢ R: ℋ –→ ℋ |
| hosdass.2 | ⊢ S: ℋ –→ ℋ |
| hosdass.3 | ⊢ T: ℋ –→ ℋ |
| Ref | Expression |
|---|---|
| hosd | ⊢ ((R +P S) −P T) = ((R −P T) +P S) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hosdass.1 | . . . 4 ⊢ R: ℋ –→ ℋ | |
| 2 | hosdass.2 | . . . 4 ⊢ S: ℋ –→ ℋ | |
| 3 | 1, 2 | hoscom 5605 | . . 3 ⊢ (R +P S) = (S +P R) |
| 4 | 3 | opreq1i 3009 | . 2 ⊢ ((R +P S) −P T) = ((S +P R) −P T) |
| 5 | hosdass.3 | . . 3 ⊢ T: ℋ –→ ℋ | |
| 6 | 2, 1, 5 | hosdass 5621 | . 2 ⊢ ((S +P R) −P T) = (S +P (R −P T)) |
| 7 | 1, 5 | hodf 5603 | . . 3 ⊢ (R −P T): ℋ –→ ℋ |
| 8 | 2, 7 | hoscom 5605 | . 2 ⊢ (S +P (R −P T)) = ((R −P T) +P S) |
| 9 | 4, 6, 8 | 3eqtr 1123 | 1 ⊢ ((R +P S) −P T) = ((R −P T) +P S) |
| Colors of variables: wff set class |
| Syntax hints: = wceq 1091 –→wf 2418 (class class class)co 3001 ℋ chil 4958 +P chos 4977 −P cpjd 4978 |
| This theorem is referenced by: hosd1 5623 |
| This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079 ax-ac 1080 ax-hilex 4983 ax-hvaddcl 4984 ax-hvcom 4985 ax-hvass 4986 ax-hvzercl 4987 ax-hvaddid 4988 ax-hvmulcl 4989 ax-hvmulid 4991 ax-hvmulass 4992 ax-hvdistr1 4993 ax-hvdistr2 4994 ax-hvmulzer 4995 ax-hicl 5043 ax-his1 5045 ax-his2 5046 ax-his3 5047 ax-his4 5048 ax-hcompl 5113 |
| This theorem depends on definitions:
df-bi 128 df-or 197
df-an 198 df-3or 582 df-3an 583 df-ex 679
df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-sup 2154 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1st 3087 df-2nd 3088 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq |