Metamath Proof Explorer

Theorem fsumdvdsmul

Description: Product of two divisor sums. (This is also the main part of the proof that " sum_ k || N F ( k ) is a multiplicative function if F is".) (Contributed by Mario Carneiro, 2-Jul-2015) Avoid ax-mulf . (Revised by GG, 18-Apr-2025)

Ref Expression
Hypotheses mpodvdsmulf1o.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
mpodvdsmulf1o.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
mpodvdsmulf1o.3 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
mpodvdsmulf1o.x ⊢ 𝑋 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 }
mpodvdsmulf1o.y ⊢ 𝑌 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
mpodvdsmulf1o.z ⊢ 𝑍 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
fsumdvdsmul.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
fsumdvdsmul.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐵 ∈ ℂ )
fsumdvdsmul.6 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → ( 𝐴 · 𝐵 ) = 𝐷 )
fsumdvdsmul.7 ⊢ ( 𝑖 = ( 𝑗 · 𝑘 ) → 𝐶 = 𝐷 )
Assertion fsumdvdsmul ( 𝜑 → ( Σ 𝑗 ∈ 𝑋 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑖 ∈ 𝑍 𝐶 )

Proof

Step Hyp Ref Expression
1 mpodvdsmulf1o.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 mpodvdsmulf1o.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 mpodvdsmulf1o.3 ⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
4 mpodvdsmulf1o.x ⊢ 𝑋 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 }
5 mpodvdsmulf1o.y ⊢ 𝑌 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 }
6 mpodvdsmulf1o.z ⊢ 𝑍 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
7 fsumdvdsmul.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
8 fsumdvdsmul.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑌 ) → 𝐵 ∈ ℂ )
9 fsumdvdsmul.6 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → ( 𝐴 · 𝐵 ) = 𝐷 )
10 fsumdvdsmul.7 ⊢ ( 𝑖 = ( 𝑗 · 𝑘 ) → 𝐶 = 𝐷 )
11 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
12 dvdsssfz1 ⊢ ( 𝑀 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ⊆ ( 1 ... 𝑀 ) )
13 1 12 syl ⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑀 } ⊆ ( 1 ... 𝑀 ) )
14 4 13 eqsstrid ⊢ ( 𝜑 → 𝑋 ⊆ ( 1 ... 𝑀 ) )
15 11 14 ssfid ⊢ ( 𝜑 → 𝑋 ∈ Fin )
16 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
17 dvdsssfz1 ⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
18 2 17 syl ⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
19 5 18 eqsstrid ⊢ ( 𝜑 → 𝑌 ⊆ ( 1 ... 𝑁 ) )
20 16 19 ssfid ⊢ ( 𝜑 → 𝑌 ∈ Fin )
21 20 8 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑌 𝐵 ∈ ℂ )
22 15 21 7 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑗 ∈ 𝑋 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑗 ∈ 𝑋 ( 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) )
23 20 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝑌 ∈ Fin )
24 8 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑌 ) → 𝐵 ∈ ℂ )
25 23 7 24 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑘 ∈ 𝑌 ( 𝐴 · 𝐵 ) )
26 9 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑌 ) → ( 𝐴 · 𝐵 ) = 𝐷 )
27 26 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → Σ 𝑘 ∈ 𝑌 ( 𝐴 · 𝐵 ) = Σ 𝑘 ∈ 𝑌 𝐷 )
28 25 27 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑘 ∈ 𝑌 𝐷 )
29 28 sumeq2dv ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑋 ( 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑗 ∈ 𝑋 Σ 𝑘 ∈ 𝑌 𝐷 )
30 elxpi ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ∃ 𝑢 ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) )
31 fveq2 ⊢ ( ⟨ 𝑢 , 𝑣 ⟩ = 𝑧 → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) )
32 31 eqcoms ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) )
33 fveq2 ⊢ ( ⟨ 𝑢 , 𝑣 ⟩ = 𝑧 → ( · ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( · ‘ 𝑧 ) )
34 33 eqcoms ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( · ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( · ‘ 𝑧 ) )
35 32 34 eqeq12d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( · ‘ ⟨ 𝑢 , 𝑣 ⟩ ) ↔ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) = ( · ‘ 𝑧 ) ) )
36 35 biimpd ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( · ‘ ⟨ 𝑢 , 𝑣 ⟩ ) → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) = ( · ‘ 𝑧 ) ) )
37 4 ssrab3 ⊢ 𝑋 ⊆ ℕ
38 nnsscn ⊢ ℕ ⊆ ℂ
39 37 38 sstri ⊢ 𝑋 ⊆ ℂ
40 39 sseli ⊢ ( 𝑢 ∈ 𝑋 → 𝑢 ∈ ℂ )
41 5 ssrab3 ⊢ 𝑌 ⊆ ℕ
42 41 38 sstri ⊢ 𝑌 ⊆ ℂ
43 42 sseli ⊢ ( 𝑣 ∈ 𝑌 → 𝑣 ∈ ℂ )
44 ovmpot ⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) = ( 𝑢 · 𝑣 ) )
45 df-ov ⊢ ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
46 df-ov ⊢ ( 𝑢 · 𝑣 ) = ( · ‘ ⟨ 𝑢 , 𝑣 ⟩ )
47 44 45 46 3eqtr3g ⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( · ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
48 40 43 47 syl2an ⊢ ( ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( · ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
49 36 48 impel ⊢ ( ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) = ( · ‘ 𝑧 ) )
50 49 exlimivv ⊢ ( ∃ 𝑢 ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) = ( · ‘ 𝑧 ) )
51 30 50 syl ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) = ( · ‘ 𝑧 ) )
52 51 eqcomd ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( · ‘ 𝑧 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) )
53 52 csbeq1d ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 = ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 )
54 53 sumeq2i ⊢ Σ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 = Σ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶
55 fveq2 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ( · ‘ 𝑧 ) = ( · ‘ ⟨ 𝑗 , 𝑘 ⟩ ) )
56 df-ov ⊢ ( 𝑗 · 𝑘 ) = ( · ‘ ⟨ 𝑗 , 𝑘 ⟩ )
57 55 56 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ( · ‘ 𝑧 ) = ( 𝑗 · 𝑘 ) )
58 57 csbeq1d ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 = ⦋ ( 𝑗 · 𝑘 ) / 𝑖 ⦌ 𝐶 )
59 ovex ⊢ ( 𝑗 · 𝑘 ) ∈ V
60 59 10 csbie ⊢ ⦋ ( 𝑗 · 𝑘 ) / 𝑖 ⦌ 𝐶 = 𝐷
61 58 60 eqtrdi ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 = 𝐷 )
62 7 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → 𝐴 ∈ ℂ )
63 8 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → 𝐵 ∈ ℂ )
64 62 63 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
65 9 64 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑌 ) ) → 𝐷 ∈ ℂ )
66 61 15 20 65 fsumxp ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑋 Σ 𝑘 ∈ 𝑌 𝐷 = Σ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 )
67 nfcv ⊢ Ⅎ 𝑤 𝐶
68 nfcsb1v ⊢ Ⅎ 𝑖 ⦋ 𝑤 / 𝑖 ⦌ 𝐶
69 csbeq1a ⊢ ( 𝑖 = 𝑤 → 𝐶 = ⦋ 𝑤 / 𝑖 ⦌ 𝐶 )
70 67 68 69 cbvsumi ⊢ Σ 𝑖 ∈ 𝑍 𝐶 = Σ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶
71 csbeq1 ⊢ ( 𝑤 = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) → ⦋ 𝑤 / 𝑖 ⦌ 𝐶 = ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 )
72 xpfi ⊢ ( ( 𝑋 ∈ Fin ∧ 𝑌 ∈ Fin ) → ( 𝑋 × 𝑌 ) ∈ Fin )
73 15 20 72 syl2anc ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ Fin )
74 1 2 3 4 5 6 mpodvdsmulf1o ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto→ 𝑍 )
75 fvres ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) )
76 75 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) )
77 65 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝑋 ∀ 𝑘 ∈ 𝑌 𝐷 ∈ ℂ )
78 61 eleq1d ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ( ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ 𝐷 ∈ ℂ ) )
79 78 ralxp ⊢ ( ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑗 ∈ 𝑋 ∀ 𝑘 ∈ 𝑌 𝐷 ∈ ℂ )
80 77 79 sylibr ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ )
81 fveq2 ⊢ ( 𝑧 = 𝑤 → ( · ‘ 𝑧 ) = ( · ‘ 𝑤 ) )
82 81 csbeq1d ⊢ ( 𝑧 = 𝑤 → ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 = ⦋ ( · ‘ 𝑤 ) / 𝑖 ⦌ 𝐶 )
83 82 eleq1d ⊢ ( 𝑧 = 𝑤 → ( ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ⦋ ( · ‘ 𝑤 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
84 83 cbvralvw ⊢ ( ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑤 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑤 ) / 𝑖 ⦌ 𝐶 ∈ ℂ )
85 id ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → 𝑧 ∈ ( 𝑋 × 𝑌 ) )
86 82 eqcoms ⊢ ( 𝑤 = 𝑧 → ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 = ⦋ ( · ‘ 𝑤 ) / 𝑖 ⦌ 𝐶 )
87 86 adantl ⊢ ( ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑤 = 𝑧 ) → ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 = ⦋ ( · ‘ 𝑤 ) / 𝑖 ⦌ 𝐶 )
88 87 eleq1d ⊢ ( ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑤 = 𝑧 ) → ( ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ⦋ ( · ‘ 𝑤 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
89 53 eleq1d ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
90 89 adantr ⊢ ( ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑤 = 𝑧 ) → ( ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
91 88 90 bitr3d ⊢ ( ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑤 = 𝑧 ) → ( ⦋ ( · ‘ 𝑤 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
92 85 91 rspcdv ⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( ∀ 𝑤 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑤 ) / 𝑖 ⦌ 𝐶 ∈ ℂ → ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
93 92 com12 ⊢ ( ∀ 𝑤 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑤 ) / 𝑖 ⦌ 𝐶 ∈ ℂ → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
94 93 ralrimiv ⊢ ( ∀ 𝑤 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑤 ) / 𝑖 ⦌ 𝐶 ∈ ℂ → ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ )
95 84 94 sylbi ⊢ ( ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( · ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ → ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ )
96 80 95 syl ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ )
97 mpomulf ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ
98 ffn ⊢ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) Fn ( ℂ × ℂ ) )
99 97 98 ax-mp ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) Fn ( ℂ × ℂ )
100 xpss12 ⊢ ( ( 𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ ) → ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) )
101 39 42 100 mp2an ⊢ ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ )
102 71 eleq1d ⊢ ( 𝑤 = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) → ( ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
103 102 ralima ⊢ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) Fn ( ℂ × ℂ ) ∧ ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) ) → ( ∀ 𝑤 ∈ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) “ ( 𝑋 × 𝑌 ) ) ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
104 99 101 103 mp2an ⊢ ( ∀ 𝑤 ∈ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) “ ( 𝑋 × 𝑌 ) ) ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ )
105 df-ima ⊢ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) “ ( 𝑋 × 𝑌 ) ) = ran ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) )
106 f1ofo ⊢ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto→ 𝑍 → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑍 )
107 forn ⊢ ( ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto→ 𝑍 → ran ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) = 𝑍 )
108 74 106 107 3syl ⊢ ( 𝜑 → ran ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ↾ ( 𝑋 × 𝑌 ) ) = 𝑍 )
109 105 108 eqtrid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) “ ( 𝑋 × 𝑌 ) ) = 𝑍 )
110 109 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) “ ( 𝑋 × 𝑌 ) ) ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
111 104 110 bitr3id ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 ∈ ℂ ↔ ∀ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ ) )
112 96 111 mpbid ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ )
113 112 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑍 ) → ⦋ 𝑤 / 𝑖 ⦌ 𝐶 ∈ ℂ )
114 71 73 74 76 113 fsumf1o ⊢ ( 𝜑 → Σ 𝑤 ∈ 𝑍 ⦋ 𝑤 / 𝑖 ⦌ 𝐶 = Σ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 )
115 70 114 eqtrid ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑍 𝐶 = Σ 𝑧 ∈ ( 𝑋 × 𝑌 ) ⦋ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ 𝑧 ) / 𝑖 ⦌ 𝐶 )
116 54 66 115 3eqtr4a ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑋 Σ 𝑘 ∈ 𝑌 𝐷 = Σ 𝑖 ∈ 𝑍 𝐶 )
117 22 29 116 3eqtrd ⊢ ( 𝜑 → ( Σ 𝑗 ∈ 𝑋 𝐴 · Σ 𝑘 ∈ 𝑌 𝐵 ) = Σ 𝑖 ∈ 𝑍 𝐶 )