Metamath Proof Explorer

Theorem itgsplit

Description: The S. integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itgsplit.i โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ( ๐ด โˆฉ ๐ต ) ) = 0 )
itgsplit.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ๐ด โˆช ๐ต ) )
itgsplit.c โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ๐ถ โˆˆ ๐‘‰ )
itgsplit.a โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ๐ถ ) โˆˆ ๐ฟ1 )
itgsplit.b โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ ๐ฟ1 )
Assertion itgsplit ( ๐œ‘ โ†’ โˆซ ๐‘ˆ ๐ถ d ๐‘ฅ = ( โˆซ ๐ด ๐ถ d ๐‘ฅ + โˆซ ๐ต ๐ถ d ๐‘ฅ ) )

Proof

Step Hyp Ref Expression
1 itgsplit.i โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ( ๐ด โˆฉ ๐ต ) ) = 0 )
2 itgsplit.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ๐ด โˆช ๐ต ) )
3 itgsplit.c โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ๐ถ โˆˆ ๐‘‰ )
4 itgsplit.a โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ๐ถ ) โˆˆ ๐ฟ1 )
5 itgsplit.b โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ ๐ฟ1 )
6 iblmbf โŠข ( ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ๐ถ ) โˆˆ ๐ฟ1 โ†’ ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ๐ถ ) โˆˆ MblFn )
7 4 6 syl โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ๐ถ ) โˆˆ MblFn )
8 ssun1 โŠข ๐ด โŠ† ( ๐ด โˆช ๐ต )
9 8 2 sseqtrrid โŠข ( ๐œ‘ โ†’ ๐ด โŠ† ๐‘ˆ )
10 9 sselda โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด ) โ†’ ๐‘ฅ โˆˆ ๐‘ˆ )
11 10 3 syldan โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด ) โ†’ ๐ถ โˆˆ ๐‘‰ )
12 7 11 mbfdm2 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ dom vol )
13 12 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ๐ด โˆˆ dom vol )
14 iblmbf โŠข ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ ๐ฟ1 โ†’ ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ MblFn )
15 5 14 syl โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ MblFn )
16 ssun2 โŠข ๐ต โŠ† ( ๐ด โˆช ๐ต )
17 16 2 sseqtrrid โŠข ( ๐œ‘ โ†’ ๐ต โŠ† ๐‘ˆ )
18 17 sselda โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐‘ฅ โˆˆ ๐‘ˆ )
19 18 3 syldan โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐ถ โˆˆ ๐‘‰ )
20 15 19 mbfdm2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ dom vol )
21 20 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ๐ต โˆˆ dom vol )
22 1 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( vol* โ€˜ ( ๐ด โˆฉ ๐ต ) ) = 0 )
23 2 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ๐‘ˆ = ( ๐ด โˆช ๐ต ) )
24 2 eleq2d โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘ˆ โ†” ๐‘ฅ โˆˆ ( ๐ด โˆช ๐ต ) ) )
25 elun โŠข ( ๐‘ฅ โˆˆ ( ๐ด โˆช ๐ต ) โ†” ( ๐‘ฅ โˆˆ ๐ด โˆจ ๐‘ฅ โˆˆ ๐ต ) )
26 24 25 bitrdi โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘ˆ โ†” ( ๐‘ฅ โˆˆ ๐ด โˆจ ๐‘ฅ โˆˆ ๐ต ) ) )
27 26 biimpa โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ( ๐‘ฅ โˆˆ ๐ด โˆจ ๐‘ฅ โˆˆ ๐ต ) )
28 7 11 mbfmptcl โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด ) โ†’ ๐ถ โˆˆ โ„‚ )
29 15 19 mbfmptcl โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐ถ โˆˆ โ„‚ )
30 28 29 jaodan โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐ด โˆจ ๐‘ฅ โˆˆ ๐ต ) ) โ†’ ๐ถ โˆˆ โ„‚ )
31 27 30 syldan โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ๐ถ โˆˆ โ„‚ )
32 31 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ๐ถ โˆˆ โ„‚ )
33 ax-icn โŠข i โˆˆ โ„‚
34 elfznn0 โŠข ( ๐‘˜ โˆˆ ( 0 ... 3 ) โ†’ ๐‘˜ โˆˆ โ„•0 )
35 34 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ๐‘˜ โˆˆ โ„•0 )
36 expcl โŠข ( ( i โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( i โ†‘ ๐‘˜ ) โˆˆ โ„‚ )
37 33 35 36 sylancr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( i โ†‘ ๐‘˜ ) โˆˆ โ„‚ )
38 37 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ( i โ†‘ ๐‘˜ ) โˆˆ โ„‚ )
39 ine0 โŠข i โ‰  0
40 elfzelz โŠข ( ๐‘˜ โˆˆ ( 0 ... 3 ) โ†’ ๐‘˜ โˆˆ โ„ค )
41 40 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ๐‘˜ โˆˆ โ„ค )
42 expne0i โŠข ( ( i โˆˆ โ„‚ โˆง i โ‰  0 โˆง ๐‘˜ โˆˆ โ„ค ) โ†’ ( i โ†‘ ๐‘˜ ) โ‰  0 )
43 33 39 41 42 mp3an12i โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( i โ†‘ ๐‘˜ ) โ‰  0 )
44 43 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ( i โ†‘ ๐‘˜ ) โ‰  0 )
45 32 38 44 divcld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) โˆˆ โ„‚ )
46 45 recld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ โ„ )
47 0re โŠข 0 โˆˆ โ„
48 ifcl โŠข ( ( ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ โ„ โˆง 0 โˆˆ โ„ ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„ )
49 46 47 48 sylancl โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„ )
50 49 rexrd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„* )
51 max1 โŠข ( ( 0 โˆˆ โ„ โˆง ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ โ„ ) โ†’ 0 โ‰ค if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
52 47 46 51 sylancr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ 0 โ‰ค if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
53 elxrge0 โŠข ( if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ ( 0 [,] +โˆž ) โ†” ( if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„* โˆง 0 โ‰ค if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
54 50 52 53 sylanbrc โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐‘ˆ ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ ( 0 [,] +โˆž ) )
55 ifan โŠข if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ๐‘ฅ โˆˆ ๐ด , if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) , 0 )
56 55 mpteq2i โŠข ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ๐‘ฅ โˆˆ ๐ด , if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) , 0 ) )
57 ifan โŠข if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ๐‘ฅ โˆˆ ๐ต , if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) , 0 )
58 57 mpteq2i โŠข ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ๐‘ฅ โˆˆ ๐ต , if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) , 0 ) )
59 ifan โŠข if ( ( ๐‘ฅ โˆˆ ๐‘ˆ โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ๐‘ฅ โˆˆ ๐‘ˆ , if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) , 0 )
60 59 mpteq2i โŠข ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐‘ˆ โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ๐‘ฅ โˆˆ ๐‘ˆ , if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) , 0 ) )
61 eqidd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
62 eqidd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด ) โ†’ ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) )
63 61 62 4 11 iblitg โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„ค ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ )
64 40 63 sylan2 โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ )
65 eqidd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
66 eqidd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) )
67 65 66 5 19 iblitg โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„ค ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ )
68 40 67 sylan2 โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ )
69 13 21 22 23 54 56 58 60 64 68 itg2split โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐‘ˆ โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) = ( ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) + ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) )
70 69 oveq2d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐‘ˆ โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) = ( ( i โ†‘ ๐‘˜ ) ยท ( ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) + ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) ) )
71 63 recnd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„ค ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„‚ )
72 40 71 sylan2 โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„‚ )
73 68 recnd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„‚ )
74 37 72 73 adddid โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) + ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) ) = ( ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) + ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) ) )
75 70 74 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐‘ˆ โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) = ( ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) + ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) ) )
76 75 sumeq2dv โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐‘ˆ โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) + ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) ) )
77 fzfid โŠข ( ๐œ‘ โ†’ ( 0 ... 3 ) โˆˆ Fin )
78 37 72 mulcld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) โˆˆ โ„‚ )
79 37 73 mulcld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) โˆˆ โ„‚ )
80 77 78 79 fsumadd โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) + ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) ) = ( ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) + ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) ) )
81 76 80 eqtrd โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐‘ˆ โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) = ( ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) + ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) ) )
82 eqid โŠข ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) )
83 82 dfitg โŠข โˆซ ๐‘ˆ ๐ถ d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐‘ˆ โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
84 82 dfitg โŠข โˆซ ๐ด ๐ถ d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
85 82 dfitg โŠข โˆซ ๐ต ๐ถ d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
86 84 85 oveq12i โŠข ( โˆซ ๐ด ๐ถ d ๐‘ฅ + โˆซ ๐ต ๐ถ d ๐‘ฅ ) = ( ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) + ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) )
87 81 83 86 3eqtr4g โŠข ( ๐œ‘ โ†’ โˆซ ๐‘ˆ ๐ถ d ๐‘ฅ = ( โˆซ ๐ด ๐ถ d ๐‘ฅ + โˆซ ๐ต ๐ถ d ๐‘ฅ ) )