Metamath Proof Explorer


Theorem nfitg

Description: Bound-variable hypothesis builder for an integral: if y is (effectively) not free in A and B , it is not free in S. A B _d x . (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Hypotheses nfitg.1 โŠข โ„ฒ ๐‘ฆ ๐ด
nfitg.2 โŠข โ„ฒ ๐‘ฆ ๐ต
Assertion nfitg โ„ฒ ๐‘ฆ โˆซ ๐ด ๐ต d ๐‘ฅ

Proof

Step Hyp Ref Expression
1 nfitg.1 โŠข โ„ฒ ๐‘ฆ ๐ด
2 nfitg.2 โŠข โ„ฒ ๐‘ฆ ๐ต
3 eqid โŠข ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) )
4 3 dfitg โŠข โˆซ ๐ด ๐ต d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
5 nfcv โŠข โ„ฒ ๐‘ฆ ( 0 ... 3 )
6 nfcv โŠข โ„ฒ ๐‘ฆ ( i โ†‘ ๐‘˜ )
7 nfcv โŠข โ„ฒ ๐‘ฆ ยท
8 nfcv โŠข โ„ฒ ๐‘ฆ โˆซ2
9 nfcv โŠข โ„ฒ ๐‘ฆ โ„
10 1 nfcri โŠข โ„ฒ ๐‘ฆ ๐‘ฅ โˆˆ ๐ด
11 nfcv โŠข โ„ฒ ๐‘ฆ 0
12 nfcv โŠข โ„ฒ ๐‘ฆ โ‰ค
13 nfcv โŠข โ„ฒ ๐‘ฆ โ„œ
14 nfcv โŠข โ„ฒ ๐‘ฆ /
15 2 14 6 nfov โŠข โ„ฒ ๐‘ฆ ( ๐ต / ( i โ†‘ ๐‘˜ ) )
16 13 15 nffv โŠข โ„ฒ ๐‘ฆ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) )
17 11 12 16 nfbr โŠข โ„ฒ ๐‘ฆ 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) )
18 10 17 nfan โŠข โ„ฒ ๐‘ฆ ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) )
19 18 16 11 nfif โŠข โ„ฒ ๐‘ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 )
20 9 19 nfmpt โŠข โ„ฒ ๐‘ฆ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
21 8 20 nffv โŠข โ„ฒ ๐‘ฆ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
22 6 7 21 nfov โŠข โ„ฒ ๐‘ฆ ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
23 5 22 nfsum โŠข โ„ฒ ๐‘ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
24 4 23 nfcxfr โŠข โ„ฒ ๐‘ฆ โˆซ ๐ด ๐ต d ๐‘ฅ