HomeRelated theorems
GIF version
| Home |
Hilbert Space Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: A Hilbert lattice element commutes with its meet. |
| Ref | Expression |
|---|---|
| pjoml2.1 | ⊢ A ∈ Cℋ |
| pjoml2.2 | ⊢ B ∈ Cℋ |
| Ref | Expression |
|---|---|
| cmm1 | ⊢ A Com (A ∩ B) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pjoml2.1 | . . 3 ⊢ Ù/FONT>A ∈ Cℋ | |
| 2 | pjoml2.2 | . . 3 ⊢ B ∈ Cℋ | |
| 3 | 1, 2 | chincl 5382 | . 2 ⊢ (A ∩ B) ∈ Cℋ |
| 4 | inss1 1657 | . . 3 ⊢ (A ∩ B) ⊆ A | |
| 5 | 3, 1, 4 | cmle 5511 | . 2 ⊢ (A ∩ B) Com A |
| 6 | 3, 1, 5 | cmcmi 5506 | 1 ⊢ A Com (A ∩ B) |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 1092 ∩ cin 1486 class class class wbr 2054 Cℋ cch 4968 Com ccm 4975 |
| This theorem is referenced by: cmm2 5515 |
| 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 |