Metamath Proof Explorer


Theorem sumeq2ii

Description: Equality theorem for sum, with the class expressions B and C guarded by _I to be always sets. (Contributed by Mario Carneiro, 13-Jun-2019)

Ref Expression
Assertion sumeq2ii ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 simpr ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ )
2 simpr ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ𝑚 ) ) ∧ 𝑛𝐴 ) → 𝑛𝐴 )
3 simplll ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ𝑚 ) ) ∧ 𝑛𝐴 ) → ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) )
4 nfcv 𝑘 I
5 nfcsb1v 𝑘 𝑛 / 𝑘 𝐵
6 4 5 nffv 𝑘 ( I ‘ 𝑛 / 𝑘 𝐵 )
7 nfcsb1v 𝑘 𝑛 / 𝑘 𝐶
8 4 7 nffv 𝑘 ( I ‘ 𝑛 / 𝑘 𝐶 )
9 6 8 nfeq 𝑘 ( I ‘ 𝑛 / 𝑘 𝐵 ) = ( I ‘ 𝑛 / 𝑘 𝐶 )
10 csbeq1a ( 𝑘 = 𝑛𝐵 = 𝑛 / 𝑘 𝐵 )
11 10 fveq2d ( 𝑘 = 𝑛 → ( I ‘ 𝐵 ) = ( I ‘ 𝑛 / 𝑘 𝐵 ) )
12 csbeq1a ( 𝑘 = 𝑛𝐶 = 𝑛 / 𝑘 𝐶 )
13 12 fveq2d ( 𝑘 = 𝑛 → ( I ‘ 𝐶 ) = ( I ‘ 𝑛 / 𝑘 𝐶 ) )
14 11 13 eqeq12d ( 𝑘 = 𝑛 → ( ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ↔ ( I ‘ 𝑛 / 𝑘 𝐵 ) = ( I ‘ 𝑛 / 𝑘 𝐶 ) ) )
15 9 14 rspc ( 𝑛𝐴 → ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( I ‘ 𝑛 / 𝑘 𝐵 ) = ( I ‘ 𝑛 / 𝑘 𝐶 ) ) )
16 2 3 15 sylc ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ𝑚 ) ) ∧ 𝑛𝐴 ) → ( I ‘ 𝑛 / 𝑘 𝐵 ) = ( I ‘ 𝑛 / 𝑘 𝐶 ) )
17 16 ifeq1da ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ𝑚 ) ) → if ( 𝑛𝐴 , ( I ‘ 𝑛 / 𝑘 𝐵 ) , ( I ‘ 0 ) ) = if ( 𝑛𝐴 , ( I ‘ 𝑛 / 𝑘 𝐶 ) , ( I ‘ 0 ) ) )
18 fvif ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) = if ( 𝑛𝐴 , ( I ‘ 𝑛 / 𝑘 𝐵 ) , ( I ‘ 0 ) )
19 fvif ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) = if ( 𝑛𝐴 , ( I ‘ 𝑛 / 𝑘 𝐶 ) , ( I ‘ 0 ) )
20 17 18 19 3eqtr4g ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ𝑚 ) ) → ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) = ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) )
21 20 mpteq2dv ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ𝑚 ) ) → ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) )
22 21 fveq1d ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ𝑚 ) ) → ( ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ‘ 𝑥 ) )
23 eqid ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) )
24 eqid ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) )
25 23 24 fvmptex ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) ‘ 𝑥 )
26 eqid ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) = ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) )
27 eqid ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) )
28 26 27 fvmptex ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℤ ↦ ( I ‘ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ‘ 𝑥 )
29 22 25 28 3eqtr4g ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ𝑚 ) ) → ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ‘ 𝑥 ) )
30 1 29 seqfeq ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) = seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) )
31 30 breq1d ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) )
32 31 anbi2d ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ) )
33 32 rexbidva ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ) )
34 simplr ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) → 𝑚 ∈ ℕ )
35 nnuz ℕ = ( ℤ ‘ 1 )
36 34 35 eleqtrdi ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) → 𝑚 ∈ ( ℤ ‘ 1 ) )
37 f1of ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 )
38 37 ad2antlr ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 )
39 ffvelrn ( ( 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴𝑥 ∈ ( 1 ... 𝑚 ) ) → ( 𝑓𝑥 ) ∈ 𝐴 )
40 38 39 sylancom ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( 𝑓𝑥 ) ∈ 𝐴 )
41 simplll ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) )
42 nfcsb1v 𝑘 ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐵 )
43 nfcsb1v 𝑘 ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐶 )
44 42 43 nfeq 𝑘 ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐵 ) = ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐶 )
45 csbeq1a ( 𝑘 = ( 𝑓𝑥 ) → ( I ‘ 𝐵 ) = ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐵 ) )
46 csbeq1a ( 𝑘 = ( 𝑓𝑥 ) → ( I ‘ 𝐶 ) = ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐶 ) )
47 45 46 eqeq12d ( 𝑘 = ( 𝑓𝑥 ) → ( ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ↔ ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐵 ) = ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐶 ) ) )
48 44 47 rspc ( ( 𝑓𝑥 ) ∈ 𝐴 → ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐵 ) = ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐶 ) ) )
49 40 41 48 sylc ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐵 ) = ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐶 ) )
50 fvex ( 𝑓𝑥 ) ∈ V
51 csbfv2g ( ( 𝑓𝑥 ) ∈ V → ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐵 ) = ( I ‘ ( 𝑓𝑥 ) / 𝑘 𝐵 ) )
52 50 51 ax-mp ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐵 ) = ( I ‘ ( 𝑓𝑥 ) / 𝑘 𝐵 )
53 csbfv2g ( ( 𝑓𝑥 ) ∈ V → ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐶 ) = ( I ‘ ( 𝑓𝑥 ) / 𝑘 𝐶 ) )
54 50 53 ax-mp ( 𝑓𝑥 ) / 𝑘 ( I ‘ 𝐶 ) = ( I ‘ ( 𝑓𝑥 ) / 𝑘 𝐶 )
55 49 52 54 3eqtr3g ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( I ‘ ( 𝑓𝑥 ) / 𝑘 𝐵 ) = ( I ‘ ( 𝑓𝑥 ) / 𝑘 𝐶 ) )
56 elfznn ( 𝑥 ∈ ( 1 ... 𝑚 ) → 𝑥 ∈ ℕ )
57 56 adantl ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → 𝑥 ∈ ℕ )
58 fveq2 ( 𝑛 = 𝑥 → ( 𝑓𝑛 ) = ( 𝑓𝑥 ) )
59 58 csbeq1d ( 𝑛 = 𝑥 ( 𝑓𝑛 ) / 𝑘 𝐵 = ( 𝑓𝑥 ) / 𝑘 𝐵 )
60 eqid ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 )
61 59 60 fvmpti ( 𝑥 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ‘ 𝑥 ) = ( I ‘ ( 𝑓𝑥 ) / 𝑘 𝐵 ) )
62 57 61 syl ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ‘ 𝑥 ) = ( I ‘ ( 𝑓𝑥 ) / 𝑘 𝐵 ) )
63 58 csbeq1d ( 𝑛 = 𝑥 ( 𝑓𝑛 ) / 𝑘 𝐶 = ( 𝑓𝑥 ) / 𝑘 𝐶 )
64 eqid ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) = ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 )
65 63 64 fvmpti ( 𝑥 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ‘ 𝑥 ) = ( I ‘ ( 𝑓𝑥 ) / 𝑘 𝐶 ) )
66 57 65 syl ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ‘ 𝑥 ) = ( I ‘ ( 𝑓𝑥 ) / 𝑘 𝐶 ) )
67 55 62 66 3eqtr4d ( ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ‘ 𝑥 ) )
68 36 67 seqfveq ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) → ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) )
69 68 eqeq2d ( ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴 ) → ( 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ↔ 𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) )
70 69 pm5.32da ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
71 70 exbidv ( ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
72 71 rexbidva ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
73 33 72 orbi12d ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
74 73 iotabidv ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
75 df-sum Σ 𝑘𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐵 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐵 ) ) ‘ 𝑚 ) ) ) )
76 df-sum Σ 𝑘𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ𝑚 ) ∧ seq 𝑚 ( + , ( 𝑛 ∈ ℤ ↦ if ( 𝑛𝐴 , 𝑛 / 𝑘 𝐶 , 0 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto𝐴𝑥 = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( 𝑓𝑛 ) / 𝑘 𝐶 ) ) ‘ 𝑚 ) ) ) )
77 74 75 76 3eqtr4g ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 𝐶 )