# Metamath Proof Explorer

## Theorem prodeq1f

Description: Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017)

Ref Expression
Hypotheses prodeq1f.1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
prodeq1f.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
Assertion prodeq1f ${⊢}{A}={B}\to \prod _{{k}\in {A}}{C}=\prod _{{k}\in {B}}{C}$

### Proof

Step Hyp Ref Expression
1 prodeq1f.1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
2 prodeq1f.2 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{B}$
3 sseq1 ${⊢}{A}={B}\to \left({A}\subseteq {ℤ}_{\ge {m}}↔{B}\subseteq {ℤ}_{\ge {m}}\right)$
4 1 2 nfeq ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{A}={B}$
5 eleq2 ${⊢}{A}={B}\to \left({k}\in {A}↔{k}\in {B}\right)$
6 5 ifbid ${⊢}{A}={B}\to if\left({k}\in {A},{C},1\right)=if\left({k}\in {B},{C},1\right)$
7 6 adantr ${⊢}\left({A}={B}\wedge {k}\in ℤ\right)\to if\left({k}\in {A},{C},1\right)=if\left({k}\in {B},{C},1\right)$
8 4 7 mpteq2da ${⊢}{A}={B}\to \left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)=\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)$
9 8 seqeq3d ${⊢}{A}={B}\to seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)=seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)$
10 9 breq1d ${⊢}{A}={B}\to \left(seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}↔seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)⇝{y}\right)$
11 10 anbi2d ${⊢}{A}={B}\to \left(\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)↔\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)⇝{y}\right)\right)$
12 11 exbidv ${⊢}{A}={B}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)⇝{y}\right)\right)$
13 12 rexbidv ${⊢}{A}={B}\to \left(\exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)↔\exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)⇝{y}\right)\right)$
14 8 seqeq3d ${⊢}{A}={B}\to seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)=seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)$
15 14 breq1d ${⊢}{A}={B}\to \left(seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{x}↔seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)⇝{x}\right)$
16 3 13 15 3anbi123d ${⊢}{A}={B}\to \left(\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{x}\right)↔\left({B}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)⇝{x}\right)\right)$
17 16 rexbidv ${⊢}{A}={B}\to \left(\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{x}\right)↔\exists {m}\in ℤ\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {ℤ}_{\ge {m}}\wedge \exists {n}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {B},{C},1\right)\right)\right)⇝{x}\right)\right)$
18 f1oeq3 ${⊢}{A}={B}\to \left({f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}↔{f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{B}\right)$
19 18 anbi1d
20 19 exbidv
21 20 rexbidv
22 17 21 orbi12d
23 22 iotabidv
24 df-prod
25 df-prod
26 23 24 25 3eqtr4g ${⊢}{A}={B}\to \prod _{{k}\in {A}}{C}=\prod _{{k}\in {B}}{C}$