Step | Hyp | Ref
| Expression |
1 | | itgadd.2 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
2 | | iblmbf 25284 |
. . . . . . . . 9
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
3 | 1, 2 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
4 | | itgadd.1 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
5 | 3, 4 | mbfmptcl 25152 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
6 | | itgadd.4 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ
๐ฟ1) |
7 | | iblmbf 25284 |
. . . . . . . . 9
โข ((๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ถ) โ MblFn) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ถ) โ MblFn) |
9 | | itgadd.3 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ ๐) |
10 | 8, 9 | mbfmptcl 25152 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ถ โ โ) |
11 | 5, 10 | readdd 15160 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ(๐ต + ๐ถ)) = ((โโ๐ต) + (โโ๐ถ))) |
12 | 11 | itgeq2dv 25298 |
. . . . 5
โข (๐ โ โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ = โซ๐ด((โโ๐ต) + (โโ๐ถ)) d๐ฅ) |
13 | 5 | recld 15140 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
14 | 5 | iblcn 25315 |
. . . . . . . 8
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1
โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1))) |
15 | 1, 14 | mpbid 231 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ต)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1)) |
16 | 15 | simpld 495 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
17 | 10 | recld 15140 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ถ) โ โ) |
18 | 10 | iblcn 25315 |
. . . . . . . 8
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ถ) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ ๐ฟ1
โง (๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ
๐ฟ1))) |
19 | 6, 18 | mpbid 231 |
. . . . . . 7
โข (๐ โ ((๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ ๐ฟ1 โง (๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ
๐ฟ1)) |
20 | 19 | simpld 495 |
. . . . . 6
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ
๐ฟ1) |
21 | 13, 16, 17, 20, 13, 17 | itgaddlem2 25340 |
. . . . 5
โข (๐ โ โซ๐ด((โโ๐ต) + (โโ๐ถ)) d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ)) |
22 | 12, 21 | eqtrd 2772 |
. . . 4
โข (๐ โ โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ)) |
23 | 5, 10 | imaddd 15161 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ(๐ต + ๐ถ)) = ((โโ๐ต) + (โโ๐ถ))) |
24 | 23 | itgeq2dv 25298 |
. . . . . . 7
โข (๐ โ โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ = โซ๐ด((โโ๐ต) + (โโ๐ถ)) d๐ฅ) |
25 | 5 | imcld 15141 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) โ โ) |
26 | 15 | simprd 496 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ต)) โ
๐ฟ1) |
27 | 10 | imcld 15141 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ถ) โ โ) |
28 | 19 | simprd 496 |
. . . . . . . 8
โข (๐ โ (๐ฅ โ ๐ด โฆ (โโ๐ถ)) โ
๐ฟ1) |
29 | 25, 26, 27, 28, 25, 27 | itgaddlem2 25340 |
. . . . . . 7
โข (๐ โ โซ๐ด((โโ๐ต) + (โโ๐ถ)) d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ)) |
30 | 24, 29 | eqtrd 2772 |
. . . . . 6
โข (๐ โ โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ)) |
31 | 30 | oveq2d 7424 |
. . . . 5
โข (๐ โ (i ยท โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ) = (i ยท (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ))) |
32 | | ax-icn 11168 |
. . . . . . 7
โข i โ
โ |
33 | 32 | a1i 11 |
. . . . . 6
โข (๐ โ i โ
โ) |
34 | 25, 26 | itgcl 25300 |
. . . . . 6
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ โ โ) |
35 | 27, 28 | itgcl 25300 |
. . . . . 6
โข (๐ โ โซ๐ด(โโ๐ถ) d๐ฅ โ โ) |
36 | 33, 34, 35 | adddid 11237 |
. . . . 5
โข (๐ โ (i ยท (โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ)) = ((i ยท โซ๐ด(โโ๐ต) d๐ฅ) + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ))) |
37 | 31, 36 | eqtrd 2772 |
. . . 4
โข (๐ โ (i ยท โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ) = ((i ยท โซ๐ด(โโ๐ต) d๐ฅ) + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ))) |
38 | 22, 37 | oveq12d 7426 |
. . 3
โข (๐ โ (โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ + (i ยท โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ)) = ((โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ) + ((i ยท โซ๐ด(โโ๐ต) d๐ฅ) + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ)))) |
39 | 13, 16 | itgcl 25300 |
. . . 4
โข (๐ โ โซ๐ด(โโ๐ต) d๐ฅ โ โ) |
40 | 17, 20 | itgcl 25300 |
. . . 4
โข (๐ โ โซ๐ด(โโ๐ถ) d๐ฅ โ โ) |
41 | | mulcl 11193 |
. . . . 5
โข ((i
โ โ โง โซ๐ด(โโ๐ต) d๐ฅ โ โ) โ (i ยท
โซ๐ด(โโ๐ต) d๐ฅ) โ โ) |
42 | 32, 34, 41 | sylancr 587 |
. . . 4
โข (๐ โ (i ยท โซ๐ด(โโ๐ต) d๐ฅ) โ โ) |
43 | | mulcl 11193 |
. . . . 5
โข ((i
โ โ โง โซ๐ด(โโ๐ถ) d๐ฅ โ โ) โ (i ยท
โซ๐ด(โโ๐ถ) d๐ฅ) โ โ) |
44 | 32, 35, 43 | sylancr 587 |
. . . 4
โข (๐ โ (i ยท โซ๐ด(โโ๐ถ) d๐ฅ) โ โ) |
45 | 39, 40, 42, 44 | add4d 11441 |
. . 3
โข (๐ โ ((โซ๐ด(โโ๐ต) d๐ฅ + โซ๐ด(โโ๐ถ) d๐ฅ) + ((i ยท โซ๐ด(โโ๐ต) d๐ฅ) + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ))) = ((โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) + (โซ๐ด(โโ๐ถ) d๐ฅ + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ)))) |
46 | 38, 45 | eqtrd 2772 |
. 2
โข (๐ โ (โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ + (i ยท โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ)) = ((โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) + (โซ๐ด(โโ๐ถ) d๐ฅ + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ)))) |
47 | | ovexd 7443 |
. . 3
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ต + ๐ถ) โ V) |
48 | 4, 1, 9, 6 | ibladd 25337 |
. . 3
โข (๐ โ (๐ฅ โ ๐ด โฆ (๐ต + ๐ถ)) โ
๐ฟ1) |
49 | 47, 48 | itgcnval 25316 |
. 2
โข (๐ โ โซ๐ด(๐ต + ๐ถ) d๐ฅ = (โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ + (i ยท โซ๐ด(โโ(๐ต + ๐ถ)) d๐ฅ))) |
50 | 4, 1 | itgcnval 25316 |
. . 3
โข (๐ โ โซ๐ด๐ต d๐ฅ = (โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ))) |
51 | 9, 6 | itgcnval 25316 |
. . 3
โข (๐ โ โซ๐ด๐ถ d๐ฅ = (โซ๐ด(โโ๐ถ) d๐ฅ + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ))) |
52 | 50, 51 | oveq12d 7426 |
. 2
โข (๐ โ (โซ๐ด๐ต d๐ฅ + โซ๐ด๐ถ d๐ฅ) = ((โซ๐ด(โโ๐ต) d๐ฅ + (i ยท โซ๐ด(โโ๐ต) d๐ฅ)) + (โซ๐ด(โโ๐ถ) d๐ฅ + (i ยท โซ๐ด(โโ๐ถ) d๐ฅ)))) |
53 | 46, 49, 52 | 3eqtr4d 2782 |
1
โข (๐ โ โซ๐ด(๐ต + ๐ถ) d๐ฅ = (โซ๐ด๐ต d๐ฅ + โซ๐ด๐ถ d๐ฅ)) |