Step | Hyp | Ref
| Expression |
1 | | flcidc.f |
. . . . . . . . 9
โข (๐ โ ๐น = (๐ โ ๐ โฆ if(๐ = ๐พ, 1, 0))) |
2 | 1 | fveq1d 6845 |
. . . . . . . 8
โข (๐ โ (๐นโ๐) = ((๐ โ ๐ โฆ if(๐ = ๐พ, 1, 0))โ๐)) |
3 | 2 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ {๐พ}) โ (๐นโ๐) = ((๐ โ ๐ โฆ if(๐ = ๐พ, 1, 0))โ๐)) |
4 | | flcidc.k |
. . . . . . . . . 10
โข (๐ โ ๐พ โ ๐) |
5 | 4 | snssd 4770 |
. . . . . . . . 9
โข (๐ โ {๐พ} โ ๐) |
6 | 5 | sselda 3945 |
. . . . . . . 8
โข ((๐ โง ๐ โ {๐พ}) โ ๐ โ ๐) |
7 | | eqeq1 2737 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐ = ๐พ โ ๐ = ๐พ)) |
8 | 7 | ifbid 4510 |
. . . . . . . . 9
โข (๐ = ๐ โ if(๐ = ๐พ, 1, 0) = if(๐ = ๐พ, 1, 0)) |
9 | | eqid 2733 |
. . . . . . . . 9
โข (๐ โ ๐ โฆ if(๐ = ๐พ, 1, 0)) = (๐ โ ๐ โฆ if(๐ = ๐พ, 1, 0)) |
10 | | 1ex 11156 |
. . . . . . . . . 10
โข 1 โ
V |
11 | | c0ex 11154 |
. . . . . . . . . 10
โข 0 โ
V |
12 | 10, 11 | ifex 4537 |
. . . . . . . . 9
โข if(๐ = ๐พ, 1, 0) โ V |
13 | 8, 9, 12 | fvmpt 6949 |
. . . . . . . 8
โข (๐ โ ๐ โ ((๐ โ ๐ โฆ if(๐ = ๐พ, 1, 0))โ๐) = if(๐ = ๐พ, 1, 0)) |
14 | 6, 13 | syl 17 |
. . . . . . 7
โข ((๐ โง ๐ โ {๐พ}) โ ((๐ โ ๐ โฆ if(๐ = ๐พ, 1, 0))โ๐) = if(๐ = ๐พ, 1, 0)) |
15 | 3, 14 | eqtrd 2773 |
. . . . . 6
โข ((๐ โง ๐ โ {๐พ}) โ (๐นโ๐) = if(๐ = ๐พ, 1, 0)) |
16 | | elsni 4604 |
. . . . . . . 8
โข (๐ โ {๐พ} โ ๐ = ๐พ) |
17 | 16 | iftrued 4495 |
. . . . . . 7
โข (๐ โ {๐พ} โ if(๐ = ๐พ, 1, 0) = 1) |
18 | 17 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ {๐พ}) โ if(๐ = ๐พ, 1, 0) = 1) |
19 | 15, 18 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ๐ โ {๐พ}) โ (๐นโ๐) = 1) |
20 | 19 | oveq1d 7373 |
. . . 4
โข ((๐ โง ๐ โ {๐พ}) โ ((๐นโ๐) ยท ๐ต) = (1 ยท ๐ต)) |
21 | | flcidc.b |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ ๐ต โ โ) |
22 | 6, 21 | syldan 592 |
. . . . 5
โข ((๐ โง ๐ โ {๐พ}) โ ๐ต โ โ) |
23 | 22 | mulid2d 11178 |
. . . 4
โข ((๐ โง ๐ โ {๐พ}) โ (1 ยท ๐ต) = ๐ต) |
24 | 20, 23 | eqtrd 2773 |
. . 3
โข ((๐ โง ๐ โ {๐พ}) โ ((๐นโ๐) ยท ๐ต) = ๐ต) |
25 | 24 | sumeq2dv 15593 |
. 2
โข (๐ โ ฮฃ๐ โ {๐พ} ((๐นโ๐) ยท ๐ต) = ฮฃ๐ โ {๐พ}๐ต) |
26 | | ax-1cn 11114 |
. . . . . 6
โข 1 โ
โ |
27 | | 0cn 11152 |
. . . . . 6
โข 0 โ
โ |
28 | 26, 27 | ifcli 4534 |
. . . . 5
โข if(๐ = ๐พ, 1, 0) โ โ |
29 | 15, 28 | eqeltrdi 2842 |
. . . 4
โข ((๐ โง ๐ โ {๐พ}) โ (๐นโ๐) โ โ) |
30 | 29, 22 | mulcld 11180 |
. . 3
โข ((๐ โง ๐ โ {๐พ}) โ ((๐นโ๐) ยท ๐ต) โ โ) |
31 | 2 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐ โ {๐พ})) โ (๐นโ๐) = ((๐ โ ๐ โฆ if(๐ = ๐พ, 1, 0))โ๐)) |
32 | | eldifi 4087 |
. . . . . . . . 9
โข (๐ โ (๐ โ {๐พ}) โ ๐ โ ๐) |
33 | 32 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ โ (๐ โ {๐พ})) โ ๐ โ ๐) |
34 | 33, 13 | syl 17 |
. . . . . . 7
โข ((๐ โง ๐ โ (๐ โ {๐พ})) โ ((๐ โ ๐ โฆ if(๐ = ๐พ, 1, 0))โ๐) = if(๐ = ๐พ, 1, 0)) |
35 | 31, 34 | eqtrd 2773 |
. . . . . 6
โข ((๐ โง ๐ โ (๐ โ {๐พ})) โ (๐นโ๐) = if(๐ = ๐พ, 1, 0)) |
36 | | eldifn 4088 |
. . . . . . . . 9
โข (๐ โ (๐ โ {๐พ}) โ ยฌ ๐ โ {๐พ}) |
37 | | velsn 4603 |
. . . . . . . . 9
โข (๐ โ {๐พ} โ ๐ = ๐พ) |
38 | 36, 37 | sylnib 328 |
. . . . . . . 8
โข (๐ โ (๐ โ {๐พ}) โ ยฌ ๐ = ๐พ) |
39 | 38 | iffalsed 4498 |
. . . . . . 7
โข (๐ โ (๐ โ {๐พ}) โ if(๐ = ๐พ, 1, 0) = 0) |
40 | 39 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ (๐ โ {๐พ})) โ if(๐ = ๐พ, 1, 0) = 0) |
41 | 35, 40 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ๐ โ (๐ โ {๐พ})) โ (๐นโ๐) = 0) |
42 | 41 | oveq1d 7373 |
. . . 4
โข ((๐ โง ๐ โ (๐ โ {๐พ})) โ ((๐นโ๐) ยท ๐ต) = (0 ยท ๐ต)) |
43 | 33, 21 | syldan 592 |
. . . . 5
โข ((๐ โง ๐ โ (๐ โ {๐พ})) โ ๐ต โ โ) |
44 | 43 | mul02d 11358 |
. . . 4
โข ((๐ โง ๐ โ (๐ โ {๐พ})) โ (0 ยท ๐ต) = 0) |
45 | 42, 44 | eqtrd 2773 |
. . 3
โข ((๐ โง ๐ โ (๐ โ {๐พ})) โ ((๐นโ๐) ยท ๐ต) = 0) |
46 | | flcidc.s |
. . 3
โข (๐ โ ๐ โ Fin) |
47 | 5, 30, 45, 46 | fsumss 15615 |
. 2
โข (๐ โ ฮฃ๐ โ {๐พ} ((๐นโ๐) ยท ๐ต) = ฮฃ๐ โ ๐ ((๐นโ๐) ยท ๐ต)) |
48 | | eleq1 2822 |
. . . . . . . 8
โข (๐ = ๐พ โ (๐ โ ๐ โ ๐พ โ ๐)) |
49 | 48 | anbi2d 630 |
. . . . . . 7
โข (๐ = ๐พ โ ((๐ โง ๐ โ ๐) โ (๐ โง ๐พ โ ๐))) |
50 | | csbeq1 3859 |
. . . . . . . 8
โข (๐ = ๐พ โ โฆ๐ / ๐โฆ๐ต = โฆ๐พ / ๐โฆ๐ต) |
51 | 50 | eleq1d 2819 |
. . . . . . 7
โข (๐ = ๐พ โ (โฆ๐ / ๐โฆ๐ต โ โ โ โฆ๐พ / ๐โฆ๐ต โ โ)) |
52 | 49, 51 | imbi12d 345 |
. . . . . 6
โข (๐ = ๐พ โ (((๐ โง ๐ โ ๐) โ โฆ๐ / ๐โฆ๐ต โ โ) โ ((๐ โง ๐พ โ ๐) โ โฆ๐พ / ๐โฆ๐ต โ โ))) |
53 | | nfv 1918 |
. . . . . . . 8
โข
โฒ๐(๐ โง ๐ โ ๐) |
54 | | nfcsb1v 3881 |
. . . . . . . . 9
โข
โฒ๐โฆ๐ / ๐โฆ๐ต |
55 | 54 | nfel1 2920 |
. . . . . . . 8
โข
โฒ๐โฆ๐ / ๐โฆ๐ต โ โ |
56 | 53, 55 | nfim 1900 |
. . . . . . 7
โข
โฒ๐((๐ โง ๐ โ ๐) โ โฆ๐ / ๐โฆ๐ต โ โ) |
57 | | eleq1 2822 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ ๐ โ ๐ โ ๐)) |
58 | 57 | anbi2d 630 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ โง ๐ โ ๐) โ (๐ โง ๐ โ ๐))) |
59 | | csbeq1a 3870 |
. . . . . . . . 9
โข (๐ = ๐ โ ๐ต = โฆ๐ / ๐โฆ๐ต) |
60 | 59 | eleq1d 2819 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ต โ โ โ โฆ๐ / ๐โฆ๐ต โ โ)) |
61 | 58, 60 | imbi12d 345 |
. . . . . . 7
โข (๐ = ๐ โ (((๐ โง ๐ โ ๐) โ ๐ต โ โ) โ ((๐ โง ๐ โ ๐) โ โฆ๐ / ๐โฆ๐ต โ โ))) |
62 | 56, 61, 21 | chvarfv 2234 |
. . . . . 6
โข ((๐ โง ๐ โ ๐) โ โฆ๐ / ๐โฆ๐ต โ โ) |
63 | 52, 62 | vtoclg 3524 |
. . . . 5
โข (๐พ โ ๐ โ ((๐ โง ๐พ โ ๐) โ โฆ๐พ / ๐โฆ๐ต โ โ)) |
64 | 63 | anabsi7 670 |
. . . 4
โข ((๐ โง ๐พ โ ๐) โ โฆ๐พ / ๐โฆ๐ต โ โ) |
65 | 4, 64 | mpdan 686 |
. . 3
โข (๐ โ โฆ๐พ / ๐โฆ๐ต โ โ) |
66 | | sumsns 15640 |
. . 3
โข ((๐พ โ ๐ โง โฆ๐พ / ๐โฆ๐ต โ โ) โ ฮฃ๐ โ {๐พ}๐ต = โฆ๐พ / ๐โฆ๐ต) |
67 | 4, 65, 66 | syl2anc 585 |
. 2
โข (๐ โ ฮฃ๐ โ {๐พ}๐ต = โฆ๐พ / ๐โฆ๐ต) |
68 | 25, 47, 67 | 3eqtr3d 2781 |
1
โข (๐ โ ฮฃ๐ โ ๐ ((๐นโ๐) ยท ๐ต) = โฆ๐พ / ๐โฆ๐ต) |