Nearby theorems
|
|
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > HSE Home > Th. List > mdslmd2i | Structured version Visualization version GIF version | ||
| Description: Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2 (join version). (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| mdslmd.1 | ⊢ 𝐴 ∈ Cℋ |
| mdslmd.2 | ⊢ 𝐵 ∈ Cℋ |
| mdslmd.3 | ⊢ 𝐶 ∈ Cℋ |
| mdslmd.4 | ⊢ 𝐷 ∈ Cℋ |
| Ref | Expression |
|---|---|
| mdslmd2i | ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵)) → (𝐶 𝑀ℋ 𝐷 ↔ (𝐶 ∨ℋ 𝐴) 𝑀ℋ (𝐷 ∨ℋ 𝐴))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mdslmd.3 | . . . . . . . 8 ⊢ 𝐶 ∈ Cℋ | |
| 2 | mdslmd.4 | . . . . . . . 8 ⊢ 𝐷 ∈ Cℋ | |
| 3 | 1, 2 | chjcli 32105 | . . . . . . 7 ⊢ (𝐶 ∨ℋ 𝐷) ∈ Cℋ |
| 4 | mdslmd.2 | . . . . . . 7 ⊢ 𝐵 ∈ Cℋ | |
| 5 | mdslmd.1 | . . . . . . 7 ⊢ 𝐴 ∈ Cℋ | |
| 6 | 3, 4, 5 | chlej1i 32121 | . . . . . 6 ⊢ ((𝐶 ∨ℋ 𝐷) ⊆ 𝐵 → ((𝐶 ∨ℋ 𝐷) ∨ℋ 𝐴) ⊆ (𝐵 ∨ℋ 𝐴)) |
| 7 | 1, 2, 5 | chjjdiri 32172 | . . . . . 6 ⊢ ((𝐶 ∨ℋ 𝐷) ∨ℋ 𝐴) = ((𝐶 ∨ℋ 𝐴) ∨ℋ (𝐷 ∨ℋ 𝐴)) |
| 8 | 4, 5 | chjcomi 32116 | . . . . . 6 ⊢ (𝐵 ∨ℋ 𝐴) = (𝐴 ∨ℋ 𝐵) |
| 9 | 6, 7, 8 | 3sstr3g 3965 | . . . . 5 ⊢ ((𝐶 ∨ℋ 𝐷) ⊆ 𝐵 → ((𝐶 ∨ℋ 𝐴) ∨ℋ (𝐷 ∨ℋ 𝐴)) ⊆ (𝐴 ∨ℋ 𝐵)) |
| 10 | 9 | adantl 487 | . . . 4 ⊢ (((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵) → ((𝐶 ∨ℋ 𝐴) ∨ℋ (𝐷 ∨ℋ 𝐴)) ⊆ (𝐴 ∨ℋ 𝐵)) |
| 11 | 5, 1 | chub2i 32118 | . . . . 5 ⊢ 𝐴 ⊆ (𝐶 ∨ℋ 𝐴) |
| 12 | 5, 2 | chub2i 32118 | . . . . 5 ⊢ 𝐴 ⊆ (𝐷 ∨ℋ 𝐴) |
| 13 | 11, 12 | ssini 4139 | . . . 4 ⊢ 𝐴 ⊆ ((𝐶 ∨ℋ 𝐴) ∩ (𝐷 ∨ℋ 𝐴)) |
| 14 | 10, 13 | jctil 529 | . . 3 ⊢ (((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵) → (𝐴 ⊆ ((𝐶 ∨ℋ 𝐴) ∩ (𝐷 ∨ℋ 𝐴)) ∧ ((𝐶 ∨ℋ 𝐴) ∨ℋ (𝐷 ∨ℋ 𝐴)) ⊆ (𝐴 ∨ℋ 𝐵))) |
| 15 | 1, 5 | chjcli 32105 | . . . 4 ⊢ (𝐶 ∨ℋ 𝐴) ∈ Cℋ |
| 16 | 2, 5 | chjcli 32105 | . . . 4 ⊢ (𝐷 ∨ℋ 𝐴) ∈ Cℋ |
| 17 | 5, 4, 15, 16 | mdslmd1i 32977 | . . 3 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ ((𝐶 ∨ℋ 𝐴) ∩ (𝐷 ∨ℋ 𝐴)) ∧ ((𝐶 ∨ℋ 𝐴) ∨ℋ (𝐷 ∨ℋ 𝐴)) ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∨ℋ 𝐴) 𝑀ℋ (𝐷 ∨ℋ 𝐴) ↔ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) 𝑀ℋ ((𝐷 ∨ℋ 𝐴) ∩ 𝐵))) |
| 18 | 14, 17 | sylan2 605 | . 2 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵)) → ((𝐶 ∨ℋ 𝐴) 𝑀ℋ (𝐷 ∨ℋ 𝐴) ↔ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) 𝑀ℋ ((𝐷 ∨ℋ 𝐴) ∩ 𝐵))) |
| 19 | id 23 | . . . . . 6 ⊢ (𝐴 𝑀ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵) | |
| 20 | inss1 4136 | . . . . . . 7 ⊢ (𝐶 ∩ 𝐷) ⊆ 𝐶 | |
| 21 | sstr 3921 | . . . . . . 7 ⊢ (((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∩ 𝐷) ⊆ 𝐶) → (𝐴 ∩ 𝐵) ⊆ 𝐶) | |
| 22 | 20, 21 | mpan2 704 | . . . . . 6 ⊢ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) → (𝐴 ∩ 𝐵) ⊆ 𝐶) |
| 23 | 1, 2 | chub1i 32117 | . . . . . . 7 ⊢ 𝐶 ⊆ (𝐶 ∨ℋ 𝐷) |
| 24 | sstr 3921 | . . . . . . 7 ⊢ ((𝐶 ⊆ (𝐶 ∨ℋ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵) → 𝐶 ⊆ 𝐵) | |
| 25 | 23, 24 | mpan 703 | . . . . . 6 ⊢ ((𝐶 ∨ℋ 𝐷) ⊆ 𝐵 → 𝐶 ⊆ 𝐵) |
| 26 | 5, 4, 1 | 3pm3.2i 1358 | . . . . . . 7 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) |
| 27 | mdsl3 32964 | . . . . . . 7 ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵)) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = 𝐶) | |
| 28 | 26, 27 | mpan 703 | . . . . . 6 ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = 𝐶) |
| 29 | 19, 22, 25, 28 | syl3an 1178 | . . . . 5 ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = 𝐶) |
| 30 | inss2 4137 | . . . . . . 7 ⊢ (𝐶 ∩ 𝐷) ⊆ 𝐷 | |
| 31 | sstr 3921 | . . . . . . 7 ⊢ (((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∩ 𝐷) ⊆ 𝐷) → (𝐴 ∩ 𝐵) ⊆ 𝐷) | |
| 32 | 30, 31 | mpan2 704 | . . . . . 6 ⊢ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) → (𝐴 ∩ 𝐵) ⊆ 𝐷) |
| 33 | 2, 1 | chub2i 32118 | . . . . . . 7 ⊢ 𝐷 ⊆ (𝐶 ∨ℋ 𝐷) |
| 34 | sstr 3921 | . . . . . . 7 ⊢ ((𝐷 ⊆ (𝐶 ∨ℋ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵) → 𝐷 ⊆ 𝐵) | |
| 35 | 33, 34 | mpan 703 | . . . . . 6 ⊢ ((𝐶 ∨ℋ 𝐷) ⊆ 𝐵 → 𝐷 ⊆ 𝐵) |
| 36 | 5, 4, 2 | 3pm3.2i 1358 | . . . . . . 7 ⊢ (𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) |
| 37 | mdsl3 32964 | . . . . . . 7 ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵)) → ((𝐷 ∨ℋ 𝐴) ∩ 𝐵) = 𝐷) | |
| 38 | 36, 37 | mpan 703 | . . . . . 6 ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵) → ((𝐷 ∨ℋ 𝐴) ∩ 𝐵) = 𝐷) |
| 39 | 19, 32, 35, 38 | syl3an 1178 | . . . . 5 ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵) → ((𝐷 ∨ℋ 𝐴) ∩ 𝐵) = 𝐷) |
| 40 | 29, 39 | breq12d 5119 | . . . 4 ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵) → (((𝐶 ∨ℋ 𝐴) ∩ 𝐵) 𝑀ℋ ((𝐷 ∨ℋ 𝐴) ∩ 𝐵) ↔ 𝐶 𝑀ℋ 𝐷)) |
| 41 | 40 | 3expb 1138 | . . 3 ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵)) → (((𝐶 ∨ℋ 𝐴) ∩ 𝐵) 𝑀ℋ ((𝐷 ∨ℋ 𝐴) ∩ 𝐵) ↔ 𝐶 𝑀ℋ 𝐷)) |
| 42 | 41 | adantlr 728 | . 2 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵)) → (((𝐶 ∨ℋ 𝐴) ∩ 𝐵) 𝑀ℋ ((𝐷 ∨ℋ 𝐴) ∩ 𝐵) ↔ 𝐶 𝑀ℋ 𝐷)) |
| 43 | 18, 42 | bitr2d 283 | 1 ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵)) → (𝐶 𝑀ℋ 𝐷 ↔ (𝐶 ∨ℋ 𝐴) 𝑀ℋ (𝐷 ∨ℋ 𝐴))) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ⊆ wss 3900 ∩ cin 4092 class class class wbr 5106 (class class class)co 7449 Cℋ cch 31577 ∨ℋ chj 31581 𝑀ℋ cmd 31614 𝑀ℋ* cdmd 31615 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-inf2 9677 ax-cc 10550 ax-cnex 11293 ax-resscn 11294 ax-1cn 11295 ax-icn 11296 ax-addcl 11297 ax-addrcl 11298 ax-mulcl 11299 ax-mulrcl 11300 ax-mulcom 11301 ax-addass 11302 ax-mulass 11303 ax-distr 11304 ax-i2m1 11305 ax-1ne0 11306 ax-1rid 11307 ax-rnegex 11308 ax-rrecex 11309 ax-cnre 11310 ax-pre-lttri 11311 ax-pre-lttrn 11312 ax-pre-ltadd 11313 ax-pre-mulgt0 11314 ax-pre-sup 11315 ax-addf 11316 ax-mulf 11317 ax-hilex 31647 ax-hfvadd 31648 ax-hvcom 31649 ax-hvass 31650 ax-hv0cl 31651 ax-hvaddid 31652 ax-hfvmul 31653 ax-hvmulid 31654 ax-hvmulass 31655 ax-hvdistr1 31656 ax-hvdistr2 31657 ax-hvmul0 31658 ax-hfi 31727 ax-his1 31730 ax-his2 31731 ax-his3 31732 ax-his4 31733 ax-hcompl 31850 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-isom 6573 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-of 7723 df-om 7910 df-1st 8033 df-2nd 8034 df-supp 8213 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-1o 8512 df-2o 8513 df-oadd 8516 df-omul 8517 df-er 8753 df-map 8885 df-pm 8886 df-ixp 8962 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-fsupp 9390 df-fi 9438 df-sup 9469 df-inf 9470 df-oi 9539 df-card 10055 df-acn 10058 df-pnf 11382 df-mnf 11383 df-xr 11384 df-ltxr 11385 df-le 11386 df-sub 11580 df-neg 11581 df-div 12012 df-nn 12374 df-2 12443 df-3 12444 df-4 12445 df-5 12446 df-6 12447 df-7 12448 df-8 12449 df-9 12450 df-n0 12645 df-z 12732 df-dec 12853 df-uz 13004 df-q 13114 df-rp 13159 df-xneg 13279 df-xadd 13280 df-xmul 13281 df-ioo 13518 df-ico 13520 df-icc 13521 df-fz 13678 df-fzo 13827 df-fl 13970 df-seq 14183 df-exp 14243 df-hash 14514 df-cj 15307 df-re 15308 df-im 15309 df-sqrt 15443 df-abs 15444 df-clim 15696 df-rlim 15697 df-sum 15895 df-struct 17366 df-sets 17383 df-slot 17401 df-ndx 17413 df-base 17429 df-ress 17450 df-plusg 17482 df-mulr 17483 df-starv 17484 df-sca 17485 df-vsca 17486 df-ip 17487 df-tset 17488 df-ple 17489 df-ds 17491 df-unif 17492 df-hom 17493 df-cco 17494 df-rest 17634 df-topn 17635 df-0g 17653 df-gsum 17654 df-topgen 17655 df-pt 17656 df-prds 17659 df-xrs 17715 df-qtop 17720 df-imas 17721 df-xps 17723 df-mre 17797 df-mrc 17798 df-acs 17800 df-mgm 18857 df-sgrp 18949 df-mnd 18965 df-submnd 19020 df-mulg 19319 df-cntz 19573 df-cmn 20038 df-psmet 21712 df-xmet 21713 df-met 21714 df-bl 21715 df-mopn 21716 df-fbas 21717 df-fg 21718 df-cnfld 21721 df-top 23256 df-topon 23273 df-topsp 23295 df-bases 23308 df-cld 23381 df-ntr 23382 df-cls 23383 df-nei 23460 df-cn 23589 df-cnp 23590 df-lm 23591 df-haus 23677 df-tx 23925 df-hmeo 24118 df-fil 24209 df-fm 24301 df-flim 24302 df-flf 24303 df-xms 24683 df-ms 24684 df-tms 24685 df-cfil 25620 df-cau 25621 df-cmet 25622 df-grpo 31141 df-gid 31142 df-ginv 31143 df-gdiv 31144 df-ablo 31193 df-vc 31207 df-nv 31240 df-va 31243 df-ba 31244 df-sm 31245 df-0v 31246 df-vs 31247 df-nmcv 31248 df-ims 31249 df-dip 31349 df-ssp 31370 df-ph 31461 df-cbn 31511 df-hnorm 31616 df-hba 31617 df-hvsub 31619 df-hlim 31620 df-hcau 31621 df-sh 31855 df-ch 31869 df-oc 31900 df-ch0 31901 df-shs 31956 df-chj 31958 df-md 32928 df-dmd 32929 |
| This theorem is used by: mdsldmd1i 32979 |
| Copyright terms: Public domain | W3C validator |