Metamath Proof Explorer


Theorem prodeq2sdv

Description: Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017) Avoid axioms. (Revised by GG, 1-Sep-2025)

Ref Expression
Hypothesis prodeq2sdv.1 ( 𝜑𝐵 = 𝐶 )
Assertion prodeq2sdv ( 𝜑 → ∏ 𝑘𝐴 𝐵 = ∏ 𝑘𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 prodeq2sdv.1 ( 𝜑𝐵 = 𝐶 )
2 1 ifeq1d ( 𝜑 → if ( 𝑘𝐴 , 𝐵 , 1 ) = if ( 𝑘𝐴 , 𝐶 , 1 ) )
3 2 mpteq2dv ( 𝜑 → ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) )
4 3 seqeq3d ( 𝜑 → seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) = seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) )
5 4 breq1d ( 𝜑 → ( seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ↔ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) )
6 5 anbi2d ( 𝜑 → ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) )
7 6 exbidv ( 𝜑 → ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) )
8 7 rexbidv ( 𝜑 → ( ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) )
9 3 seqeq3d ( 𝜑 → seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) = seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) )
10 9 breq1d ( 𝜑 → ( seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) )
11 8 10 3anbi23d ( 𝜑 → ( ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ) )
12 11 rexbidv ( 𝜑 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ) )
13 1 csbeq2dv ( 𝜑 ( 𝑓𝑛 ) / 𝑘 𝐵 = ( 𝑓𝑛 ) / 𝑘 𝐶 )
14 13 mpteq2dv ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) )
15 14 seqeq3d ( 𝜑 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) )
16 15 fveq1d ( 𝜑 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) )
17 16 eqeq2d ( 𝜑 → ( 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ↔ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) )
18 17 anbi2d ( 𝜑 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
19 18 exbidv ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
20 19 rexbidv ( 𝜑 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
21 12 20 orbi12d ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 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 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
22 21 iotabidv ( 𝜑 → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 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 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
23 df-prod 𝑘𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) )
24 df-prod 𝑘𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
25 22 23 24 3eqtr4g ( 𝜑 → ∏ 𝑘𝐴 𝐵 = ∏ 𝑘𝐴 𝐶 )