![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fprodsplit1f | GIF version |
Description: Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Ref | Expression |
---|---|
fprodsplit1f.kph | โข โฒ๐๐ |
fprodsplit1f.fk | โข (๐ โ โฒ๐๐ท) |
fprodsplit1f.a | โข (๐ โ ๐ด โ Fin) |
fprodsplit1f.b | โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) |
fprodsplit1f.c | โข (๐ โ ๐ถ โ ๐ด) |
fprodsplit1f.d | โข ((๐ โง ๐ = ๐ถ) โ ๐ต = ๐ท) |
Ref | Expression |
---|---|
fprodsplit1f | โข (๐ โ โ๐ โ ๐ด ๐ต = (๐ท ยท โ๐ โ (๐ด โ {๐ถ})๐ต)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fprodsplit1f.kph | . . 3 โข โฒ๐๐ | |
2 | disjdif 3510 | . . . 4 โข ({๐ถ} โฉ (๐ด โ {๐ถ})) = โ | |
3 | 2 | a1i 9 | . . 3 โข (๐ โ ({๐ถ} โฉ (๐ด โ {๐ถ})) = โ ) |
4 | fprodsplit1f.a | . . . 4 โข (๐ โ ๐ด โ Fin) | |
5 | fprodsplit1f.c | . . . . 5 โข (๐ โ ๐ถ โ ๐ด) | |
6 | snfig 6833 | . . . . 5 โข (๐ถ โ ๐ด โ {๐ถ} โ Fin) | |
7 | 5, 6 | syl 14 | . . . 4 โข (๐ โ {๐ถ} โ Fin) |
8 | 5 | snssd 3752 | . . . 4 โข (๐ โ {๐ถ} โ ๐ด) |
9 | undiffi 6943 | . . . 4 โข ((๐ด โ Fin โง {๐ถ} โ Fin โง {๐ถ} โ ๐ด) โ ๐ด = ({๐ถ} โช (๐ด โ {๐ถ}))) | |
10 | 4, 7, 8, 9 | syl3anc 1249 | . . 3 โข (๐ โ ๐ด = ({๐ถ} โช (๐ด โ {๐ถ}))) |
11 | fprodsplit1f.b | . . 3 โข ((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) | |
12 | 1, 3, 10, 4, 11 | fprodsplitf 11660 | . 2 โข (๐ โ โ๐ โ ๐ด ๐ต = (โ๐ โ {๐ถ}๐ต ยท โ๐ โ (๐ด โ {๐ถ})๐ต)) |
13 | 5 | ancli 323 | . . . . . 6 โข (๐ โ (๐ โง ๐ถ โ ๐ด)) |
14 | nfv 1539 | . . . . . . . . 9 โข โฒ๐ ๐ถ โ ๐ด | |
15 | 1, 14 | nfan 1576 | . . . . . . . 8 โข โฒ๐(๐ โง ๐ถ โ ๐ด) |
16 | nfcsb1v 3105 | . . . . . . . . 9 โข โฒ๐โฆ๐ถ / ๐โฆ๐ต | |
17 | 16 | nfel1 2343 | . . . . . . . 8 โข โฒ๐โฆ๐ถ / ๐โฆ๐ต โ โ |
18 | 15, 17 | nfim 1583 | . . . . . . 7 โข โฒ๐((๐ โง ๐ถ โ ๐ด) โ โฆ๐ถ / ๐โฆ๐ต โ โ) |
19 | eleq1 2252 | . . . . . . . . 9 โข (๐ = ๐ถ โ (๐ โ ๐ด โ ๐ถ โ ๐ด)) | |
20 | 19 | anbi2d 464 | . . . . . . . 8 โข (๐ = ๐ถ โ ((๐ โง ๐ โ ๐ด) โ (๐ โง ๐ถ โ ๐ด))) |
21 | csbeq1a 3081 | . . . . . . . . 9 โข (๐ = ๐ถ โ ๐ต = โฆ๐ถ / ๐โฆ๐ต) | |
22 | 21 | eleq1d 2258 | . . . . . . . 8 โข (๐ = ๐ถ โ (๐ต โ โ โ โฆ๐ถ / ๐โฆ๐ต โ โ)) |
23 | 20, 22 | imbi12d 234 | . . . . . . 7 โข (๐ = ๐ถ โ (((๐ โง ๐ โ ๐ด) โ ๐ต โ โ) โ ((๐ โง ๐ถ โ ๐ด) โ โฆ๐ถ / ๐โฆ๐ต โ โ))) |
24 | 18, 23, 11 | vtoclg1f 2811 | . . . . . 6 โข (๐ถ โ ๐ด โ ((๐ โง ๐ถ โ ๐ด) โ โฆ๐ถ / ๐โฆ๐ต โ โ)) |
25 | 5, 13, 24 | sylc 62 | . . . . 5 โข (๐ โ โฆ๐ถ / ๐โฆ๐ต โ โ) |
26 | prodsns 11631 | . . . . 5 โข ((๐ถ โ ๐ด โง โฆ๐ถ / ๐โฆ๐ต โ โ) โ โ๐ โ {๐ถ}๐ต = โฆ๐ถ / ๐โฆ๐ต) | |
27 | 5, 25, 26 | syl2anc 411 | . . . 4 โข (๐ โ โ๐ โ {๐ถ}๐ต = โฆ๐ถ / ๐โฆ๐ต) |
28 | fprodsplit1f.fk | . . . . 5 โข (๐ โ โฒ๐๐ท) | |
29 | fprodsplit1f.d | . . . . 5 โข ((๐ โง ๐ = ๐ถ) โ ๐ต = ๐ท) | |
30 | 1, 28, 5, 29 | csbiedf 3112 | . . . 4 โข (๐ โ โฆ๐ถ / ๐โฆ๐ต = ๐ท) |
31 | 27, 30 | eqtrd 2222 | . . 3 โข (๐ โ โ๐ โ {๐ถ}๐ต = ๐ท) |
32 | 31 | oveq1d 5907 | . 2 โข (๐ โ (โ๐ โ {๐ถ}๐ต ยท โ๐ โ (๐ด โ {๐ถ})๐ต) = (๐ท ยท โ๐ โ (๐ด โ {๐ถ})๐ต)) |
33 | 12, 32 | eqtrd 2222 | 1 โข (๐ โ โ๐ โ ๐ด ๐ต = (๐ท ยท โ๐ โ (๐ด โ {๐ถ})๐ต)) |
Colors of variables: wff set class |
Syntax hints: โ wi 4 โง wa 104 = wceq 1364 โฒwnf 1471 โ wcel 2160 โฒwnfc 2319 โฆcsb 3072 โ cdif 3141 โช cun 3142 โฉ cin 3143 โ wss 3144 โ c0 3437 {csn 3607 (class class class)co 5892 Fincfn 6759 โcc 7829 ยท cmul 7836 โcprod 11578 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4189 ax-pr 4224 ax-un 4448 ax-setind 4551 ax-iinf 4602 ax-cnex 7922 ax-resscn 7923 ax-1cn 7924 ax-1re 7925 ax-icn 7926 ax-addcl 7927 ax-addrcl 7928 ax-mulcl 7929 ax-mulrcl 7930 ax-addcom 7931 ax-mulcom 7932 ax-addass 7933 ax-mulass 7934 ax-distr 7935 ax-i2m1 7936 ax-0lt1 7937 ax-1rid 7938 ax-0id 7939 ax-rnegex 7940 ax-precex 7941 ax-cnre 7942 ax-pre-ltirr 7943 ax-pre-ltwlin 7944 ax-pre-lttrn 7945 ax-pre-apti 7946 ax-pre-ltadd 7947 ax-pre-mulgt0 7948 ax-pre-mulext 7949 ax-arch 7950 ax-caucvg 7951 |
This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4308 df-po 4311 df-iso 4312 df-iord 4381 df-on 4383 df-ilim 4384 df-suc 4386 df-iom 4605 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-rn 4652 df-res 4653 df-ima 4654 df-iota 5193 df-fun 5234 df-fn 5235 df-f 5236 df-f1 5237 df-fo 5238 df-f1o 5239 df-fv 5240 df-isom 5241 df-riota 5848 df-ov 5895 df-oprab 5896 df-mpo 5897 df-1st 6160 df-2nd 6161 df-recs 6325 df-irdg 6390 df-frec 6411 df-1o 6436 df-oadd 6440 df-er 6554 df-en 6760 df-dom 6761 df-fin 6762 df-pnf 8014 df-mnf 8015 df-xr 8016 df-ltxr 8017 df-le 8018 df-sub 8150 df-neg 8151 df-reap 8552 df-ap 8559 df-div 8650 df-inn 8940 df-2 8998 df-3 8999 df-4 9000 df-n0 9197 df-z 9274 df-uz 9549 df-q 9640 df-rp 9674 df-fz 10029 df-fzo 10163 df-seqfrec 10466 df-exp 10540 df-ihash 10776 df-cj 10871 df-re 10872 df-im 10873 df-rsqrt 11027 df-abs 11028 df-clim 11307 df-proddc 11579 |
This theorem is referenced by: fprodeq0g 11666 |
Copyright terms: Public domain | W3C validator |