Step | Hyp | Ref
| Expression |
1 | | reex 11143 |
. . . . 5
β’ β
β V |
2 | 1 | a1i 11 |
. . . 4
β’ ((π β§ π΄ = 0) β β β
V) |
3 | | i1fmulc.2 |
. . . . . 6
β’ (π β πΉ β dom
β«1) |
4 | | i1ff 25043 |
. . . . . 6
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β πΉ:ββΆβ) |
6 | 5 | adantr 482 |
. . . 4
β’ ((π β§ π΄ = 0) β πΉ:ββΆβ) |
7 | | i1fmulc.3 |
. . . . 5
β’ (π β π΄ β β) |
8 | 7 | adantr 482 |
. . . 4
β’ ((π β§ π΄ = 0) β π΄ β β) |
9 | | 0red 11159 |
. . . 4
β’ ((π β§ π΄ = 0) β 0 β
β) |
10 | | simplr 768 |
. . . . . 6
β’ (((π β§ π΄ = 0) β§ π₯ β β) β π΄ = 0) |
11 | 10 | oveq1d 7373 |
. . . . 5
β’ (((π β§ π΄ = 0) β§ π₯ β β) β (π΄ Β· π₯) = (0 Β· π₯)) |
12 | | mul02lem2 11333 |
. . . . . 6
β’ (π₯ β β β (0
Β· π₯) =
0) |
13 | 12 | adantl 483 |
. . . . 5
β’ (((π β§ π΄ = 0) β§ π₯ β β) β (0 Β· π₯) = 0) |
14 | 11, 13 | eqtrd 2777 |
. . . 4
β’ (((π β§ π΄ = 0) β§ π₯ β β) β (π΄ Β· π₯) = 0) |
15 | 2, 6, 8, 9, 14 | caofid2 7652 |
. . 3
β’ ((π β§ π΄ = 0) β ((β Γ {π΄}) βf Β·
πΉ) = (β Γ
{0})) |
16 | | i1f0 25054 |
. . 3
β’ (β
Γ {0}) β dom β«1 |
17 | 15, 16 | eqeltrdi 2846 |
. 2
β’ ((π β§ π΄ = 0) β ((β Γ {π΄}) βf Β·
πΉ) β dom
β«1) |
18 | | remulcl 11137 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
19 | 18 | adantl 483 |
. . . . 5
β’ ((π β§ (π₯ β β β§ π¦ β β)) β (π₯ Β· π¦) β β) |
20 | | fconst6g 6732 |
. . . . . 6
β’ (π΄ β β β (β
Γ {π΄}):ββΆβ) |
21 | 7, 20 | syl 17 |
. . . . 5
β’ (π β (β Γ {π΄}):ββΆβ) |
22 | 1 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
23 | | inidm 4179 |
. . . . 5
β’ (β
β© β) = β |
24 | 19, 21, 5, 22, 22, 23 | off 7636 |
. . . 4
β’ (π β ((β Γ {π΄}) βf Β·
πΉ):ββΆβ) |
25 | 24 | adantr 482 |
. . 3
β’ ((π β§ π΄ β 0) β ((β Γ {π΄}) βf Β·
πΉ):ββΆβ) |
26 | | i1frn 25044 |
. . . . . . 7
β’ (πΉ β dom β«1
β ran πΉ β
Fin) |
27 | 3, 26 | syl 17 |
. . . . . 6
β’ (π β ran πΉ β Fin) |
28 | | ovex 7391 |
. . . . . . . 8
β’ (π΄ Β· π¦) β V |
29 | | eqid 2737 |
. . . . . . . 8
β’ (π¦ β ran πΉ β¦ (π΄ Β· π¦)) = (π¦ β ran πΉ β¦ (π΄ Β· π¦)) |
30 | 28, 29 | fnmpti 6645 |
. . . . . . 7
β’ (π¦ β ran πΉ β¦ (π΄ Β· π¦)) Fn ran πΉ |
31 | | dffn4 6763 |
. . . . . . 7
β’ ((π¦ β ran πΉ β¦ (π΄ Β· π¦)) Fn ran πΉ β (π¦ β ran πΉ β¦ (π΄ Β· π¦)):ran πΉβontoβran (π¦ β ran πΉ β¦ (π΄ Β· π¦))) |
32 | 30, 31 | mpbi 229 |
. . . . . 6
β’ (π¦ β ran πΉ β¦ (π΄ Β· π¦)):ran πΉβontoβran (π¦ β ran πΉ β¦ (π΄ Β· π¦)) |
33 | | fofi 9283 |
. . . . . 6
β’ ((ran
πΉ β Fin β§ (π¦ β ran πΉ β¦ (π΄ Β· π¦)):ran πΉβontoβran (π¦ β ran πΉ β¦ (π΄ Β· π¦))) β ran (π¦ β ran πΉ β¦ (π΄ Β· π¦)) β Fin) |
34 | 27, 32, 33 | sylancl 587 |
. . . . 5
β’ (π β ran (π¦ β ran πΉ β¦ (π΄ Β· π¦)) β Fin) |
35 | | id 22 |
. . . . . . . . . . 11
β’ (π€ β ran πΉ β π€ β ran πΉ) |
36 | | elsni 4604 |
. . . . . . . . . . . 12
β’ (π₯ β {π΄} β π₯ = π΄) |
37 | 36 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (π₯ β {π΄} β (π₯ Β· π€) = (π΄ Β· π€)) |
38 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π¦ = π€ β (π΄ Β· π¦) = (π΄ Β· π€)) |
39 | 38 | rspceeqv 3596 |
. . . . . . . . . . 11
β’ ((π€ β ran πΉ β§ (π₯ Β· π€) = (π΄ Β· π€)) β βπ¦ β ran πΉ(π₯ Β· π€) = (π΄ Β· π¦)) |
40 | 35, 37, 39 | syl2anr 598 |
. . . . . . . . . 10
β’ ((π₯ β {π΄} β§ π€ β ran πΉ) β βπ¦ β ran πΉ(π₯ Β· π€) = (π΄ Β· π¦)) |
41 | | ovex 7391 |
. . . . . . . . . . 11
β’ (π₯ Β· π€) β V |
42 | | eqeq1 2741 |
. . . . . . . . . . . 12
β’ (π§ = (π₯ Β· π€) β (π§ = (π΄ Β· π¦) β (π₯ Β· π€) = (π΄ Β· π¦))) |
43 | 42 | rexbidv 3176 |
. . . . . . . . . . 11
β’ (π§ = (π₯ Β· π€) β (βπ¦ β ran πΉ π§ = (π΄ Β· π¦) β βπ¦ β ran πΉ(π₯ Β· π€) = (π΄ Β· π¦))) |
44 | 41, 43 | elab 3631 |
. . . . . . . . . 10
β’ ((π₯ Β· π€) β {π§ β£ βπ¦ β ran πΉ π§ = (π΄ Β· π¦)} β βπ¦ β ran πΉ(π₯ Β· π€) = (π΄ Β· π¦)) |
45 | 40, 44 | sylibr 233 |
. . . . . . . . 9
β’ ((π₯ β {π΄} β§ π€ β ran πΉ) β (π₯ Β· π€) β {π§ β£ βπ¦ β ran πΉ π§ = (π΄ Β· π¦)}) |
46 | 45 | adantl 483 |
. . . . . . . 8
β’ ((π β§ (π₯ β {π΄} β§ π€ β ran πΉ)) β (π₯ Β· π€) β {π§ β£ βπ¦ β ran πΉ π§ = (π΄ Β· π¦)}) |
47 | | fconstg 6730 |
. . . . . . . . 9
β’ (π΄ β β β (β
Γ {π΄}):ββΆ{π΄}) |
48 | 7, 47 | syl 17 |
. . . . . . . 8
β’ (π β (β Γ {π΄}):ββΆ{π΄}) |
49 | 5 | ffnd 6670 |
. . . . . . . . 9
β’ (π β πΉ Fn β) |
50 | | dffn3 6682 |
. . . . . . . . 9
β’ (πΉ Fn β β πΉ:ββΆran πΉ) |
51 | 49, 50 | sylib 217 |
. . . . . . . 8
β’ (π β πΉ:ββΆran πΉ) |
52 | 46, 48, 51, 22, 22, 23 | off 7636 |
. . . . . . 7
β’ (π β ((β Γ {π΄}) βf Β·
πΉ):ββΆ{π§ β£ βπ¦ β ran πΉ π§ = (π΄ Β· π¦)}) |
53 | 52 | frnd 6677 |
. . . . . 6
β’ (π β ran ((β Γ
{π΄}) βf
Β· πΉ) β {π§ β£ βπ¦ β ran πΉ π§ = (π΄ Β· π¦)}) |
54 | 29 | rnmpt 5911 |
. . . . . 6
β’ ran
(π¦ β ran πΉ β¦ (π΄ Β· π¦)) = {π§ β£ βπ¦ β ran πΉ π§ = (π΄ Β· π¦)} |
55 | 53, 54 | sseqtrrdi 3996 |
. . . . 5
β’ (π β ran ((β Γ
{π΄}) βf
Β· πΉ) β ran
(π¦ β ran πΉ β¦ (π΄ Β· π¦))) |
56 | 34, 55 | ssfid 9212 |
. . . 4
β’ (π β ran ((β Γ
{π΄}) βf
Β· πΉ) β
Fin) |
57 | 56 | adantr 482 |
. . 3
β’ ((π β§ π΄ β 0) β ran ((β Γ {π΄}) βf Β·
πΉ) β
Fin) |
58 | 24 | frnd 6677 |
. . . . . . . 8
β’ (π β ran ((β Γ
{π΄}) βf
Β· πΉ) β
β) |
59 | 58 | ssdifssd 4103 |
. . . . . . 7
β’ (π β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β β) |
60 | 59 | adantr 482 |
. . . . . 6
β’ ((π β§ π΄ β 0) β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β β) |
61 | 60 | sselda 3945 |
. . . . 5
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π¦ β
β) |
62 | 3, 7 | i1fmulclem 25070 |
. . . . 5
β’ (((π β§ π΄ β 0) β§ π¦ β β) β (β‘((β Γ {π΄}) βf Β· πΉ) β {π¦}) = (β‘πΉ β {(π¦ / π΄)})) |
63 | 61, 62 | syldan 592 |
. . . 4
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(β‘((β Γ {π΄}) βf Β· πΉ) β {π¦}) = (β‘πΉ β {(π¦ / π΄)})) |
64 | | i1fima 25045 |
. . . . . 6
β’ (πΉ β dom β«1
β (β‘πΉ β {(π¦ / π΄)}) β dom vol) |
65 | 3, 64 | syl 17 |
. . . . 5
β’ (π β (β‘πΉ β {(π¦ / π΄)}) β dom vol) |
66 | 65 | ad2antrr 725 |
. . . 4
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(β‘πΉ β {(π¦ / π΄)}) β dom vol) |
67 | 63, 66 | eqeltrd 2838 |
. . 3
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(β‘((β Γ {π΄}) βf Β· πΉ) β {π¦}) β dom vol) |
68 | 63 | fveq2d 6847 |
. . . 4
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(volβ(β‘((β Γ {π΄}) βf Β·
πΉ) β {π¦})) = (volβ(β‘πΉ β {(π¦ / π΄)}))) |
69 | 3 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
πΉ β dom
β«1) |
70 | 7 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π΄ β
β) |
71 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π΄ β 0) |
72 | 61, 70, 71 | redivcld 11984 |
. . . . . 6
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π¦ / π΄) β β) |
73 | 61 | recnd 11184 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π¦ β
β) |
74 | 70 | recnd 11184 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π΄ β
β) |
75 | | eldifsni 4751 |
. . . . . . . 8
β’ (π¦ β (ran ((β Γ
{π΄}) βf
Β· πΉ) β {0})
β π¦ β
0) |
76 | 75 | adantl 483 |
. . . . . . 7
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
π¦ β 0) |
77 | 73, 74, 76, 71 | divne0d 11948 |
. . . . . 6
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π¦ / π΄) β 0) |
78 | | eldifsn 4748 |
. . . . . 6
β’ ((π¦ / π΄) β (β β {0}) β
((π¦ / π΄) β β β§ (π¦ / π΄) β 0)) |
79 | 72, 77, 78 | sylanbrc 584 |
. . . . 5
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(π¦ / π΄) β (β β
{0})) |
80 | | i1fima2sn 25047 |
. . . . 5
β’ ((πΉ β dom β«1
β§ (π¦ / π΄) β (β β {0}))
β (volβ(β‘πΉ β {(π¦ / π΄)})) β β) |
81 | 69, 79, 80 | syl2anc 585 |
. . . 4
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(volβ(β‘πΉ β {(π¦ / π΄)})) β β) |
82 | 68, 81 | eqeltrd 2838 |
. . 3
β’ (((π β§ π΄ β 0) β§ π¦ β (ran ((β Γ {π΄}) βf Β·
πΉ) β {0})) β
(volβ(β‘((β Γ {π΄}) βf Β·
πΉ) β {π¦})) β
β) |
83 | 25, 57, 67, 82 | i1fd 25048 |
. 2
β’ ((π β§ π΄ β 0) β ((β Γ {π΄}) βf Β·
πΉ) β dom
β«1) |
84 | 17, 83 | pm2.61dane 3033 |
1
β’ (π β ((β Γ {π΄}) βf Β·
πΉ) β dom
β«1) |