# Metamath Proof Explorer

## Theorem cbvprod

Description: Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses cbvprod.1 ( 𝑗 = 𝑘𝐵 = 𝐶 )
cbvprod.2 𝑘 𝐴
cbvprod.3 𝑗 𝐴
cbvprod.4 𝑘 𝐵
cbvprod.5 𝑗 𝐶
Assertion cbvprod 𝑗𝐴 𝐵 = ∏ 𝑘𝐴 𝐶

### Proof

Step Hyp Ref Expression
1 cbvprod.1 ( 𝑗 = 𝑘𝐵 = 𝐶 )
2 cbvprod.2 𝑘 𝐴
3 cbvprod.3 𝑗 𝐴
4 cbvprod.4 𝑘 𝐵
5 cbvprod.5 𝑗 𝐶
6 biid ( 𝐴 ⊆ ( ℤ𝑚 ) ↔ 𝐴 ⊆ ( ℤ𝑚 ) )
7 2 nfcri 𝑘 𝑗𝐴
8 nfcv 𝑘 1
9 7 4 8 nfif 𝑘 if ( 𝑗𝐴 , 𝐵 , 1 )
10 3 nfcri 𝑗 𝑘𝐴
11 nfcv 𝑗 1
12 10 5 11 nfif 𝑗 if ( 𝑘𝐴 , 𝐶 , 1 )
13 eleq1w ( 𝑗 = 𝑘 → ( 𝑗𝐴𝑘𝐴 ) )
14 13 1 ifbieq1d ( 𝑗 = 𝑘 → if ( 𝑗𝐴 , 𝐵 , 1 ) = if ( 𝑘𝐴 , 𝐶 , 1 ) )
15 9 12 14 cbvmpt ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) )
16 seqeq3 ( ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) → seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) = seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) )
17 15 16 ax-mp seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) = seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) )
18 17 breq1i ( seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ↔ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 )
19 18 anbi2i ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) )
20 19 exbii ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) )
21 20 rexbii ( ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) )
22 seqeq3 ( ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) → seq 𝑚 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) = seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) )
23 15 22 ax-mp seq 𝑚 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) = seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) )
24 23 breq1i ( seq 𝑚 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 )
25 6 21 24 3anbi123i ( ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) )
26 25 rexbii ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) )
27 4 5 1 cbvcsbw ( 𝑓𝑛 ) / 𝑗 𝐵 = ( 𝑓𝑛 ) / 𝑘 𝐶
28 27 mpteq2i ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 )
29 seqeq3 ( ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) )
30 28 29 ax-mp seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) )
31 30 fveq1i ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 )
32 31 eqeq2i ( 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ↔ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) )
33 32 anbi2i ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) )
34 33 exbii ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) )
35 34 rexbii ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) )
36 26 35 orbi12i ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
37 36 iotabii ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
38 df-prod 𝑗𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑗 ∈ ℤ ↦ if ( 𝑗𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑗 𝐵 ) ) ‘ 𝑚 ) ) ) )
39 df-prod 𝑘𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
40 37 38 39 3eqtr4i 𝑗𝐴 𝐵 = ∏ 𝑘𝐴 𝐶