Step | Hyp | Ref
| Expression |
1 | | itgadd.2 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
2 | | iblmbf 25155 |
. . . . . . . . 9
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
4 | | itgadd.1 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
5 | 3, 4 | mbfmptcl 25023 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
6 | | itgadd.4 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ
๐ฟ1) |
7 | | iblmbf 25155 |
. . . . . . . . 9
โข ((๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ถ) โ MblFn) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ MblFn) |
9 | | itgadd.3 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) |
10 | 8, 9 | mbfmptcl 25023 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) |
11 | 5, 10 | readdd 15108 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ(๐ต + ๐ถ)) = ((โโ๐ต) + (โโ๐ถ))) |
12 | 11 | itgeq2dv 25169 |
. . . . 5
โข (๐ โ โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ = โซ๐ด((โโ๐ต) + (โโ๐ถ)) d๐ฅ) |
13 | 5 | recld 15088 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
14 | 5 | iblcn 25186 |
. . . . . . . 8
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1
โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1))) |
15 | 1, 14 | mpbid 231 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1)) |
16 | 15 | simpld 496 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
17 | 10 | recld 15088 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ถ) โ โ) |
18 | 10 | iblcn 25186 |
. . . . . . . 8
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ ๐ฟ1
โง (๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ
๐ฟ1))) |
19 | 6, 18 | mpbid 231 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ
๐ฟ1)) |
20 | 19 | simpld 496 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ
๐ฟ1) |
21 | 13, 16, 17, 20, 13, 17 | itgaddlem2 25211 |
. . . . 5
โข (๐ โ โซ๐ด((โโ๐ต) + (โโ๐ถ)) d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ)) |
22 | 12, 21 | eqtrd 2773 |
. . . 4
โข (๐ โ โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ)) |
23 | 5, 10 | imaddd 15109 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ(๐ต + ๐ถ)) = ((โโ๐ต) + (โโ๐ถ))) |
24 | 23 | itgeq2dv 25169 |
. . . . . . 7
โข (๐ โ โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ = โซ๐ด((โโ๐ต) + (โโ๐ถ)) d๐ฅ) |
25 | 5 | imcld 15089 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
26 | 15 | simprd 497 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
27 | 10 | imcld 15089 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ถ) โ โ) |
28 | 19 | simprd 497 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ
๐ฟ1) |
29 | 25, 26, 27, 28, 25, 27 | itgaddlem2 25211 |
. . . . . . 7
โข (๐ โ โซ๐ด((โโ๐ต) + (โโ๐ถ)) d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ)) |
30 | 24, 29 | eqtrd 2773 |
. . . . . 6
โข (๐ โ โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ)) |
31 | 30 | oveq2d 7377 |
. . . . 5
โข (๐ โ (i ยท โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ) = (i ยท (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ))) |
32 | | ax-icn 11118 |
. . . . . . 7
โข i โ
โ |
33 | 32 | a1i 11 |
. . . . . 6
โข (๐ โ i โ
โ) |
34 | 25, 26 | itgcl 25171 |
. . . . . 6
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ โ โ) |
35 | 27, 28 | itgcl 25171 |
. . . . . 6
โข (๐ โ โซ๐ด(โโ๐ถ) d๐ฅ โ โ) |
36 | 33, 34, 35 | adddid 11187 |
. . . . 5
โข (๐ โ (i ยท (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ)) = ((i ยท โซ๐ด(โโ๐ต) d๐ฅ) + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ))) |
37 | 31, 36 | eqtrd 2773 |
. . . 4
โข (๐ โ (i ยท โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ) = ((i ยท โซ๐ด(โโ๐ต) d๐ฅ) + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ))) |
38 | 22, 37 | oveq12d 7379 |
. . 3
โข (๐ โ (โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ + (i ยท โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ)) = ((โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ) + ((i ยท โซ๐ด(โโ๐ต) d๐ฅ) + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ)))) |
39 | 13, 16 | itgcl 25171 |
. . . 4
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ โ โ) |
40 | 17, 20 | itgcl 25171 |
. . . 4
โข (๐ โ โซ๐ด(โโ๐ถ) d๐ฅ โ โ) |
41 | | mulcl 11143 |
. . . . 5
โข ((i
โ โ โง โซ๐ด(โโ๐ต) d๐ฅ โ โ) โ (i ยท
โซ๐ด(โโ๐ต) d๐ฅ) โ โ) |
42 | 32, 34, 41 | sylancr 588 |
. . . 4
โข (๐ โ (i ยท โซ๐ด(โโ๐ต) d๐ฅ) โ โ) |
43 | | mulcl 11143 |
. . . . 5
โข ((i
โ โ โง โซ๐ด(โโ๐ถ) d๐ฅ โ โ) โ (i ยท
โซ๐ด(โโ๐ถ) d๐ฅ) โ โ) |
44 | 32, 35, 43 | sylancr 588 |
. . . 4
โข (๐ โ (i ยท โซ๐ด(โโ๐ถ) d๐ฅ) โ โ) |
45 | 39, 40, 42, 44 | add4d 11391 |
. . 3
โข (๐ โ ((โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ) + ((i ยท โซ๐ด(โโ๐ต) d๐ฅ) + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ))) = ((โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) + (โซ๐ด(โโ๐ถ) d๐ฅ + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ)))) |
46 | 38, 45 | eqtrd 2773 |
. 2
โข (๐ โ (โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ + (i ยท โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ)) = ((โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) + (โซ๐ด(โโ๐ถ) d๐ฅ + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ)))) |
47 | | ovexd 7396 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ต + ๐ถ) โ V) |
48 | 4, 1, 9, 6 | ibladd 25208 |
. . 3
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ต + ๐ถ)) โ
๐ฟ1) |
49 | 47, 48 | itgcnval 25187 |
. 2
โข (๐ โ โซ๐ด(๐ต + ๐ถ) d๐ฅ = (โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ + (i ยท โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ))) |
50 | 4, 1 | itgcnval 25187 |
. . 3
โข (๐ โ โซ๐ด๐ต d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) |
51 | 9, 6 | itgcnval 25187 |
. . 3
โข (๐ โ โซ๐ด๐ถ d๐ฅ = (โซ๐ด(โโ๐ถ) d๐ฅ + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ))) |
52 | 50, 51 | oveq12d 7379 |
. 2
โข (๐ โ (โซ๐ด๐ต d๐ฅ + โซ๐ด๐ถ d๐ฅ) = ((โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) + (โซ๐ด(โโ๐ถ) d๐ฅ + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ)))) |
53 | 46, 49, 52 | 3eqtr4d 2783 |
1
โข (๐ โ โซ๐ด(๐ต + ๐ถ) d๐ฅ = (โซ๐ด๐ต d๐ฅ + โซ๐ด๐ถ d๐ฅ)) |