# Metamath Proof Explorer

## Theorem prodeq2w

Description: Equality theorem for product, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Assertion prodeq2w ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}ℤ=ℤ$
2 ifeq1 ${⊢}{B}={C}\to if\left({k}\in {A},{B},1\right)=if\left({k}\in {A},{C},1\right)$
3 2 alimi ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to \forall {k}\phantom{\rule{.4em}{0ex}}if\left({k}\in {A},{B},1\right)=if\left({k}\in {A},{C},1\right)$
4 alral ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}if\left({k}\in {A},{B},1\right)=if\left({k}\in {A},{C},1\right)\to \forall {k}\in ℤ\phantom{\rule{.4em}{0ex}}if\left({k}\in {A},{B},1\right)=if\left({k}\in {A},{C},1\right)$
5 3 4 syl ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to \forall {k}\in ℤ\phantom{\rule{.4em}{0ex}}if\left({k}\in {A},{B},1\right)=if\left({k}\in {A},{C},1\right)$
6 mpteq12 ${⊢}\left(ℤ=ℤ\wedge \forall {k}\in ℤ\phantom{\rule{.4em}{0ex}}if\left({k}\in {A},{B},1\right)=if\left({k}\in {A},{C},1\right)\right)\to \left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)$
7 1 5 6 sylancr ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to \left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)$
8 7 seqeq3d ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)=seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)$
9 8 breq1d ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to \left(seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}↔seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)$
10 9 anbi2d ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to \left(\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{y}\right)↔\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{y}\right)\right)$
11 10 exbidv ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},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 {A},{C},1\right)\right)\right)⇝{y}\right)\right)$
12 11 rexbidv ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\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},{B},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 {A},{C},1\right)\right)\right)⇝{y}\right)\right)$
13 7 seqeq3d ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)=seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)$
14 13 breq1d ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to \left(seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{x}↔seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\right)⇝{x}\right)$
15 12 14 3anbi23d ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\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},{B},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{x}\right)↔\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)\right)$
16 15 rexbidv ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\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},{B},1\right)\right)\right)⇝{y}\right)\wedge seq{m}\left(×,\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\right)⇝{x}\right)↔\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)\right)$
17 csbeq2
18 17 mpteq2dv
19 18 seqeq3d
20 19 fveq1d
21 20 eqeq2d
22 21 anbi2d
23 22 exbidv
24 23 rexbidv
25 16 24 orbi12d
26 25 iotabidv
27 df-prod
28 df-prod
29 26 27 28 3eqtr4g ${⊢}\forall {k}\phantom{\rule{.4em}{0ex}}{B}={C}\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$