Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > h1de2ctlem | Structured version Visualization version GIF version |
Description: Lemma for h1de2ci 30303. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
Ref | Expression |
---|---|
h1de2.1 | โข ๐ด โ โ |
h1de2.2 | โข ๐ต โ โ |
Ref | Expression |
---|---|
h1de2ctlem | โข (๐ด โ (โฅโ(โฅโ{๐ต})) โ โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | h1de2.1 | . . . . . . . 8 โข ๐ด โ โ | |
2 | 1 | elexi 3463 | . . . . . . 7 โข ๐ด โ V |
3 | 2 | elsn 4600 | . . . . . 6 โข (๐ด โ {0โ} โ ๐ด = 0โ) |
4 | hsn0elch 29995 | . . . . . . . 8 โข {0โ} โ Cโ | |
5 | 4 | ococi 30152 | . . . . . . 7 โข (โฅโ(โฅโ{0โ})) = {0โ} |
6 | 5 | eleq2i 2830 | . . . . . 6 โข (๐ด โ (โฅโ(โฅโ{0โ})) โ ๐ด โ {0โ}) |
7 | h1de2.2 | . . . . . . . 8 โข ๐ต โ โ | |
8 | ax-hvmul0 29757 | . . . . . . . 8 โข (๐ต โ โ โ (0 ยทโ ๐ต) = 0โ) | |
9 | 7, 8 | ax-mp 5 | . . . . . . 7 โข (0 ยทโ ๐ต) = 0โ |
10 | 9 | eqeq2i 2751 | . . . . . 6 โข (๐ด = (0 ยทโ ๐ต) โ ๐ด = 0โ) |
11 | 3, 6, 10 | 3bitr4ri 304 | . . . . 5 โข (๐ด = (0 ยทโ ๐ต) โ ๐ด โ (โฅโ(โฅโ{0โ}))) |
12 | sneq 4595 | . . . . . . . 8 โข (๐ต = 0โ โ {๐ต} = {0โ}) | |
13 | 12 | fveq2d 6842 | . . . . . . 7 โข (๐ต = 0โ โ (โฅโ{๐ต}) = (โฅโ{0โ})) |
14 | 13 | fveq2d 6842 | . . . . . 6 โข (๐ต = 0โ โ (โฅโ(โฅโ{๐ต})) = (โฅโ(โฅโ{0โ}))) |
15 | 14 | eleq2d 2824 | . . . . 5 โข (๐ต = 0โ โ (๐ด โ (โฅโ(โฅโ{๐ต})) โ ๐ด โ (โฅโ(โฅโ{0โ})))) |
16 | 11, 15 | bitr4id 290 | . . . 4 โข (๐ต = 0โ โ (๐ด = (0 ยทโ ๐ต) โ ๐ด โ (โฅโ(โฅโ{๐ต})))) |
17 | 0cn 11081 | . . . . 5 โข 0 โ โ | |
18 | oveq1 7357 | . . . . . 6 โข (๐ฅ = 0 โ (๐ฅ ยทโ ๐ต) = (0 ยทโ ๐ต)) | |
19 | 18 | rspceeqv 3594 | . . . . 5 โข ((0 โ โ โง ๐ด = (0 ยทโ ๐ต)) โ โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต)) |
20 | 17, 19 | mpan 689 | . . . 4 โข (๐ด = (0 ยทโ ๐ต) โ โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต)) |
21 | 16, 20 | syl6bir 254 | . . 3 โข (๐ต = 0โ โ (๐ด โ (โฅโ(โฅโ{๐ต})) โ โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต))) |
22 | 1, 7 | h1de2bi 30301 | . . . 4 โข (๐ต โ 0โ โ (๐ด โ (โฅโ(โฅโ{๐ต})) โ ๐ด = (((๐ด ยทih ๐ต) / (๐ต ยทih ๐ต)) ยทโ ๐ต))) |
23 | his6 29846 | . . . . . . . . 9 โข (๐ต โ โ โ ((๐ต ยทih ๐ต) = 0 โ ๐ต = 0โ)) | |
24 | 7, 23 | ax-mp 5 | . . . . . . . 8 โข ((๐ต ยทih ๐ต) = 0 โ ๐ต = 0โ) |
25 | 24 | necon3bii 2995 | . . . . . . 7 โข ((๐ต ยทih ๐ต) โ 0 โ ๐ต โ 0โ) |
26 | 1, 7 | hicli 29828 | . . . . . . . 8 โข (๐ด ยทih ๐ต) โ โ |
27 | 7, 7 | hicli 29828 | . . . . . . . 8 โข (๐ต ยทih ๐ต) โ โ |
28 | 26, 27 | divclzi 11824 | . . . . . . 7 โข ((๐ต ยทih ๐ต) โ 0 โ ((๐ด ยทih ๐ต) / (๐ต ยทih ๐ต)) โ โ) |
29 | 25, 28 | sylbir 234 | . . . . . 6 โข (๐ต โ 0โ โ ((๐ด ยทih ๐ต) / (๐ต ยทih ๐ต)) โ โ) |
30 | oveq1 7357 | . . . . . . 7 โข (๐ฅ = ((๐ด ยทih ๐ต) / (๐ต ยทih ๐ต)) โ (๐ฅ ยทโ ๐ต) = (((๐ด ยทih ๐ต) / (๐ต ยทih ๐ต)) ยทโ ๐ต)) | |
31 | 30 | rspceeqv 3594 | . . . . . 6 โข ((((๐ด ยทih ๐ต) / (๐ต ยทih ๐ต)) โ โ โง ๐ด = (((๐ด ยทih ๐ต) / (๐ต ยทih ๐ต)) ยทโ ๐ต)) โ โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต)) |
32 | 29, 31 | sylan 581 | . . . . 5 โข ((๐ต โ 0โ โง ๐ด = (((๐ด ยทih ๐ต) / (๐ต ยทih ๐ต)) ยทโ ๐ต)) โ โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต)) |
33 | 32 | ex 414 | . . . 4 โข (๐ต โ 0โ โ (๐ด = (((๐ด ยทih ๐ต) / (๐ต ยทih ๐ต)) ยทโ ๐ต) โ โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต))) |
34 | 22, 33 | sylbid 239 | . . 3 โข (๐ต โ 0โ โ (๐ด โ (โฅโ(โฅโ{๐ต})) โ โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต))) |
35 | 21, 34 | pm2.61ine 3027 | . 2 โข (๐ด โ (โฅโ(โฅโ{๐ต})) โ โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต)) |
36 | snssi 4767 | . . . . . . . 8 โข (๐ต โ โ โ {๐ต} โ โ) | |
37 | occl 30051 | . . . . . . . 8 โข ({๐ต} โ โ โ (โฅโ{๐ต}) โ Cโ ) | |
38 | 7, 36, 37 | mp2b 10 | . . . . . . 7 โข (โฅโ{๐ต}) โ Cโ |
39 | 38 | choccli 30054 | . . . . . 6 โข (โฅโ(โฅโ{๐ต})) โ Cโ |
40 | 39 | chshii 29974 | . . . . 5 โข (โฅโ(โฅโ{๐ต})) โ Sโ |
41 | h1did 30298 | . . . . . 6 โข (๐ต โ โ โ ๐ต โ (โฅโ(โฅโ{๐ต}))) | |
42 | 7, 41 | ax-mp 5 | . . . . 5 โข ๐ต โ (โฅโ(โฅโ{๐ต})) |
43 | shmulcl 29965 | . . . . 5 โข (((โฅโ(โฅโ{๐ต})) โ Sโ โง ๐ฅ โ โ โง ๐ต โ (โฅโ(โฅโ{๐ต}))) โ (๐ฅ ยทโ ๐ต) โ (โฅโ(โฅโ{๐ต}))) | |
44 | 40, 42, 43 | mp3an13 1453 | . . . 4 โข (๐ฅ โ โ โ (๐ฅ ยทโ ๐ต) โ (โฅโ(โฅโ{๐ต}))) |
45 | eleq1 2826 | . . . 4 โข (๐ด = (๐ฅ ยทโ ๐ต) โ (๐ด โ (โฅโ(โฅโ{๐ต})) โ (๐ฅ ยทโ ๐ต) โ (โฅโ(โฅโ{๐ต})))) | |
46 | 44, 45 | syl5ibrcom 247 | . . 3 โข (๐ฅ โ โ โ (๐ด = (๐ฅ ยทโ ๐ต) โ ๐ด โ (โฅโ(โฅโ{๐ต})))) |
47 | 46 | rexlimiv 3144 | . 2 โข (โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต) โ ๐ด โ (โฅโ(โฅโ{๐ต}))) |
48 | 35, 47 | impbii 208 | 1 โข (๐ด โ (โฅโ(โฅโ{๐ต})) โ โ๐ฅ โ โ ๐ด = (๐ฅ ยทโ ๐ต)) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โ wb 205 = wceq 1542 โ wcel 2107 โ wne 2942 โwrex 3072 โ wss 3909 {csn 4585 โcfv 6492 (class class class)co 7350 โcc 10983 0cc0 10985 / cdiv 11746 โchba 29666 ยทโ csm 29668 ยทih csp 29669 0โc0v 29671 Sโ csh 29675 Cโ cch 29676 โฅcort 29677 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-rep 5241 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7663 ax-inf2 9511 ax-cc 10305 ax-cnex 11041 ax-resscn 11042 ax-1cn 11043 ax-icn 11044 ax-addcl 11045 ax-addrcl 11046 ax-mulcl 11047 ax-mulrcl 11048 ax-mulcom 11049 ax-addass 11050 ax-mulass 11051 ax-distr 11052 ax-i2m1 11053 ax-1ne0 11054 ax-1rid 11055 ax-rnegex 11056 ax-rrecex 11057 ax-cnre 11058 ax-pre-lttri 11059 ax-pre-lttrn 11060 ax-pre-ltadd 11061 ax-pre-mulgt0 11062 ax-pre-sup 11063 ax-addf 11064 ax-mulf 11065 ax-hilex 29746 ax-hfvadd 29747 ax-hvcom 29748 ax-hvass 29749 ax-hv0cl 29750 ax-hvaddid 29751 ax-hfvmul 29752 ax-hvmulid 29753 ax-hvmulass 29754 ax-hvdistr1 29755 ax-hvdistr2 29756 ax-hvmul0 29757 ax-hfi 29826 ax-his1 29829 ax-his2 29830 ax-his3 29831 ax-his4 29832 ax-hcompl 29949 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-rmo 3352 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-pss 3928 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4865 df-int 4907 df-iun 4955 df-iin 4956 df-br 5105 df-opab 5167 df-mpt 5188 df-tr 5222 df-id 5529 df-eprel 5535 df-po 5543 df-so 5544 df-fr 5586 df-se 5587 df-we 5588 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6250 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6444 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7306 df-ov 7353 df-oprab 7354 df-mpo 7355 df-of 7608 df-om 7794 df-1st 7912 df-2nd 7913 df-supp 8061 df-frecs 8180 df-wrecs 8211 df-recs 8285 df-rdg 8324 df-1o 8380 df-2o 8381 df-oadd 8384 df-omul 8385 df-er 8582 df-map 8701 df-pm 8702 df-ixp 8770 df-en 8818 df-dom 8819 df-sdom 8820 df-fin 8821 df-fsupp 9240 df-fi 9281 df-sup 9312 df-inf 9313 df-oi 9380 df-card 9809 df-acn 9812 df-pnf 11125 df-mnf 11126 df-xr 11127 df-ltxr 11128 df-le 11129 df-sub 11321 df-neg 11322 df-div 11747 df-nn 12088 df-2 12150 df-3 12151 df-4 12152 df-5 12153 df-6 12154 df-7 12155 df-8 12156 df-9 12157 df-n0 12348 df-z 12434 df-dec 12553 df-uz 12698 df-q 12804 df-rp 12846 df-xneg 12963 df-xadd 12964 df-xmul 12965 df-ioo 13198 df-ico 13200 df-icc 13201 df-fz 13355 df-fzo 13498 df-fl 13627 df-seq 13837 df-exp 13898 df-hash 14160 df-cj 14919 df-re 14920 df-im 14921 df-sqrt 15055 df-abs 15056 df-clim 15306 df-rlim 15307 df-sum 15507 df-struct 16955 df-sets 16972 df-slot 16990 df-ndx 17002 df-base 17020 df-ress 17049 df-plusg 17082 df-mulr 17083 df-starv 17084 df-sca 17085 df-vsca 17086 df-ip 17087 df-tset 17088 df-ple 17089 df-ds 17091 df-unif 17092 df-hom 17093 df-cco 17094 df-rest 17240 df-topn 17241 df-0g 17259 df-gsum 17260 df-topgen 17261 df-pt 17262 df-prds 17265 df-xrs 17320 df-qtop 17325 df-imas 17326 df-xps 17328 df-mre 17402 df-mrc 17403 df-acs 17405 df-mgm 18433 df-sgrp 18482 df-mnd 18493 df-submnd 18538 df-mulg 18808 df-cntz 19032 df-cmn 19499 df-psmet 20717 df-xmet 20718 df-met 20719 df-bl 20720 df-mopn 20721 df-fbas 20722 df-fg 20723 df-cnfld 20726 df-top 22171 df-topon 22188 df-topsp 22210 df-bases 22224 df-cld 22298 df-ntr 22299 df-cls 22300 df-nei 22377 df-cn 22506 df-cnp 22507 df-lm 22508 df-haus 22594 df-tx 22841 df-hmeo 23034 df-fil 23125 df-fm 23217 df-flim 23218 df-flf 23219 df-xms 23601 df-ms 23602 df-tms 23603 df-cfil 24547 df-cau 24548 df-cmet 24549 df-grpo 29240 df-gid 29241 df-ginv 29242 df-gdiv 29243 df-ablo 29292 df-vc 29306 df-nv 29339 df-va 29342 df-ba 29343 df-sm 29344 df-0v 29345 df-vs 29346 df-nmcv 29347 df-ims 29348 df-dip 29448 df-ssp 29469 df-ph 29560 df-cbn 29610 df-hnorm 29715 df-hba 29716 df-hvsub 29718 df-hlim 29719 df-hcau 29720 df-sh 29954 df-ch 29968 df-oc 29999 df-ch0 30000 |
This theorem is referenced by: h1de2ci 30303 |
Copyright terms: Public domain | W3C validator |