![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > mdsymi | Structured version Visualization version GIF version |
Description: M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.) |
Ref | Expression |
---|---|
mdsym.1 | ⊢ 𝐴 ∈ Cℋ |
mdsym.2 | ⊢ 𝐵 ∈ Cℋ |
Ref | Expression |
---|---|
mdsymi | ⊢ (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mdsym.2 | . . . . 5 ⊢ 𝐵 ∈ Cℋ | |
2 | 1 | choccli 28471 | . . . 4 ⊢ (⊥‘𝐵) ∈ Cℋ |
3 | mdsym.1 | . . . . 5 ⊢ 𝐴 ∈ Cℋ | |
4 | 3 | choccli 28471 | . . . 4 ⊢ (⊥‘𝐴) ∈ Cℋ |
5 | eqid 2756 | . . . 4 ⊢ ((⊥‘𝐵) ∨ℋ 𝑥) = ((⊥‘𝐵) ∨ℋ 𝑥) | |
6 | 2, 4, 5 | mdsymlem8 29574 | . . 3 ⊢ (((⊥‘𝐵) ≠ 0ℋ ∧ (⊥‘𝐴) ≠ 0ℋ) → ((⊥‘𝐴) 𝑀ℋ* (⊥‘𝐵) ↔ (⊥‘𝐵) 𝑀ℋ* (⊥‘𝐴))) |
7 | mddmd 29465 | . . . 4 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ (⊥‘𝐴) 𝑀ℋ* (⊥‘𝐵))) | |
8 | 3, 1, 7 | mp2an 710 | . . 3 ⊢ (𝐴 𝑀ℋ 𝐵 ↔ (⊥‘𝐴) 𝑀ℋ* (⊥‘𝐵)) |
9 | mddmd 29465 | . . . 4 ⊢ ((𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → (𝐵 𝑀ℋ 𝐴 ↔ (⊥‘𝐵) 𝑀ℋ* (⊥‘𝐴))) | |
10 | 1, 3, 9 | mp2an 710 | . . 3 ⊢ (𝐵 𝑀ℋ 𝐴 ↔ (⊥‘𝐵) 𝑀ℋ* (⊥‘𝐴)) |
11 | 6, 8, 10 | 3bitr4g 303 | . 2 ⊢ (((⊥‘𝐵) ≠ 0ℋ ∧ (⊥‘𝐴) ≠ 0ℋ) → (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴)) |
12 | 3 | chssii 28393 | . . . 4 ⊢ 𝐴 ⊆ ℋ |
13 | fveq2 6348 | . . . . 5 ⊢ ((⊥‘𝐵) = 0ℋ → (⊥‘(⊥‘𝐵)) = (⊥‘0ℋ)) | |
14 | 1 | pjococi 28601 | . . . . 5 ⊢ (⊥‘(⊥‘𝐵)) = 𝐵 |
15 | choc0 28490 | . . . . 5 ⊢ (⊥‘0ℋ) = ℋ | |
16 | 13, 14, 15 | 3eqtr3g 2813 | . . . 4 ⊢ ((⊥‘𝐵) = 0ℋ → 𝐵 = ℋ) |
17 | 12, 16 | syl5sseqr 3791 | . . 3 ⊢ ((⊥‘𝐵) = 0ℋ → 𝐴 ⊆ 𝐵) |
18 | ssmd1 29475 | . . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐴 𝑀ℋ 𝐵) | |
19 | 3, 1, 18 | mp3an12 1559 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 𝑀ℋ 𝐵) |
20 | ssmd2 29476 | . . . . 5 ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐵 𝑀ℋ 𝐴) | |
21 | 3, 1, 20 | mp3an12 1559 | . . . 4 ⊢ (𝐴 ⊆ 𝐵 → 𝐵 𝑀ℋ 𝐴) |
22 | 19, 21 | jca 555 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ 𝐴)) |
23 | pm5.1 938 | . . 3 ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ 𝐴) → (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴)) | |
24 | 17, 22, 23 | 3syl 18 | . 2 ⊢ ((⊥‘𝐵) = 0ℋ → (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴)) |
25 | 1 | chssii 28393 | . . . 4 ⊢ 𝐵 ⊆ ℋ |
26 | fveq2 6348 | . . . . 5 ⊢ ((⊥‘𝐴) = 0ℋ → (⊥‘(⊥‘𝐴)) = (⊥‘0ℋ)) | |
27 | 3 | pjococi 28601 | . . . . 5 ⊢ (⊥‘(⊥‘𝐴)) = 𝐴 |
28 | 26, 27, 15 | 3eqtr3g 2813 | . . . 4 ⊢ ((⊥‘𝐴) = 0ℋ → 𝐴 = ℋ) |
29 | 25, 28 | syl5sseqr 3791 | . . 3 ⊢ ((⊥‘𝐴) = 0ℋ → 𝐵 ⊆ 𝐴) |
30 | ssmd2 29476 | . . . . 5 ⊢ ((𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝐵 ⊆ 𝐴) → 𝐴 𝑀ℋ 𝐵) | |
31 | 1, 3, 30 | mp3an12 1559 | . . . 4 ⊢ (𝐵 ⊆ 𝐴 → 𝐴 𝑀ℋ 𝐵) |
32 | ssmd1 29475 | . . . . 5 ⊢ ((𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝐵 ⊆ 𝐴) → 𝐵 𝑀ℋ 𝐴) | |
33 | 1, 3, 32 | mp3an12 1559 | . . . 4 ⊢ (𝐵 ⊆ 𝐴 → 𝐵 𝑀ℋ 𝐴) |
34 | 31, 33 | jca 555 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ 𝐴)) |
35 | 29, 34, 23 | 3syl 18 | . 2 ⊢ ((⊥‘𝐴) = 0ℋ → (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴)) |
36 | 11, 24, 35 | pm2.61iine 3018 | 1 ⊢ (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 = wceq 1628 ∈ wcel 2135 ≠ wne 2928 ⊆ wss 3711 class class class wbr 4800 ‘cfv 6045 (class class class)co 6809 ℋchil 28081 Cℋ cch 28091 ⊥cort 28092 ∨ℋ chj 28095 0ℋc0h 28097 𝑀ℋ cmd 28128 𝑀ℋ* cdmd 28129 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-8 2137 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 ax-rep 4919 ax-sep 4929 ax-nul 4937 ax-pow 4988 ax-pr 5051 ax-un 7110 ax-inf2 8707 ax-cc 9445 ax-cnex 10180 ax-resscn 10181 ax-1cn 10182 ax-icn 10183 ax-addcl 10184 ax-addrcl 10185 ax-mulcl 10186 ax-mulrcl 10187 ax-mulcom 10188 ax-addass 10189 ax-mulass 10190 ax-distr 10191 ax-i2m1 10192 ax-1ne0 10193 ax-1rid 10194 ax-rnegex 10195 ax-rrecex 10196 ax-cnre 10197 ax-pre-lttri 10198 ax-pre-lttrn 10199 ax-pre-ltadd 10200 ax-pre-mulgt0 10201 ax-pre-sup 10202 ax-addf 10203 ax-mulf 10204 ax-hilex 28161 ax-hfvadd 28162 ax-hvcom 28163 ax-hvass 28164 ax-hv0cl 28165 ax-hvaddid 28166 ax-hfvmul 28167 ax-hvmulid 28168 ax-hvmulass 28169 ax-hvdistr1 28170 ax-hvdistr2 28171 ax-hvmul0 28172 ax-hfi 28241 ax-his1 28244 ax-his2 28245 ax-his3 28246 ax-his4 28247 ax-hcompl 28364 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1631 df-fal 1634 df-ex 1850 df-nf 1855 df-sb 2043 df-eu 2607 df-mo 2608 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-ne 2929 df-nel 3032 df-ral 3051 df-rex 3052 df-reu 3053 df-rmo 3054 df-rab 3055 df-v 3338 df-sbc 3573 df-csb 3671 df-dif 3714 df-un 3716 df-in 3718 df-ss 3725 df-pss 3727 df-nul 4055 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4585 df-int 4624 df-iun 4670 df-iin 4671 df-br 4801 df-opab 4861 df-mpt 4878 df-tr 4901 df-id 5170 df-eprel 5175 df-po 5183 df-so 5184 df-fr 5221 df-se 5222 df-we 5223 df-xp 5268 df-rel 5269 df-cnv 5270 df-co 5271 df-dm 5272 df-rn 5273 df-res 5274 df-ima 5275 df-pred 5837 df-ord 5883 df-on 5884 df-lim 5885 df-suc 5886 df-iota 6008 df-fun 6047 df-fn 6048 df-f 6049 df-f1 6050 df-fo 6051 df-f1o 6052 df-fv 6053 df-isom 6054 df-riota 6770 df-ov 6812 df-oprab 6813 df-mpt2 6814 df-of 7058 df-om 7227 df-1st 7329 df-2nd 7330 df-supp 7460 df-wrecs 7572 df-recs 7633 df-rdg 7671 df-1o 7725 df-2o 7726 df-oadd 7729 df-omul 7730 df-er 7907 df-map 8021 df-pm 8022 df-ixp 8071 df-en 8118 df-dom 8119 df-sdom 8120 df-fin 8121 df-fsupp 8437 df-fi 8478 df-sup 8509 df-inf 8510 df-oi 8576 df-card 8951 df-acn 8954 df-cda 9178 df-pnf 10264 df-mnf 10265 df-xr 10266 df-ltxr 10267 df-le 10268 df-sub 10456 df-neg 10457 df-div 10873 df-nn 11209 df-2 11267 df-3 11268 df-4 11269 df-5 11270 df-6 11271 df-7 11272 df-8 11273 df-9 11274 df-n0 11481 df-z 11566 df-dec 11682 df-uz 11876 df-q 11978 df-rp 12022 df-xneg 12135 df-xadd 12136 df-xmul 12137 df-ioo 12368 df-ico 12370 df-icc 12371 df-fz 12516 df-fzo 12656 df-fl 12783 df-seq 12992 df-exp 13051 df-hash 13308 df-cj 14034 df-re 14035 df-im 14036 df-sqrt 14170 df-abs 14171 df-clim 14414 df-rlim 14415 df-sum 14612 df-struct 16057 df-ndx 16058 df-slot 16059 df-base 16061 df-sets 16062 df-ress 16063 df-plusg 16152 df-mulr 16153 df-starv 16154 df-sca 16155 df-vsca 16156 df-ip 16157 df-tset 16158 df-ple 16159 df-ds 16162 df-unif 16163 df-hom 16164 df-cco 16165 df-rest 16281 df-topn 16282 df-0g 16300 df-gsum 16301 df-topgen 16302 df-pt 16303 df-prds 16306 df-xrs 16360 df-qtop 16365 df-imas 16366 df-xps 16368 df-mre 16444 df-mrc 16445 df-acs 16447 df-mgm 17439 df-sgrp 17481 df-mnd 17492 df-submnd 17533 df-mulg 17738 df-cntz 17946 df-cmn 18391 df-psmet 19936 df-xmet 19937 df-met 19938 df-bl 19939 df-mopn 19940 df-fbas 19941 df-fg 19942 df-cnfld 19945 df-top 20897 df-topon 20914 df-topsp 20935 df-bases 20948 df-cld 21021 df-ntr 21022 df-cls 21023 df-nei 21100 df-cn 21229 df-cnp 21230 df-lm 21231 df-haus 21317 df-tx 21563 df-hmeo 21756 df-fil 21847 df-fm 21939 df-flim 21940 df-flf 21941 df-xms 22322 df-ms 22323 df-tms 22324 df-cfil 23249 df-cau 23250 df-cmet 23251 df-grpo 27652 df-gid 27653 df-ginv 27654 df-gdiv 27655 df-ablo 27704 df-vc 27719 df-nv 27752 df-va 27755 df-ba 27756 df-sm 27757 df-0v 27758 df-vs 27759 df-nmcv 27760 df-ims 27761 df-dip 27861 df-ssp 27882 df-ph 27973 df-cbn 28024 df-hnorm 28130 df-hba 28131 df-hvsub 28133 df-hlim 28134 df-hcau 28135 df-sh 28369 df-ch 28383 df-oc 28414 df-ch0 28415 df-shs 28472 df-span 28473 df-chj 28474 df-chsup 28475 df-pjh 28559 df-cv 29443 df-md 29444 df-dmd 29445 df-at 29502 |
This theorem is referenced by: mdsym 29576 |
Copyright terms: Public domain | W3C validator |