Metamath Proof Explorer

Theorem itgeq2

Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itgeq2 ( โˆ€ ๐‘ฅ โˆˆ ๐ด ๐ต = ๐ถ โ†’ โˆซ ๐ด ๐ต d ๐‘ฅ = โˆซ ๐ด ๐ถ d ๐‘ฅ )

Proof

Step Hyp Ref Expression
1 eqid โŠข โ„ = โ„
2 simpl โŠข ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) โ†’ ๐‘ฅ โˆˆ ๐ด )
3 2 con3i โŠข ( ยฌ ๐‘ฅ โˆˆ ๐ด โ†’ ยฌ ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) )
4 3 iffalsed โŠข ( ยฌ ๐‘ฅ โˆˆ ๐ด โ†’ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = 0 )
5 simpl โŠข ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) โ†’ ๐‘ฅ โˆˆ ๐ด )
6 5 con3i โŠข ( ยฌ ๐‘ฅ โˆˆ ๐ด โ†’ ยฌ ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) )
7 6 iffalsed โŠข ( ยฌ ๐‘ฅ โˆˆ ๐ด โ†’ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = 0 )
8 4 7 eqtr4d โŠข ( ยฌ ๐‘ฅ โˆˆ ๐ด โ†’ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
9 fvoveq1 โŠข ( ๐ต = ๐ถ โ†’ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) )
10 9 breq2d โŠข ( ๐ต = ๐ถ โ†’ ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) โ†” 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) )
11 10 anbi2d โŠข ( ๐ต = ๐ถ โ†’ ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) โ†” ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) ) )
12 11 9 ifbieq1d โŠข ( ๐ต = ๐ถ โ†’ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
13 8 12 ja โŠข ( ( ๐‘ฅ โˆˆ ๐ด โ†’ ๐ต = ๐ถ ) โ†’ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
14 13 a1d โŠข ( ( ๐‘ฅ โˆˆ ๐ด โ†’ ๐ต = ๐ถ ) โ†’ ( ๐‘ฅ โˆˆ โ„ โ†’ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
15 14 ralimi2 โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐ด ๐ต = ๐ถ โ†’ โˆ€ ๐‘ฅ โˆˆ โ„ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
16 mpteq12 โŠข ( ( โ„ = โ„ โˆง โˆ€ ๐‘ฅ โˆˆ โ„ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ†’ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
17 1 15 16 sylancr โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐ด ๐ต = ๐ถ โ†’ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
18 17 fveq2d โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐ด ๐ต = ๐ถ โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) = ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
19 18 oveq2d โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐ด ๐ต = ๐ถ โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) = ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) )
20 19 sumeq2sdv โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐ด ๐ต = ๐ถ โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) )
21 eqid โŠข ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) )
22 21 dfitg โŠข โˆซ ๐ด ๐ต d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
23 eqid โŠข ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) )
24 23 dfitg โŠข โˆซ ๐ด ๐ถ d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
25 20 22 24 3eqtr4g โŠข ( โˆ€ ๐‘ฅ โˆˆ ๐ด ๐ต = ๐ถ โ†’ โˆซ ๐ด ๐ต d ๐‘ฅ = โˆซ ๐ด ๐ถ d ๐‘ฅ )