Step | Hyp | Ref
| Expression |
1 | | i1fadd.1 |
. . . . 5
β’ (π β πΉ β dom
β«1) |
2 | | i1fadd.2 |
. . . . 5
β’ (π β πΊ β dom
β«1) |
3 | 1, 2 | i1fadd 25075 |
. . . 4
β’ (π β (πΉ βf + πΊ) β dom
β«1) |
4 | | i1frn 25057 |
. . . . . . . 8
β’ (πΉ β dom β«1
β ran πΉ β
Fin) |
5 | 1, 4 | syl 17 |
. . . . . . 7
β’ (π β ran πΉ β Fin) |
6 | | i1frn 25057 |
. . . . . . . 8
β’ (πΊ β dom β«1
β ran πΊ β
Fin) |
7 | 2, 6 | syl 17 |
. . . . . . 7
β’ (π β ran πΊ β Fin) |
8 | | xpfi 9268 |
. . . . . . 7
β’ ((ran
πΉ β Fin β§ ran
πΊ β Fin) β (ran
πΉ Γ ran πΊ) β Fin) |
9 | 5, 7, 8 | syl2anc 585 |
. . . . . 6
β’ (π β (ran πΉ Γ ran πΊ) β Fin) |
10 | | ax-addf 11137 |
. . . . . . . . . 10
β’ +
:(β Γ β)βΆβ |
11 | | ffn 6673 |
. . . . . . . . . 10
β’ ( +
:(β Γ β)βΆβ β + Fn (β Γ
β)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
β’ + Fn
(β Γ β) |
13 | | i1ff 25056 |
. . . . . . . . . . . . 13
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
14 | 1, 13 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΉ:ββΆβ) |
15 | 14 | frnd 6681 |
. . . . . . . . . . 11
β’ (π β ran πΉ β β) |
16 | | ax-resscn 11115 |
. . . . . . . . . . 11
β’ β
β β |
17 | 15, 16 | sstrdi 3961 |
. . . . . . . . . 10
β’ (π β ran πΉ β β) |
18 | | i1ff 25056 |
. . . . . . . . . . . . 13
β’ (πΊ β dom β«1
β πΊ:ββΆβ) |
19 | 2, 18 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΊ:ββΆβ) |
20 | 19 | frnd 6681 |
. . . . . . . . . . 11
β’ (π β ran πΊ β β) |
21 | 20, 16 | sstrdi 3961 |
. . . . . . . . . 10
β’ (π β ran πΊ β β) |
22 | | xpss12 5653 |
. . . . . . . . . 10
β’ ((ran
πΉ β β β§ ran
πΊ β β) β
(ran πΉ Γ ran πΊ) β (β Γ
β)) |
23 | 17, 21, 22 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (ran πΉ Γ ran πΊ) β (β Γ
β)) |
24 | | fnssres 6629 |
. . . . . . . . 9
β’ (( + Fn
(β Γ β) β§ (ran πΉ Γ ran πΊ) β (β Γ β)) β
( + βΎ (ran πΉ Γ
ran πΊ)) Fn (ran πΉ Γ ran πΊ)) |
25 | 12, 23, 24 | sylancr 588 |
. . . . . . . 8
β’ (π β ( + βΎ (ran πΉ Γ ran πΊ)) Fn (ran πΉ Γ ran πΊ)) |
26 | | itg1add.4 |
. . . . . . . . 9
β’ π = ( + βΎ (ran πΉ Γ ran πΊ)) |
27 | 26 | fneq1i 6604 |
. . . . . . . 8
β’ (π Fn (ran πΉ Γ ran πΊ) β ( + βΎ (ran πΉ Γ ran πΊ)) Fn (ran πΉ Γ ran πΊ)) |
28 | 25, 27 | sylibr 233 |
. . . . . . 7
β’ (π β π Fn (ran πΉ Γ ran πΊ)) |
29 | | dffn4 6767 |
. . . . . . 7
β’ (π Fn (ran πΉ Γ ran πΊ) β π:(ran πΉ Γ ran πΊ)βontoβran π) |
30 | 28, 29 | sylib 217 |
. . . . . 6
β’ (π β π:(ran πΉ Γ ran πΊ)βontoβran π) |
31 | | fofi 9289 |
. . . . . 6
β’ (((ran
πΉ Γ ran πΊ) β Fin β§ π:(ran πΉ Γ ran πΊ)βontoβran π) β ran π β Fin) |
32 | 9, 30, 31 | syl2anc 585 |
. . . . 5
β’ (π β ran π β Fin) |
33 | | difss 4096 |
. . . . 5
β’ (ran
π β {0}) β ran
π |
34 | | ssfi 9124 |
. . . . 5
β’ ((ran
π β Fin β§ (ran
π β {0}) β ran
π) β (ran π β {0}) β
Fin) |
35 | 32, 33, 34 | sylancl 587 |
. . . 4
β’ (π β (ran π β {0}) β Fin) |
36 | | ffun 6676 |
. . . . . . . . . . 11
β’ ( +
:(β Γ β)βΆβ β Fun + ) |
37 | 10, 36 | ax-mp 5 |
. . . . . . . . . 10
β’ Fun
+ |
38 | 10 | fdmi 6685 |
. . . . . . . . . . 11
β’ dom + =
(β Γ β) |
39 | 23, 38 | sseqtrrdi 4000 |
. . . . . . . . . 10
β’ (π β (ran πΉ Γ ran πΊ) β dom + ) |
40 | | funfvima2 7186 |
. . . . . . . . . 10
β’ ((Fun +
β§ (ran πΉ Γ ran
πΊ) β dom + ) β
(β¨π₯, π¦β© β (ran πΉ Γ ran πΊ) β ( + ββ¨π₯, π¦β©) β ( + β (ran πΉ Γ ran πΊ)))) |
41 | 37, 39, 40 | sylancr 588 |
. . . . . . . . 9
β’ (π β (β¨π₯, π¦β© β (ran πΉ Γ ran πΊ) β ( + ββ¨π₯, π¦β©) β ( + β (ran πΉ Γ ran πΊ)))) |
42 | | opelxpi 5675 |
. . . . . . . . 9
β’ ((π₯ β ran πΉ β§ π¦ β ran πΊ) β β¨π₯, π¦β© β (ran πΉ Γ ran πΊ)) |
43 | 41, 42 | impel 507 |
. . . . . . . 8
β’ ((π β§ (π₯ β ran πΉ β§ π¦ β ran πΊ)) β ( + ββ¨π₯, π¦β©) β ( + β (ran πΉ Γ ran πΊ))) |
44 | | df-ov 7365 |
. . . . . . . 8
β’ (π₯ + π¦) = ( + ββ¨π₯, π¦β©) |
45 | 26 | rneqi 5897 |
. . . . . . . . 9
β’ ran π = ran ( + βΎ (ran πΉ Γ ran πΊ)) |
46 | | df-ima 5651 |
. . . . . . . . 9
β’ ( +
β (ran πΉ Γ ran
πΊ)) = ran ( + βΎ (ran
πΉ Γ ran πΊ)) |
47 | 45, 46 | eqtr4i 2768 |
. . . . . . . 8
β’ ran π = ( + β (ran πΉ Γ ran πΊ)) |
48 | 43, 44, 47 | 3eltr4g 2855 |
. . . . . . 7
β’ ((π β§ (π₯ β ran πΉ β§ π¦ β ran πΊ)) β (π₯ + π¦) β ran π) |
49 | 14 | ffnd 6674 |
. . . . . . . 8
β’ (π β πΉ Fn β) |
50 | | dffn3 6686 |
. . . . . . . 8
β’ (πΉ Fn β β πΉ:ββΆran πΉ) |
51 | 49, 50 | sylib 217 |
. . . . . . 7
β’ (π β πΉ:ββΆran πΉ) |
52 | 19 | ffnd 6674 |
. . . . . . . 8
β’ (π β πΊ Fn β) |
53 | | dffn3 6686 |
. . . . . . . 8
β’ (πΊ Fn β β πΊ:ββΆran πΊ) |
54 | 52, 53 | sylib 217 |
. . . . . . 7
β’ (π β πΊ:ββΆran πΊ) |
55 | | reex 11149 |
. . . . . . . 8
β’ β
β V |
56 | 55 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
57 | | inidm 4183 |
. . . . . . 7
β’ (β
β© β) = β |
58 | 48, 51, 54, 56, 56, 57 | off 7640 |
. . . . . 6
β’ (π β (πΉ βf + πΊ):ββΆran π) |
59 | 58 | frnd 6681 |
. . . . 5
β’ (π β ran (πΉ βf + πΊ) β ran π) |
60 | 59 | ssdifd 4105 |
. . . 4
β’ (π β (ran (πΉ βf + πΊ) β {0}) β (ran π β {0})) |
61 | 15 | sselda 3949 |
. . . . . . . . . 10
β’ ((π β§ π¦ β ran πΉ) β π¦ β β) |
62 | 20 | sselda 3949 |
. . . . . . . . . 10
β’ ((π β§ π§ β ran πΊ) β π§ β β) |
63 | 61, 62 | anim12dan 620 |
. . . . . . . . 9
β’ ((π β§ (π¦ β ran πΉ β§ π§ β ran πΊ)) β (π¦ β β β§ π§ β β)) |
64 | | readdcl 11141 |
. . . . . . . . 9
β’ ((π¦ β β β§ π§ β β) β (π¦ + π§) β β) |
65 | 63, 64 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π¦ β ran πΉ β§ π§ β ran πΊ)) β (π¦ + π§) β β) |
66 | 65 | ralrimivva 3198 |
. . . . . . 7
β’ (π β βπ¦ β ran πΉβπ§ β ran πΊ(π¦ + π§) β β) |
67 | | funimassov 7536 |
. . . . . . . 8
β’ ((Fun +
β§ (ran πΉ Γ ran
πΊ) β dom + ) β
(( + β (ran πΉ Γ
ran πΊ)) β β
β βπ¦ β ran
πΉβπ§ β ran πΊ(π¦ + π§) β β)) |
68 | 37, 39, 67 | sylancr 588 |
. . . . . . 7
β’ (π β (( + β (ran πΉ Γ ran πΊ)) β β β βπ¦ β ran πΉβπ§ β ran πΊ(π¦ + π§) β β)) |
69 | 66, 68 | mpbird 257 |
. . . . . 6
β’ (π β ( + β (ran πΉ Γ ran πΊ)) β β) |
70 | 47, 69 | eqsstrid 3997 |
. . . . 5
β’ (π β ran π β β) |
71 | 70 | ssdifd 4105 |
. . . 4
β’ (π β (ran π β {0}) β (β β
{0})) |
72 | | itg1val2 25064 |
. . . 4
β’ (((πΉ βf + πΊ) β dom β«1
β§ ((ran π β {0})
β Fin β§ (ran (πΉ
βf + πΊ)
β {0}) β (ran π
β {0}) β§ (ran π
β {0}) β (β β {0}))) β
(β«1β(πΉ
βf + πΊ)) =
Ξ£π€ β (ran π β {0})(π€ Β· (volβ(β‘(πΉ βf + πΊ) β {π€})))) |
73 | 3, 35, 60, 71, 72 | syl13anc 1373 |
. . 3
β’ (π β
(β«1β(πΉ
βf + πΊ)) =
Ξ£π€ β (ran π β {0})(π€ Β· (volβ(β‘(πΉ βf + πΊ) β {π€})))) |
74 | 19 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π€ β (ran π β {0})) β πΊ:ββΆβ) |
75 | 7 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π€ β (ran π β {0})) β ran πΊ β Fin) |
76 | | inss2 4194 |
. . . . . . . . 9
β’ ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§})) β (β‘πΊ β {π§}) |
77 | 76 | a1i 11 |
. . . . . . . 8
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§})) β (β‘πΊ β {π§})) |
78 | | i1fima 25058 |
. . . . . . . . . . 11
β’ (πΉ β dom β«1
β (β‘πΉ β {(π€ β π§)}) β dom vol) |
79 | 1, 78 | syl 17 |
. . . . . . . . . 10
β’ (π β (β‘πΉ β {(π€ β π§)}) β dom vol) |
80 | | i1fima 25058 |
. . . . . . . . . . 11
β’ (πΊ β dom β«1
β (β‘πΊ β {π§}) β dom vol) |
81 | 2, 80 | syl 17 |
. . . . . . . . . 10
β’ (π β (β‘πΊ β {π§}) β dom vol) |
82 | | inmbl 24922 |
. . . . . . . . . 10
β’ (((β‘πΉ β {(π€ β π§)}) β dom vol β§ (β‘πΊ β {π§}) β dom vol) β ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§})) β dom vol) |
83 | 79, 81, 82 | syl2anc 585 |
. . . . . . . . 9
β’ (π β ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§})) β dom vol) |
84 | 83 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§})) β dom vol) |
85 | 33, 70 | sstrid 3960 |
. . . . . . . . . . . . 13
β’ (π β (ran π β {0}) β
β) |
86 | 85 | sselda 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β (ran π β {0})) β π€ β β) |
87 | 86 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β π€ β β) |
88 | 62 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β π§ β β) |
89 | 87, 88 | resubcld 11590 |
. . . . . . . . . 10
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β (π€ β π§) β β) |
90 | 87 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β π€ β β) |
91 | 88 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β π§ β β) |
92 | 90, 91 | npcand 11523 |
. . . . . . . . . . . 12
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β ((π€ β π§) + π§) = π€) |
93 | | eldifsni 4755 |
. . . . . . . . . . . . 13
β’ (π€ β (ran π β {0}) β π€ β 0) |
94 | 93 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β π€ β 0) |
95 | 92, 94 | eqnetrd 3012 |
. . . . . . . . . . 11
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β ((π€ β π§) + π§) β 0) |
96 | | oveq12 7371 |
. . . . . . . . . . . . 13
β’ (((π€ β π§) = 0 β§ π§ = 0) β ((π€ β π§) + π§) = (0 + 0)) |
97 | | 00id 11337 |
. . . . . . . . . . . . 13
β’ (0 + 0) =
0 |
98 | 96, 97 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’ (((π€ β π§) = 0 β§ π§ = 0) β ((π€ β π§) + π§) = 0) |
99 | 98 | necon3ai 2969 |
. . . . . . . . . . 11
β’ (((π€ β π§) + π§) β 0 β Β¬ ((π€ β π§) = 0 β§ π§ = 0)) |
100 | 95, 99 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β Β¬ ((π€ β π§) = 0 β§ π§ = 0)) |
101 | | itg1add.3 |
. . . . . . . . . . 11
β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) |
102 | 1, 2, 101 | itg1addlem3 25078 |
. . . . . . . . . 10
β’ ((((π€ β π§) β β β§ π§ β β) β§ Β¬ ((π€ β π§) = 0 β§ π§ = 0)) β ((π€ β π§)πΌπ§) = (volβ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§})))) |
103 | 89, 88, 100, 102 | syl21anc 837 |
. . . . . . . . 9
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β ((π€ β π§)πΌπ§) = (volβ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§})))) |
104 | 1, 2, 101 | itg1addlem2 25077 |
. . . . . . . . . . 11
β’ (π β πΌ:(β Γ
β)βΆβ) |
105 | 104 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β πΌ:(β Γ
β)βΆβ) |
106 | 105, 89, 88 | fovcdmd 7531 |
. . . . . . . . 9
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β ((π€ β π§)πΌπ§) β β) |
107 | 103, 106 | eqeltrrd 2839 |
. . . . . . . 8
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β (volβ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§}))) β β) |
108 | 74, 75, 77, 84, 107 | itg1addlem1 25072 |
. . . . . . 7
β’ ((π β§ π€ β (ran π β {0})) β (volββͺ π§ β ran πΊ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§}))) = Ξ£π§ β ran πΊ(volβ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§})))) |
109 | 86 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π€ β (ran π β {0})) β π€ β β) |
110 | 1, 2 | i1faddlem 25073 |
. . . . . . . . 9
β’ ((π β§ π€ β β) β (β‘(πΉ βf + πΊ) β {π€}) = βͺ
π§ β ran πΊ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§}))) |
111 | 109, 110 | syldan 592 |
. . . . . . . 8
β’ ((π β§ π€ β (ran π β {0})) β (β‘(πΉ βf + πΊ) β {π€}) = βͺ
π§ β ran πΊ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§}))) |
112 | 111 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ π€ β (ran π β {0})) β (volβ(β‘(πΉ βf + πΊ) β {π€})) = (volββͺ π§ β ran πΊ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§})))) |
113 | 103 | sumeq2dv 15595 |
. . . . . . 7
β’ ((π β§ π€ β (ran π β {0})) β Ξ£π§ β ran πΊ((π€ β π§)πΌπ§) = Ξ£π§ β ran πΊ(volβ((β‘πΉ β {(π€ β π§)}) β© (β‘πΊ β {π§})))) |
114 | 108, 112,
113 | 3eqtr4d 2787 |
. . . . . 6
β’ ((π β§ π€ β (ran π β {0})) β (volβ(β‘(πΉ βf + πΊ) β {π€})) = Ξ£π§ β ran πΊ((π€ β π§)πΌπ§)) |
115 | 114 | oveq2d 7378 |
. . . . 5
β’ ((π β§ π€ β (ran π β {0})) β (π€ Β· (volβ(β‘(πΉ βf + πΊ) β {π€}))) = (π€ Β· Ξ£π§ β ran πΊ((π€ β π§)πΌπ§))) |
116 | 106 | recnd 11190 |
. . . . . 6
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β ((π€ β π§)πΌπ§) β β) |
117 | 75, 109, 116 | fsummulc2 15676 |
. . . . 5
β’ ((π β§ π€ β (ran π β {0})) β (π€ Β· Ξ£π§ β ran πΊ((π€ β π§)πΌπ§)) = Ξ£π§ β ran πΊ(π€ Β· ((π€ β π§)πΌπ§))) |
118 | 115, 117 | eqtrd 2777 |
. . . 4
β’ ((π β§ π€ β (ran π β {0})) β (π€ Β· (volβ(β‘(πΉ βf + πΊ) β {π€}))) = Ξ£π§ β ran πΊ(π€ Β· ((π€ β π§)πΌπ§))) |
119 | 118 | sumeq2dv 15595 |
. . 3
β’ (π β Ξ£π€ β (ran π β {0})(π€ Β· (volβ(β‘(πΉ βf + πΊ) β {π€}))) = Ξ£π€ β (ran π β {0})Ξ£π§ β ran πΊ(π€ Β· ((π€ β π§)πΌπ§))) |
120 | 90, 116 | mulcld 11182 |
. . . . 5
β’ (((π β§ π€ β (ran π β {0})) β§ π§ β ran πΊ) β (π€ Β· ((π€ β π§)πΌπ§)) β β) |
121 | 120 | anasss 468 |
. . . 4
β’ ((π β§ (π€ β (ran π β {0}) β§ π§ β ran πΊ)) β (π€ Β· ((π€ β π§)πΌπ§)) β β) |
122 | 35, 7, 121 | fsumcom 15667 |
. . 3
β’ (π β Ξ£π€ β (ran π β {0})Ξ£π§ β ran πΊ(π€ Β· ((π€ β π§)πΌπ§)) = Ξ£π§ β ran πΊΞ£π€ β (ran π β {0})(π€ Β· ((π€ β π§)πΌπ§))) |
123 | 73, 119, 122 | 3eqtrd 2781 |
. 2
β’ (π β
(β«1β(πΉ
βf + πΊ)) =
Ξ£π§ β ran πΊΞ£π€ β (ran π β {0})(π€ Β· ((π€ β π§)πΌπ§))) |
124 | | oveq1 7369 |
. . . . . . 7
β’ (π¦ = (π€ β π§) β (π¦ + π§) = ((π€ β π§) + π§)) |
125 | | oveq1 7369 |
. . . . . . 7
β’ (π¦ = (π€ β π§) β (π¦πΌπ§) = ((π€ β π§)πΌπ§)) |
126 | 124, 125 | oveq12d 7380 |
. . . . . 6
β’ (π¦ = (π€ β π§) β ((π¦ + π§) Β· (π¦πΌπ§)) = (((π€ β π§) + π§) Β· ((π€ β π§)πΌπ§))) |
127 | 32 | adantr 482 |
. . . . . 6
β’ ((π β§ π§ β ran πΊ) β ran π β Fin) |
128 | 70 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π§ β ran πΊ) β ran π β β) |
129 | 128 | sselda 3949 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ π£ β ran π) β π£ β β) |
130 | 62 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ π£ β ran π) β π§ β β) |
131 | 129, 130 | resubcld 11590 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ π£ β ran π) β (π£ β π§) β β) |
132 | 131 | ex 414 |
. . . . . . . 8
β’ ((π β§ π§ β ran πΊ) β (π£ β ran π β (π£ β π§) β β)) |
133 | 129 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ π£ β ran π) β π£ β β) |
134 | 133 | adantrr 716 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ (π£ β ran π β§ π¦ β ran π)) β π£ β β) |
135 | 70 | sselda 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β ran π) β π¦ β β) |
136 | 135 | ad2ant2rl 748 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ (π£ β ran π β§ π¦ β ran π)) β π¦ β β) |
137 | 136 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ (π£ β ran π β§ π¦ β ran π)) β π¦ β β) |
138 | 62 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ π§ β ran πΊ) β π§ β β) |
139 | 138 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ (π£ β ran π β§ π¦ β ran π)) β π§ β β) |
140 | 134, 137,
139 | subcan2ad 11564 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ (π£ β ran π β§ π¦ β ran π)) β ((π£ β π§) = (π¦ β π§) β π£ = π¦)) |
141 | 140 | ex 414 |
. . . . . . . 8
β’ ((π β§ π§ β ran πΊ) β ((π£ β ran π β§ π¦ β ran π) β ((π£ β π§) = (π¦ β π§) β π£ = π¦))) |
142 | 132, 141 | dom2lem 8939 |
. . . . . . 7
β’ ((π β§ π§ β ran πΊ) β (π£ β ran π β¦ (π£ β π§)):ran πβ1-1ββ) |
143 | | f1f1orn 6800 |
. . . . . . 7
β’ ((π£ β ran π β¦ (π£ β π§)):ran πβ1-1ββ β (π£ β ran π β¦ (π£ β π§)):ran πβ1-1-ontoβran
(π£ β ran π β¦ (π£ β π§))) |
144 | 142, 143 | syl 17 |
. . . . . 6
β’ ((π β§ π§ β ran πΊ) β (π£ β ran π β¦ (π£ β π§)):ran πβ1-1-ontoβran
(π£ β ran π β¦ (π£ β π§))) |
145 | | oveq1 7369 |
. . . . . . . 8
β’ (π£ = π€ β (π£ β π§) = (π€ β π§)) |
146 | | eqid 2737 |
. . . . . . . 8
β’ (π£ β ran π β¦ (π£ β π§)) = (π£ β ran π β¦ (π£ β π§)) |
147 | | ovex 7395 |
. . . . . . . 8
β’ (π€ β π§) β V |
148 | 145, 146,
147 | fvmpt 6953 |
. . . . . . 7
β’ (π€ β ran π β ((π£ β ran π β¦ (π£ β π§))βπ€) = (π€ β π§)) |
149 | 148 | adantl 483 |
. . . . . 6
β’ (((π β§ π§ β ran πΊ) β§ π€ β ran π) β ((π£ β ran π β¦ (π£ β π§))βπ€) = (π€ β π§)) |
150 | | f1f 6743 |
. . . . . . . . . . 11
β’ ((π£ β ran π β¦ (π£ β π§)):ran πβ1-1ββ β (π£ β ran π β¦ (π£ β π§)):ran πβΆβ) |
151 | | frn 6680 |
. . . . . . . . . . 11
β’ ((π£ β ran π β¦ (π£ β π§)):ran πβΆβ β ran (π£ β ran π β¦ (π£ β π§)) β β) |
152 | 142, 150,
151 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β§ π§ β ran πΊ) β ran (π£ β ran π β¦ (π£ β π§)) β β) |
153 | 152 | sselda 3949 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran (π£ β ran π β¦ (π£ β π§))) β π¦ β β) |
154 | 62 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran (π£ β ran π β¦ (π£ β π§))) β π§ β β) |
155 | 153, 154 | readdcld 11191 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran (π£ β ran π β¦ (π£ β π§))) β (π¦ + π§) β β) |
156 | 104 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran (π£ β ran π β¦ (π£ β π§))) β πΌ:(β Γ
β)βΆβ) |
157 | 156, 153,
154 | fovcdmd 7531 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran (π£ β ran π β¦ (π£ β π§))) β (π¦πΌπ§) β β) |
158 | 155, 157 | remulcld 11192 |
. . . . . . 7
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran (π£ β ran π β¦ (π£ β π§))) β ((π¦ + π§) Β· (π¦πΌπ§)) β β) |
159 | 158 | recnd 11190 |
. . . . . 6
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran (π£ β ran π β¦ (π£ β π§))) β ((π¦ + π§) Β· (π¦πΌπ§)) β β) |
160 | 126, 127,
144, 149, 159 | fsumf1o 15615 |
. . . . 5
β’ ((π β§ π§ β ran πΊ) β Ξ£π¦ β ran (π£ β ran π β¦ (π£ β π§))((π¦ + π§) Β· (π¦πΌπ§)) = Ξ£π€ β ran π(((π€ β π§) + π§) Β· ((π€ β π§)πΌπ§))) |
161 | 128 | sselda 3949 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ π€ β ran π) β π€ β β) |
162 | 161 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π€ β ran π) β π€ β β) |
163 | 138 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π€ β ran π) β π§ β β) |
164 | 162, 163 | npcand 11523 |
. . . . . . 7
β’ (((π β§ π§ β ran πΊ) β§ π€ β ran π) β ((π€ β π§) + π§) = π€) |
165 | 164 | oveq1d 7377 |
. . . . . 6
β’ (((π β§ π§ β ran πΊ) β§ π€ β ran π) β (((π€ β π§) + π§) Β· ((π€ β π§)πΌπ§)) = (π€ Β· ((π€ β π§)πΌπ§))) |
166 | 165 | sumeq2dv 15595 |
. . . . 5
β’ ((π β§ π§ β ran πΊ) β Ξ£π€ β ran π(((π€ β π§) + π§) Β· ((π€ β π§)πΌπ§)) = Ξ£π€ β ran π(π€ Β· ((π€ β π§)πΌπ§))) |
167 | 160, 166 | eqtrd 2777 |
. . . 4
β’ ((π β§ π§ β ran πΊ) β Ξ£π¦ β ran (π£ β ran π β¦ (π£ β π§))((π¦ + π§) Β· (π¦πΌπ§)) = Ξ£π€ β ran π(π€ Β· ((π€ β π§)πΌπ§))) |
168 | 39 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β (ran πΉ Γ ran πΊ) β dom + ) |
169 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β π¦ β ran πΉ) |
170 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β π§ β ran πΊ) |
171 | 169, 170 | opelxpd 5676 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β β¨π¦, π§β© β (ran πΉ Γ ran πΊ)) |
172 | | funfvima2 7186 |
. . . . . . . . . . . 12
β’ ((Fun +
β§ (ran πΉ Γ ran
πΊ) β dom + ) β
(β¨π¦, π§β© β (ran πΉ Γ ran πΊ) β ( + ββ¨π¦, π§β©) β ( + β (ran πΉ Γ ran πΊ)))) |
173 | 37, 172 | mpan 689 |
. . . . . . . . . . 11
β’ ((ran
πΉ Γ ran πΊ) β dom + β
(β¨π¦, π§β© β (ran πΉ Γ ran πΊ) β ( + ββ¨π¦, π§β©) β ( + β (ran πΉ Γ ran πΊ)))) |
174 | 168, 171,
173 | sylc 65 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β ( + ββ¨π¦, π§β©) β ( + β (ran πΉ Γ ran πΊ))) |
175 | | df-ov 7365 |
. . . . . . . . . 10
β’ (π¦ + π§) = ( + ββ¨π¦, π§β©) |
176 | 174, 175,
47 | 3eltr4g 2855 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β (π¦ + π§) β ran π) |
177 | 61 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β π¦ β β) |
178 | 177 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β π¦ β β) |
179 | 138 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β π§ β β) |
180 | 178, 179 | pncand 11520 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β ((π¦ + π§) β π§) = π¦) |
181 | 180 | eqcomd 2743 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β π¦ = ((π¦ + π§) β π§)) |
182 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π£ = (π¦ + π§) β (π£ β π§) = ((π¦ + π§) β π§)) |
183 | 182 | rspceeqv 3600 |
. . . . . . . . 9
β’ (((π¦ + π§) β ran π β§ π¦ = ((π¦ + π§) β π§)) β βπ£ β ran π π¦ = (π£ β π§)) |
184 | 176, 181,
183 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β βπ£ β ran π π¦ = (π£ β π§)) |
185 | 184 | ralrimiva 3144 |
. . . . . . 7
β’ ((π β§ π§ β ran πΊ) β βπ¦ β ran πΉβπ£ β ran π π¦ = (π£ β π§)) |
186 | | ssabral 4024 |
. . . . . . 7
β’ (ran
πΉ β {π¦ β£ βπ£ β ran π π¦ = (π£ β π§)} β βπ¦ β ran πΉβπ£ β ran π π¦ = (π£ β π§)) |
187 | 185, 186 | sylibr 233 |
. . . . . 6
β’ ((π β§ π§ β ran πΊ) β ran πΉ β {π¦ β£ βπ£ β ran π π¦ = (π£ β π§)}) |
188 | 146 | rnmpt 5915 |
. . . . . 6
β’ ran
(π£ β ran π β¦ (π£ β π§)) = {π¦ β£ βπ£ β ran π π¦ = (π£ β π§)} |
189 | 187, 188 | sseqtrrdi 4000 |
. . . . 5
β’ ((π β§ π§ β ran πΊ) β ran πΉ β ran (π£ β ran π β¦ (π£ β π§))) |
190 | 62 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β π§ β β) |
191 | 177, 190 | readdcld 11191 |
. . . . . . 7
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β (π¦ + π§) β β) |
192 | 104 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β πΌ:(β Γ
β)βΆβ) |
193 | 192, 177,
190 | fovcdmd 7531 |
. . . . . . 7
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β (π¦πΌπ§) β β) |
194 | 191, 193 | remulcld 11192 |
. . . . . 6
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β ((π¦ + π§) Β· (π¦πΌπ§)) β β) |
195 | 194 | recnd 11190 |
. . . . 5
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β ((π¦ + π§) Β· (π¦πΌπ§)) β β) |
196 | 152 | ssdifd 4105 |
. . . . . . 7
β’ ((π β§ π§ β ran πΊ) β (ran (π£ β ran π β¦ (π£ β π§)) β ran πΉ) β (β β ran πΉ)) |
197 | 196 | sselda 3949 |
. . . . . 6
β’ (((π β§ π§ β ran πΊ) β§ π¦ β (ran (π£ β ran π β¦ (π£ β π§)) β ran πΉ)) β π¦ β (β β ran πΉ)) |
198 | | eldifi 4091 |
. . . . . . . . . . . . 13
β’ (π¦ β (β β ran
πΉ) β π¦ β
β) |
199 | 198 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β π¦ β β) |
200 | 62 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β π§ β β) |
201 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β Β¬ (π¦ = 0 β§ π§ = 0)) |
202 | 1, 2, 101 | itg1addlem3 25078 |
. . . . . . . . . . . 12
β’ (((π¦ β β β§ π§ β β) β§ Β¬
(π¦ = 0 β§ π§ = 0)) β (π¦πΌπ§) = (volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
203 | 199, 200,
201, 202 | syl21anc 837 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β (π¦πΌπ§) = (volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
204 | | inss1 4193 |
. . . . . . . . . . . . . . 15
β’ ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) β (β‘πΉ β {π¦}) |
205 | | eldifn 4092 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β (β β ran
πΉ) β Β¬ π¦ β ran πΉ) |
206 | 205 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β Β¬ π¦ β ran πΉ) |
207 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π£ β V |
208 | 207 | eliniseg 6051 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β V β (π£ β (β‘πΉ β {π¦}) β π£πΉπ¦)) |
209 | 208 | elv 3454 |
. . . . . . . . . . . . . . . . . . 19
β’ (π£ β (β‘πΉ β {π¦}) β π£πΉπ¦) |
210 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . 20
β’ π¦ β V |
211 | 207, 210 | brelrn 5902 |
. . . . . . . . . . . . . . . . . . 19
β’ (π£πΉπ¦ β π¦ β ran πΉ) |
212 | 209, 211 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ β (β‘πΉ β {π¦}) β π¦ β ran πΉ) |
213 | 206, 212 | nsyl 140 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β Β¬ π£ β (β‘πΉ β {π¦})) |
214 | 213 | pm2.21d 121 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β (π£ β (β‘πΉ β {π¦}) β π£ β β
)) |
215 | 214 | ssrdv 3955 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β (β‘πΉ β {π¦}) β β
) |
216 | 204, 215 | sstrid 3960 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) β β
) |
217 | | ss0 4363 |
. . . . . . . . . . . . . 14
β’ (((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) β β
β ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) = β
) |
218 | 216, 217 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) = β
) |
219 | 218 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β (volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§}))) = (volββ
)) |
220 | | 0mbl 24919 |
. . . . . . . . . . . . . 14
β’ β
β dom vol |
221 | | mblvol 24910 |
. . . . . . . . . . . . . 14
β’ (β
β dom vol β (volββ
) =
(vol*ββ
)) |
222 | 220, 221 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(volββ
) = (vol*ββ
) |
223 | | ovol0 24873 |
. . . . . . . . . . . . 13
β’
(vol*ββ
) = 0 |
224 | 222, 223 | eqtri 2765 |
. . . . . . . . . . . 12
β’
(volββ
) = 0 |
225 | 219, 224 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β (volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§}))) = 0) |
226 | 203, 225 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β (π¦πΌπ§) = 0) |
227 | 226 | oveq2d 7378 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β ((π¦ + π§) Β· (π¦πΌπ§)) = ((π¦ + π§) Β· 0)) |
228 | 199, 200 | readdcld 11191 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β (π¦ + π§) β β) |
229 | 228 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β (π¦ + π§) β β) |
230 | 229 | mul01d 11361 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β ((π¦ + π§) Β· 0) = 0) |
231 | 227, 230 | eqtrd 2777 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ (π¦ β (β β ran πΉ) β§ Β¬ (π¦ = 0 β§ π§ = 0))) β ((π¦ + π§) Β· (π¦πΌπ§)) = 0) |
232 | 231 | expr 458 |
. . . . . . 7
β’ (((π β§ π§ β ran πΊ) β§ π¦ β (β β ran πΉ)) β (Β¬ (π¦ = 0 β§ π§ = 0) β ((π¦ + π§) Β· (π¦πΌπ§)) = 0)) |
233 | | oveq12 7371 |
. . . . . . . . . 10
β’ ((π¦ = 0 β§ π§ = 0) β (π¦ + π§) = (0 + 0)) |
234 | 233, 97 | eqtrdi 2793 |
. . . . . . . . 9
β’ ((π¦ = 0 β§ π§ = 0) β (π¦ + π§) = 0) |
235 | | oveq12 7371 |
. . . . . . . . . 10
β’ ((π¦ = 0 β§ π§ = 0) β (π¦πΌπ§) = (0πΌ0)) |
236 | | 0re 11164 |
. . . . . . . . . . 11
β’ 0 β
β |
237 | | iftrue 4497 |
. . . . . . . . . . . 12
β’ ((π = 0 β§ π = 0) β if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π})))) = 0) |
238 | | c0ex 11156 |
. . . . . . . . . . . 12
β’ 0 β
V |
239 | 237, 101,
238 | ovmpoa 7515 |
. . . . . . . . . . 11
β’ ((0
β β β§ 0 β β) β (0πΌ0) = 0) |
240 | 236, 236,
239 | mp2an 691 |
. . . . . . . . . 10
β’ (0πΌ0) = 0 |
241 | 235, 240 | eqtrdi 2793 |
. . . . . . . . 9
β’ ((π¦ = 0 β§ π§ = 0) β (π¦πΌπ§) = 0) |
242 | 234, 241 | oveq12d 7380 |
. . . . . . . 8
β’ ((π¦ = 0 β§ π§ = 0) β ((π¦ + π§) Β· (π¦πΌπ§)) = (0 Β· 0)) |
243 | | 0cn 11154 |
. . . . . . . . 9
β’ 0 β
β |
244 | 243 | mul01i 11352 |
. . . . . . . 8
β’ (0
Β· 0) = 0 |
245 | 242, 244 | eqtrdi 2793 |
. . . . . . 7
β’ ((π¦ = 0 β§ π§ = 0) β ((π¦ + π§) Β· (π¦πΌπ§)) = 0) |
246 | 232, 245 | pm2.61d2 181 |
. . . . . 6
β’ (((π β§ π§ β ran πΊ) β§ π¦ β (β β ran πΉ)) β ((π¦ + π§) Β· (π¦πΌπ§)) = 0) |
247 | 197, 246 | syldan 592 |
. . . . 5
β’ (((π β§ π§ β ran πΊ) β§ π¦ β (ran (π£ β ran π β¦ (π£ β π§)) β ran πΉ)) β ((π¦ + π§) Β· (π¦πΌπ§)) = 0) |
248 | | f1ofo 6796 |
. . . . . . 7
β’ ((π£ β ran π β¦ (π£ β π§)):ran πβ1-1-ontoβran
(π£ β ran π β¦ (π£ β π§)) β (π£ β ran π β¦ (π£ β π§)):ran πβontoβran (π£ β ran π β¦ (π£ β π§))) |
249 | 144, 248 | syl 17 |
. . . . . 6
β’ ((π β§ π§ β ran πΊ) β (π£ β ran π β¦ (π£ β π§)):ran πβontoβran (π£ β ran π β¦ (π£ β π§))) |
250 | | fofi 9289 |
. . . . . 6
β’ ((ran
π β Fin β§ (π£ β ran π β¦ (π£ β π§)):ran πβontoβran (π£ β ran π β¦ (π£ β π§))) β ran (π£ β ran π β¦ (π£ β π§)) β Fin) |
251 | 127, 249,
250 | syl2anc 585 |
. . . . 5
β’ ((π β§ π§ β ran πΊ) β ran (π£ β ran π β¦ (π£ β π§)) β Fin) |
252 | 189, 195,
247, 251 | fsumss 15617 |
. . . 4
β’ ((π β§ π§ β ran πΊ) β Ξ£π¦ β ran πΉ((π¦ + π§) Β· (π¦πΌπ§)) = Ξ£π¦ β ran (π£ β ran π β¦ (π£ β π§))((π¦ + π§) Β· (π¦πΌπ§))) |
253 | 33 | a1i 11 |
. . . . 5
β’ ((π β§ π§ β ran πΊ) β (ran π β {0}) β ran π) |
254 | 120 | an32s 651 |
. . . . 5
β’ (((π β§ π§ β ran πΊ) β§ π€ β (ran π β {0})) β (π€ Β· ((π€ β π§)πΌπ§)) β β) |
255 | | dfin4 4232 |
. . . . . . . 8
β’ (ran
π β© {0}) = (ran π β (ran π β {0})) |
256 | | inss2 4194 |
. . . . . . . 8
β’ (ran
π β© {0}) β
{0} |
257 | 255, 256 | eqsstrri 3984 |
. . . . . . 7
β’ (ran
π β (ran π β {0})) β
{0} |
258 | 257 | sseli 3945 |
. . . . . 6
β’ (π€ β (ran π β (ran π β {0})) β π€ β {0}) |
259 | | elsni 4608 |
. . . . . . . . 9
β’ (π€ β {0} β π€ = 0) |
260 | 259 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π€ β {0}) β π€ = 0) |
261 | 260 | oveq1d 7377 |
. . . . . . 7
β’ (((π β§ π§ β ran πΊ) β§ π€ β {0}) β (π€ Β· ((π€ β π§)πΌπ§)) = (0 Β· ((π€ β π§)πΌπ§))) |
262 | 104 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ π€ β {0}) β πΌ:(β Γ
β)βΆβ) |
263 | 260, 236 | eqeltrdi 2846 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ π€ β {0}) β π€ β β) |
264 | 62 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π§ β ran πΊ) β§ π€ β {0}) β π§ β β) |
265 | 263, 264 | resubcld 11590 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ π€ β {0}) β (π€ β π§) β β) |
266 | 262, 265,
264 | fovcdmd 7531 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ π€ β {0}) β ((π€ β π§)πΌπ§) β β) |
267 | 266 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π€ β {0}) β ((π€ β π§)πΌπ§) β β) |
268 | 267 | mul02d 11360 |
. . . . . . 7
β’ (((π β§ π§ β ran πΊ) β§ π€ β {0}) β (0 Β· ((π€ β π§)πΌπ§)) = 0) |
269 | 261, 268 | eqtrd 2777 |
. . . . . 6
β’ (((π β§ π§ β ran πΊ) β§ π€ β {0}) β (π€ Β· ((π€ β π§)πΌπ§)) = 0) |
270 | 258, 269 | sylan2 594 |
. . . . 5
β’ (((π β§ π§ β ran πΊ) β§ π€ β (ran π β (ran π β {0}))) β (π€ Β· ((π€ β π§)πΌπ§)) = 0) |
271 | 253, 254,
270, 127 | fsumss 15617 |
. . . 4
β’ ((π β§ π§ β ran πΊ) β Ξ£π€ β (ran π β {0})(π€ Β· ((π€ β π§)πΌπ§)) = Ξ£π€ β ran π(π€ Β· ((π€ β π§)πΌπ§))) |
272 | 167, 252,
271 | 3eqtr4d 2787 |
. . 3
β’ ((π β§ π§ β ran πΊ) β Ξ£π¦ β ran πΉ((π¦ + π§) Β· (π¦πΌπ§)) = Ξ£π€ β (ran π β {0})(π€ Β· ((π€ β π§)πΌπ§))) |
273 | 272 | sumeq2dv 15595 |
. 2
β’ (π β Ξ£π§ β ran πΊΞ£π¦ β ran πΉ((π¦ + π§) Β· (π¦πΌπ§)) = Ξ£π§ β ran πΊΞ£π€ β (ran π β {0})(π€ Β· ((π€ β π§)πΌπ§))) |
274 | 195 | anasss 468 |
. . 3
β’ ((π β§ (π§ β ran πΊ β§ π¦ β ran πΉ)) β ((π¦ + π§) Β· (π¦πΌπ§)) β β) |
275 | 7, 5, 274 | fsumcom 15667 |
. 2
β’ (π β Ξ£π§ β ran πΊΞ£π¦ β ran πΉ((π¦ + π§) Β· (π¦πΌπ§)) = Ξ£π¦ β ran πΉΞ£π§ β ran πΊ((π¦ + π§) Β· (π¦πΌπ§))) |
276 | 123, 273,
275 | 3eqtr2d 2783 |
1
β’ (π β
(β«1β(πΉ
βf + πΊ)) =
Ξ£π¦ β ran πΉΞ£π§ β ran πΊ((π¦ + π§) Β· (π¦πΌπ§))) |