# Metamath Proof Explorer

## Theorem prodeq2ii

Description: Equality theorem for product, with the class expressions B and C guarded by _I to be always sets. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Assertion prodeq2ii ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$

### Proof

Step Hyp Ref Expression
1 eluzelz ${⊢}{n}\in {ℤ}_{\ge {m}}\to {n}\in ℤ$
2 1 adantl ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {n}\in {ℤ}_{\ge {m}}\right)\to {n}\in ℤ$
3 nfra1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)$
4 rsp ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\to \left({k}\in {A}\to \mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\right)$
5 4 adantr ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {k}\in ℤ\right)\to \left({k}\in {A}\to \mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\right)$
6 ifeq1 ${⊢}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\to if\left({k}\in {A},\mathrm{I}\left({B}\right),\mathrm{I}\left(1\right)\right)=if\left({k}\in {A},\mathrm{I}\left({C}\right),\mathrm{I}\left(1\right)\right)$
7 5 6 syl6 ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {k}\in ℤ\right)\to \left({k}\in {A}\to if\left({k}\in {A},\mathrm{I}\left({B}\right),\mathrm{I}\left(1\right)\right)=if\left({k}\in {A},\mathrm{I}\left({C}\right),\mathrm{I}\left(1\right)\right)\right)$
8 iffalse ${⊢}¬{k}\in {A}\to if\left({k}\in {A},\mathrm{I}\left({B}\right),\mathrm{I}\left(1\right)\right)=\mathrm{I}\left(1\right)$
9 iffalse ${⊢}¬{k}\in {A}\to if\left({k}\in {A},\mathrm{I}\left({C}\right),\mathrm{I}\left(1\right)\right)=\mathrm{I}\left(1\right)$
10 8 9 eqtr4d ${⊢}¬{k}\in {A}\to if\left({k}\in {A},\mathrm{I}\left({B}\right),\mathrm{I}\left(1\right)\right)=if\left({k}\in {A},\mathrm{I}\left({C}\right),\mathrm{I}\left(1\right)\right)$
11 7 10 pm2.61d1 ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {k}\in ℤ\right)\to if\left({k}\in {A},\mathrm{I}\left({B}\right),\mathrm{I}\left(1\right)\right)=if\left({k}\in {A},\mathrm{I}\left({C}\right),\mathrm{I}\left(1\right)\right)$
12 fvif ${⊢}\mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)=if\left({k}\in {A},\mathrm{I}\left({B}\right),\mathrm{I}\left(1\right)\right)$
13 fvif ${⊢}\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)=if\left({k}\in {A},\mathrm{I}\left({C}\right),\mathrm{I}\left(1\right)\right)$
14 11 12 13 3eqtr4g ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {k}\in ℤ\right)\to \mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)=\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)$
15 3 14 mpteq2da ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\to \left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)\right)=\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)\right)$
16 15 adantr ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {x}\in {ℤ}_{\ge {n}}\right)\to \left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)\right)=\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)\right)$
17 16 fveq1d ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {x}\in {ℤ}_{\ge {n}}\right)\to \left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)\right)\left({x}\right)=\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)\right)\left({x}\right)$
18 17 adantlr ${⊢}\left(\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {n}\in {ℤ}_{\ge {m}}\right)\wedge {x}\in {ℤ}_{\ge {n}}\right)\to \left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)\right)\left({x}\right)=\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)\right)\left({x}\right)$
19 eqid ${⊢}\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
20 eqid ${⊢}\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)\right)=\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)\right)$
21 19 20 fvmptex ${⊢}\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\left({x}\right)=\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)\right)\left({x}\right)$
22 eqid ${⊢}\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)$
23 eqid ${⊢}\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)\right)=\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)\right)$
24 22 23 fvmptex ${⊢}\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\left({x}\right)=\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)\right)\left({x}\right)$
25 18 21 24 3eqtr4g ${⊢}\left(\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {n}\in {ℤ}_{\ge {m}}\right)\wedge {x}\in {ℤ}_{\ge {n}}\right)\to \left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\left({x}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\left({x}\right)$
26 2 25 seqfeq ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {n}\in {ℤ}_{\ge {m}}\right)\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)$
27 26 breq1d ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {n}\in {ℤ}_{\ge {m}}\right)\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)$
28 27 anbi2d ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {n}\in {ℤ}_{\ge {m}}\right)\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)$
29 28 exbidv ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {n}\in {ℤ}_{\ge {m}}\right)\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)$
30 29 rexbidva ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\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)$
31 30 adantr ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℤ\right)\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)$
32 simpr ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℤ\right)\to {m}\in ℤ$
33 15 adantr ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {x}\in {ℤ}_{\ge {m}}\right)\to \left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)\right)=\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)\right)$
34 33 fveq1d ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {x}\in {ℤ}_{\ge {m}}\right)\to \left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{B},1\right)\right)\right)\left({x}\right)=\left({k}\in ℤ⟼\mathrm{I}\left(if\left({k}\in {A},{C},1\right)\right)\right)\left({x}\right)$
35 34 21 24 3eqtr4g ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {x}\in {ℤ}_{\ge {m}}\right)\to \left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\left({x}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\left({x}\right)$
36 35 adantlr ${⊢}\left(\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℤ\right)\wedge {x}\in {ℤ}_{\ge {m}}\right)\to \left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)\left({x}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{C},1\right)\right)\left({x}\right)$
37 32 36 seqfeq ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℤ\right)\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)$
38 37 breq1d ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℤ\right)\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)$
39 31 38 3anbi23d ${⊢}\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℤ\right)\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)$
40 39 rexbidva ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\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)$
41 simplr ${⊢}\left(\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\to {m}\in ℕ$
42 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
43 41 42 eleqtrdi ${⊢}\left(\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\to {m}\in {ℤ}_{\ge 1}$
44 f1of ${⊢}{f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\to {f}:\left(1\dots {m}\right)⟶{A}$
45 44 ad2antlr ${⊢}\left(\left(\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {x}\in \left(1\dots {m}\right)\right)\to {f}:\left(1\dots {m}\right)⟶{A}$
46 ffvelrn ${⊢}\left({f}:\left(1\dots {m}\right)⟶{A}\wedge {x}\in \left(1\dots {m}\right)\right)\to {f}\left({x}\right)\in {A}$
47 45 46 sylancom ${⊢}\left(\left(\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {x}\in \left(1\dots {m}\right)\right)\to {f}\left({x}\right)\in {A}$
48 simplll ${⊢}\left(\left(\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {x}\in \left(1\dots {m}\right)\right)\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)$
49 nfcsb1v
50 nfcsb1v
51 49 50 nfeq
52 csbeq1a
53 csbeq1a
54 52 53 eqeq12d
55 51 54 rspc
56 47 48 55 sylc
57 fvex ${⊢}{f}\left({x}\right)\in \mathrm{V}$
58 csbfv2g
59 57 58 ax-mp
60 csbfv2g
61 57 60 ax-mp
62 56 59 61 3eqtr3g
63 elfznn ${⊢}{x}\in \left(1\dots {m}\right)\to {x}\in ℕ$
64 63 adantl ${⊢}\left(\left(\left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\wedge {m}\in ℕ\right)\wedge {f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}\right)\wedge {x}\in \left(1\dots {m}\right)\right)\to {x}\in ℕ$
65 fveq2 ${⊢}{n}={x}\to {f}\left({n}\right)={f}\left({x}\right)$
66 65 csbeq1d
67 eqid
68 66 67 fvmpti
69 64 68 syl
70 65 csbeq1d
71 eqid
72 70 71 fvmpti
73 64 72 syl
74 62 69 73 3eqtr4d
75 43 74 seqfveq
76 75 eqeq2d
77 76 pm5.32da
78 77 exbidv
79 78 rexbidva
80 40 79 orbi12d
81 80 iotabidv
82 df-prod
83 df-prod
84 81 82 83 3eqtr4g ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{I}\left({B}\right)=\mathrm{I}\left({C}\right)\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$