| Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HSE Home > Th. List > chjcomi | Structured version Visualization version GIF version | ||
| Description: Commutative law for join in Cℋ. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ch0le.1 | ⊢ 𝐴 ∈ Cℋ |
| chjcl.2 | ⊢ 𝐵 ∈ Cℋ |
| Ref | Expression |
|---|---|
| chjcomi | ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ch0le.1 | . . 3 ⊢ 𝐴 ∈ Cℋ | |
| 2 | 1 | chshii 31190 | . 2 ⊢ 𝐴 ∈ Sℋ |
| 3 | chjcl.2 | . . 3 ⊢ 𝐵 ∈ Cℋ | |
| 4 | 3 | chshii 31190 | . 2 ⊢ 𝐵 ∈ Sℋ |
| 5 | 2, 4 | shjcomi 31334 | 1 ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∈ wcel 2109 (class class class)co 7353 Cℋ cch 30892 ∨ℋ chj 30896 |
| 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 5238 ax-nul 5248 ax-pr 5374 ax-hilex 30962 |
| 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 3397 df-v 3440 df-sbc 3745 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-br 5096 df-opab 5158 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-iota 6442 df-fun 6488 df-fv 6494 df-ov 7356 df-oprab 7357 df-mpo 7358 df-sh 31170 df-ch 31184 df-chj 31273 |
| This theorem is referenced by: chub2i 31433 chnlei 31448 chj12i 31485 lejdiri 31502 cmcm2i 31556 cmbr3i 31563 qlax2i 31591 osumcor2i 31607 3oalem5 31629 pjcji 31647 mayetes3i 31692 mdslj2i 32283 mdsl1i 32284 cvmdi 32287 mdslmd2i 32293 mdexchi 32298 cvexchi 32332 atabsi 32364 mdsymlem1 32366 mdsymlem6 32371 mdsymlem8 32373 sumdmdlem2 32382 dmdbr5ati 32385 |
| Copyright terms: Public domain | W3C validator |