Metamath Proof Explorer

Theorem dfitg

Description: Evaluate the class substitution in df-itg . (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis dfitg.1 โŠข ๐‘‡ = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) )
Assertion dfitg โˆซ ๐ด ๐ต d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘‡ ) , ๐‘‡ , 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 dfitg.1 โŠข ๐‘‡ = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) )
2 df-itg โŠข โˆซ ๐ด ๐ต d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ โฆ‹ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) / ๐‘ฆ โฆŒ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) , ๐‘ฆ , 0 ) ) ) )
3 fvex โŠข ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ V
4 id โŠข ( ๐‘ฆ = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) โ†’ ๐‘ฆ = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) )
5 4 1 eqtr4di โŠข ( ๐‘ฆ = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) โ†’ ๐‘ฆ = ๐‘‡ )
6 5 breq2d โŠข ( ๐‘ฆ = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) โ†’ ( 0 โ‰ค ๐‘ฆ โ†” 0 โ‰ค ๐‘‡ ) )
7 6 anbi2d โŠข ( ๐‘ฆ = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) โ†’ ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) โ†” ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘‡ ) ) )
8 7 5 ifbieq1d โŠข ( ๐‘ฆ = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) โ†’ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) , ๐‘ฆ , 0 ) = if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘‡ ) , ๐‘‡ , 0 ) )
9 3 8 csbie โŠข โฆ‹ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) / ๐‘ฆ โฆŒ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) , ๐‘ฆ , 0 ) = if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘‡ ) , ๐‘‡ , 0 )
10 9 mpteq2i โŠข ( ๐‘ฅ โˆˆ โ„ โ†ฆ โฆ‹ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) / ๐‘ฆ โฆŒ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) , ๐‘ฆ , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘‡ ) , ๐‘‡ , 0 ) )
11 10 fveq2i โŠข ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ โฆ‹ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) / ๐‘ฆ โฆŒ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) , ๐‘ฆ , 0 ) ) ) = ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘‡ ) , ๐‘‡ , 0 ) ) )
12 11 oveq2i โŠข ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ โฆ‹ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) / ๐‘ฆ โฆŒ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) , ๐‘ฆ , 0 ) ) ) ) = ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘‡ ) , ๐‘‡ , 0 ) ) ) )
13 12 a1i โŠข ( ๐‘˜ โˆˆ ( 0 ... 3 ) โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ โฆ‹ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) / ๐‘ฆ โฆŒ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) , ๐‘ฆ , 0 ) ) ) ) = ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘‡ ) , ๐‘‡ , 0 ) ) ) ) )
14 13 sumeq2i โŠข ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ โฆ‹ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) / ๐‘ฆ โฆŒ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘ฆ ) , ๐‘ฆ , 0 ) ) ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘‡ ) , ๐‘‡ , 0 ) ) ) )
15 2 14 eqtri โŠข โˆซ ๐ด ๐ต d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ๐‘‡ ) , ๐‘‡ , 0 ) ) ) )