This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm ⊢ ( ( 𝑓 : ( 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 ‘ 𝐶 ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ 𝐴 𝐶 )