# 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 $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C → ∏ k ∈ A B = ∏ k ∈ A C$

### Proof

Step Hyp Ref Expression
1 eluzelz $⊢ n ∈ ℤ ≥ m → n ∈ ℤ$
2 1 adantl $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ n ∈ ℤ ≥ m → n ∈ ℤ$
3 nfra1 $⊢ Ⅎ k ∀ k ∈ A I ⁡ B = I ⁡ C$
4 rsp $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C → k ∈ A → I ⁡ B = I ⁡ C$
5 4 adantr $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ k ∈ ℤ → k ∈ A → I ⁡ B = I ⁡ C$
6 ifeq1 $⊢ I ⁡ B = I ⁡ C → if k ∈ A I ⁡ B I ⁡ 1 = if k ∈ A I ⁡ C I ⁡ 1$
7 5 6 syl6 $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ k ∈ ℤ → k ∈ A → if k ∈ A I ⁡ B I ⁡ 1 = if k ∈ A I ⁡ C I ⁡ 1$
8 iffalse $⊢ ¬ k ∈ A → if k ∈ A I ⁡ B I ⁡ 1 = I ⁡ 1$
9 iffalse $⊢ ¬ k ∈ A → if k ∈ A I ⁡ C I ⁡ 1 = I ⁡ 1$
10 8 9 eqtr4d $⊢ ¬ k ∈ A → if k ∈ A I ⁡ B I ⁡ 1 = if k ∈ A I ⁡ C I ⁡ 1$
11 7 10 pm2.61d1 $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ k ∈ ℤ → if k ∈ A I ⁡ B I ⁡ 1 = if k ∈ A I ⁡ C I ⁡ 1$
12 fvif $⊢ I ⁡ if k ∈ A B 1 = if k ∈ A I ⁡ B I ⁡ 1$
13 fvif $⊢ I ⁡ if k ∈ A C 1 = if k ∈ A I ⁡ C I ⁡ 1$
14 11 12 13 3eqtr4g $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ k ∈ ℤ → I ⁡ if k ∈ A B 1 = I ⁡ if k ∈ A C 1$
15 3 14 mpteq2da $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C → k ∈ ℤ ⟼ I ⁡ if k ∈ A B 1 = k ∈ ℤ ⟼ I ⁡ if k ∈ A C 1$
16 15 adantr $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ x ∈ ℤ ≥ n → k ∈ ℤ ⟼ I ⁡ if k ∈ A B 1 = k ∈ ℤ ⟼ I ⁡ if k ∈ A C 1$
17 16 fveq1d $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ x ∈ ℤ ≥ n → k ∈ ℤ ⟼ I ⁡ if k ∈ A B 1 ⁡ x = k ∈ ℤ ⟼ I ⁡ if k ∈ A C 1 ⁡ x$
18 17 adantlr $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ n ∈ ℤ ≥ m ∧ x ∈ ℤ ≥ n → k ∈ ℤ ⟼ I ⁡ if k ∈ A B 1 ⁡ x = k ∈ ℤ ⟼ I ⁡ if k ∈ A C 1 ⁡ x$
19 eqid $⊢ k ∈ ℤ ⟼ if k ∈ A B 1 = k ∈ ℤ ⟼ if k ∈ A B 1$
20 eqid $⊢ k ∈ ℤ ⟼ I ⁡ if k ∈ A B 1 = k ∈ ℤ ⟼ I ⁡ if k ∈ A B 1$
21 19 20 fvmptex $⊢ k ∈ ℤ ⟼ if k ∈ A B 1 ⁡ x = k ∈ ℤ ⟼ I ⁡ if k ∈ A B 1 ⁡ x$
22 eqid $⊢ k ∈ ℤ ⟼ if k ∈ A C 1 = k ∈ ℤ ⟼ if k ∈ A C 1$
23 eqid $⊢ k ∈ ℤ ⟼ I ⁡ if k ∈ A C 1 = k ∈ ℤ ⟼ I ⁡ if k ∈ A C 1$
24 22 23 fvmptex $⊢ k ∈ ℤ ⟼ if k ∈ A C 1 ⁡ x = k ∈ ℤ ⟼ I ⁡ if k ∈ A C 1 ⁡ x$
25 18 21 24 3eqtr4g $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ n ∈ ℤ ≥ m ∧ x ∈ ℤ ≥ n → k ∈ ℤ ⟼ if k ∈ A B 1 ⁡ x = k ∈ ℤ ⟼ if k ∈ A C 1 ⁡ x$
26 2 25 seqfeq $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ n ∈ ℤ ≥ m → seq n × k ∈ ℤ ⟼ if k ∈ A B 1 = seq n × k ∈ ℤ ⟼ if k ∈ A C 1$
27 26 breq1d $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ n ∈ ℤ ≥ m → seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ↔ seq n × k ∈ ℤ ⟼ if k ∈ A C 1 ⇝ y$
28 27 anbi2d $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ n ∈ ℤ ≥ m → y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ↔ y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A C 1 ⇝ y$
29 28 exbidv $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ n ∈ ℤ ≥ m → ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ↔ ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A C 1 ⇝ y$
30 29 rexbidva $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C → ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ↔ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A C 1 ⇝ y$
31 30 adantr $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℤ → ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ↔ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A C 1 ⇝ y$
32 simpr $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℤ → m ∈ ℤ$
33 15 adantr $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ x ∈ ℤ ≥ m → k ∈ ℤ ⟼ I ⁡ if k ∈ A B 1 = k ∈ ℤ ⟼ I ⁡ if k ∈ A C 1$
34 33 fveq1d $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ x ∈ ℤ ≥ m → k ∈ ℤ ⟼ I ⁡ if k ∈ A B 1 ⁡ x = k ∈ ℤ ⟼ I ⁡ if k ∈ A C 1 ⁡ x$
35 34 21 24 3eqtr4g $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ x ∈ ℤ ≥ m → k ∈ ℤ ⟼ if k ∈ A B 1 ⁡ x = k ∈ ℤ ⟼ if k ∈ A C 1 ⁡ x$
36 35 adantlr $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℤ ∧ x ∈ ℤ ≥ m → k ∈ ℤ ⟼ if k ∈ A B 1 ⁡ x = k ∈ ℤ ⟼ if k ∈ A C 1 ⁡ x$
37 32 36 seqfeq $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℤ → seq m × k ∈ ℤ ⟼ if k ∈ A B 1 = seq m × k ∈ ℤ ⟼ if k ∈ A C 1$
38 37 breq1d $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℤ → seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x ↔ seq m × k ∈ ℤ ⟼ if k ∈ A C 1 ⇝ x$
39 31 38 3anbi23d $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℤ → A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x ↔ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A C 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A C 1 ⇝ x$
40 39 rexbidva $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C → ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A B 1 ⇝ x ↔ ∃ m ∈ ℤ A ⊆ ℤ ≥ m ∧ ∃ n ∈ ℤ ≥ m ∃ y y ≠ 0 ∧ seq n × k ∈ ℤ ⟼ if k ∈ A C 1 ⇝ y ∧ seq m × k ∈ ℤ ⟼ if k ∈ A C 1 ⇝ x$
41 simplr $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℕ ∧ f : 1 … m ⟶ 1-1 onto A → m ∈ ℕ$
42 nnuz $⊢ ℕ = ℤ ≥ 1$
43 41 42 eleqtrdi $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℕ ∧ f : 1 … m ⟶ 1-1 onto A → m ∈ ℤ ≥ 1$
44 f1of $⊢ f : 1 … m ⟶ 1-1 onto A → f : 1 … m ⟶ A$
45 44 ad2antlr $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℕ ∧ f : 1 … m ⟶ 1-1 onto A ∧ x ∈ 1 … m → f : 1 … m ⟶ A$
46 ffvelrn $⊢ f : 1 … m ⟶ A ∧ x ∈ 1 … m → f ⁡ x ∈ A$
47 45 46 sylancom $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℕ ∧ f : 1 … m ⟶ 1-1 onto A ∧ x ∈ 1 … m → f ⁡ x ∈ A$
48 simplll $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℕ ∧ f : 1 … m ⟶ 1-1 onto A ∧ x ∈ 1 … m → ∀ k ∈ A I ⁡ B = I ⁡ C$
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 ⁡ x ∈ V$
58 csbfv2g
59 57 58 ax-mp
60 csbfv2g
61 57 60 ax-mp
62 56 59 61 3eqtr3g
63 elfznn $⊢ x ∈ 1 … m → x ∈ ℕ$
64 63 adantl $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C ∧ m ∈ ℕ ∧ f : 1 … m ⟶ 1-1 onto A ∧ x ∈ 1 … m → x ∈ ℕ$
65 fveq2 $⊢ n = x → f ⁡ n = f ⁡ x$
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 $⊢ ∀ k ∈ A I ⁡ B = I ⁡ C → ∏ k ∈ A B = ∏ k ∈ A C$