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

Metamath Proof Explorer

Theorem dchrsum2

Description: An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character X is 0 if X is non-principal and phi ( n ) otherwise. Part of Theorem 6.5.1 of Shapiro p. 230. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrsum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrsum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrsum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrsum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
dchrsum.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrsum2.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
Assertion dchrsum2 ( 𝜑 → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) )

Proof

Step Hyp Ref Expression
1 dchrsum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrsum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrsum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchrsum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
5 dchrsum.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
6 dchrsum2.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
7 eqeq2 ⊢ ( ( ϕ ‘ 𝑁 ) = if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) → ( Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = ( ϕ ‘ 𝑁 ) ↔ Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) ) )
8 eqeq2 ⊢ ( 0 = if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) → ( Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = 0 ↔ Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) ) )
9 fveq1 ⊢ ( 𝑋 = 1 → ( 𝑋 ‘ 𝑎 ) = ( 1 ‘ 𝑎 ) )
10 1 3 dchrrcl ⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
11 5 10 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) → 𝑁 ∈ ℕ )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) → 𝑎 ∈ 𝑈 )
14 1 2 4 6 12 13 dchr1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) → ( 1 ‘ 𝑎 ) = 1 )
15 9 14 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) ∧ 𝑋 = 1 ) → ( 𝑋 ‘ 𝑎 ) = 1 )
16 15 an32s ⊢ ( ( ( 𝜑 ∧ 𝑋 = 1 ) ∧ 𝑎 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑎 ) = 1 )
17 16 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑋 = 1 ) → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = Σ 𝑎 ∈ 𝑈 1 )
18 2 6 znunithash ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝑈 ) = ( ϕ ‘ 𝑁 ) )
19 11 18 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ϕ ‘ 𝑁 ) )
20 11 phicld ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ )
21 20 nnnn0d ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
22 19 21 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
23 6 fvexi ⊢ 𝑈 ∈ V
24 hashclb ⊢ ( 𝑈 ∈ V → ( 𝑈 ∈ Fin ↔ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ) )
25 23 24 ax-mp ⊢ ( 𝑈 ∈ Fin ↔ ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
26 22 25 sylibr ⊢ ( 𝜑 → 𝑈 ∈ Fin )
27 ax-1cn ⊢ 1 ∈ ℂ
28 fsumconst ⊢ ( ( 𝑈 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑎 ∈ 𝑈 1 = ( ( ♯ ‘ 𝑈 ) · 1 ) )
29 26 27 28 sylancl ⊢ ( 𝜑 → Σ 𝑎 ∈ 𝑈 1 = ( ( ♯ ‘ 𝑈 ) · 1 ) )
30 19 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) · 1 ) = ( ( ϕ ‘ 𝑁 ) · 1 ) )
31 20 nncnd ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℂ )
32 31 mulridd ⊢ ( 𝜑 → ( ( ϕ ‘ 𝑁 ) · 1 ) = ( ϕ ‘ 𝑁 ) )
33 29 30 32 3eqtrd ⊢ ( 𝜑 → Σ 𝑎 ∈ 𝑈 1 = ( ϕ ‘ 𝑁 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 1 ) → Σ 𝑎 ∈ 𝑈 1 = ( ϕ ‘ 𝑁 ) )
35 17 34 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 1 ) → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = ( ϕ ‘ 𝑁 ) )
36 1 dchrabl ⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
37 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
38 3 4 grpidcl ⊢ ( 𝐺 ∈ Grp → 1 ∈ 𝐷 )
39 11 36 37 38 4syl ⊢ ( 𝜑 → 1 ∈ 𝐷 )
40 1 2 3 6 5 39 dchreq ⊢ ( 𝜑 → ( 𝑋 = 1 ↔ ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 1 ‘ 𝑘 ) ) )
41 40 notbid ⊢ ( 𝜑 → ( ¬ 𝑋 = 1 ↔ ¬ ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 1 ‘ 𝑘 ) ) )
42 rexnal ⊢ ( ∃ 𝑘 ∈ 𝑈 ¬ ( 𝑋 ‘ 𝑘 ) = ( 1 ‘ 𝑘 ) ↔ ¬ ∀ 𝑘 ∈ 𝑈 ( 𝑋 ‘ 𝑘 ) = ( 1 ‘ 𝑘 ) )
43 41 42 bitr4di ⊢ ( 𝜑 → ( ¬ 𝑋 = 1 ↔ ∃ 𝑘 ∈ 𝑈 ¬ ( 𝑋 ‘ 𝑘 ) = ( 1 ‘ 𝑘 ) ) )
44 df-ne ⊢ ( ( 𝑋 ‘ 𝑘 ) ≠ ( 1 ‘ 𝑘 ) ↔ ¬ ( 𝑋 ‘ 𝑘 ) = ( 1 ‘ 𝑘 ) )
45 11 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝑁 ∈ ℕ )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 𝑘 ∈ 𝑈 )
47 1 2 4 6 45 46 dchr1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( 1 ‘ 𝑘 ) = 1 )
48 47 neeq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( ( 𝑋 ‘ 𝑘 ) ≠ ( 1 ‘ 𝑘 ) ↔ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) )
49 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → 𝑈 ∈ Fin )
50 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
51 1 2 3 50 5 dchrf ⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
52 50 6 unitss ⊢ 𝑈 ⊆ ( Base ‘ 𝑍 )
53 52 sseli ⊢ ( 𝑎 ∈ 𝑈 → 𝑎 ∈ ( Base ‘ 𝑍 ) )
54 ffvelcdm ⊢ ( ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ 𝑎 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ 𝑎 ) ∈ ℂ )
55 51 53 54 syl2an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑎 ) ∈ ℂ )
56 55 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) ∧ 𝑎 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑎 ) ∈ ℂ )
57 49 56 fsumcl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ∈ ℂ )
58 0cnd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → 0 ∈ ℂ )
59 51 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
60 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → 𝑘 ∈ 𝑈 )
61 52 60 sselid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → 𝑘 ∈ ( Base ‘ 𝑍 ) )
62 59 61 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( 𝑋 ‘ 𝑘 ) ∈ ℂ )
63 subcl ⊢ ( ( ( 𝑋 ‘ 𝑘 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑋 ‘ 𝑘 ) − 1 ) ∈ ℂ )
64 62 27 63 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( 𝑋 ‘ 𝑘 ) − 1 ) ∈ ℂ )
65 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( 𝑋 ‘ 𝑘 ) ≠ 1 )
66 subeq0 ⊢ ( ( ( 𝑋 ‘ 𝑘 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝑋 ‘ 𝑘 ) − 1 ) = 0 ↔ ( 𝑋 ‘ 𝑘 ) = 1 ) )
67 62 27 66 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( ( 𝑋 ‘ 𝑘 ) − 1 ) = 0 ↔ ( 𝑋 ‘ 𝑘 ) = 1 ) )
68 67 necon3bid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( ( 𝑋 ‘ 𝑘 ) − 1 ) ≠ 0 ↔ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) )
69 65 68 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( 𝑋 ‘ 𝑘 ) − 1 ) ≠ 0 )
70 oveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑘 ( .r ‘ 𝑍 ) 𝑥 ) = ( 𝑘 ( .r ‘ 𝑍 ) 𝑎 ) )
71 70 fveq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑋 ‘ ( 𝑘 ( .r ‘ 𝑍 ) 𝑥 ) ) = ( 𝑋 ‘ ( 𝑘 ( .r ‘ 𝑍 ) 𝑎 ) ) )
72 71 cbvsumv ⊢ Σ 𝑥 ∈ 𝑈 ( 𝑋 ‘ ( 𝑘 ( .r ‘ 𝑍 ) 𝑥 ) ) = Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ ( 𝑘 ( .r ‘ 𝑍 ) 𝑎 ) )
73 1 2 3 dchrmhm ⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
74 73 5 sselid ⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
75 74 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) ∧ 𝑎 ∈ 𝑈 ) → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
76 61 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) ∧ 𝑎 ∈ 𝑈 ) → 𝑘 ∈ ( Base ‘ 𝑍 ) )
77 53 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) ∧ 𝑎 ∈ 𝑈 ) → 𝑎 ∈ ( Base ‘ 𝑍 ) )
78 eqid ⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
79 78 50 mgpbas ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ ( mulGrp ‘ 𝑍 ) )
80 eqid ⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 )
81 78 80 mgpplusg ⊢ ( .r ‘ 𝑍 ) = ( +g ‘ ( mulGrp ‘ 𝑍 ) )
82 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
83 cnfldmul ⊢ · = ( .r ‘ ℂfld )
84 82 83 mgpplusg ⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
85 79 81 84 mhmlin ⊢ ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝑘 ∈ ( Base ‘ 𝑍 ) ∧ 𝑎 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ ( 𝑘 ( .r ‘ 𝑍 ) 𝑎 ) ) = ( ( 𝑋 ‘ 𝑘 ) · ( 𝑋 ‘ 𝑎 ) ) )
86 75 76 77 85 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) ∧ 𝑎 ∈ 𝑈 ) → ( 𝑋 ‘ ( 𝑘 ( .r ‘ 𝑍 ) 𝑎 ) ) = ( ( 𝑋 ‘ 𝑘 ) · ( 𝑋 ‘ 𝑎 ) ) )
87 86 sumeq2dv ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ ( 𝑘 ( .r ‘ 𝑍 ) 𝑎 ) ) = Σ 𝑎 ∈ 𝑈 ( ( 𝑋 ‘ 𝑘 ) · ( 𝑋 ‘ 𝑎 ) ) )
88 72 87 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → Σ 𝑥 ∈ 𝑈 ( 𝑋 ‘ ( 𝑘 ( .r ‘ 𝑍 ) 𝑥 ) ) = Σ 𝑎 ∈ 𝑈 ( ( 𝑋 ‘ 𝑘 ) · ( 𝑋 ‘ 𝑎 ) ) )
89 fveq2 ⊢ ( 𝑎 = ( 𝑘 ( .r ‘ 𝑍 ) 𝑥 ) → ( 𝑋 ‘ 𝑎 ) = ( 𝑋 ‘ ( 𝑘 ( .r ‘ 𝑍 ) 𝑥 ) ) )
90 11 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
91 2 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
92 crngring ⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
93 eqid ⊢ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
94 6 93 unitgrp ⊢ ( 𝑍 ∈ Ring → ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp )
95 90 91 92 94 4syl ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp )
96 eqid ⊢ ( 𝑏 ∈ 𝑈 ↦ ( 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( .r ‘ 𝑍 ) 𝑐 ) ) ) = ( 𝑏 ∈ 𝑈 ↦ ( 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( .r ‘ 𝑍 ) 𝑐 ) ) )
97 6 93 unitgrpbas ⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
98 93 81 ressplusg ⊢ ( 𝑈 ∈ V → ( .r ‘ 𝑍 ) = ( +g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) )
99 23 98 ax-mp ⊢ ( .r ‘ 𝑍 ) = ( +g ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) )
100 96 97 99 grplactf1o ⊢ ( ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑘 ∈ 𝑈 ) → ( ( 𝑏 ∈ 𝑈 ↦ ( 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( .r ‘ 𝑍 ) 𝑐 ) ) ) ‘ 𝑘 ) : 𝑈 –1-1-onto→ 𝑈 )
101 95 60 100 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( 𝑏 ∈ 𝑈 ↦ ( 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( .r ‘ 𝑍 ) 𝑐 ) ) ) ‘ 𝑘 ) : 𝑈 –1-1-onto→ 𝑈 )
102 96 97 grplactval ⊢ ( ( 𝑘 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) → ( ( ( 𝑏 ∈ 𝑈 ↦ ( 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( .r ‘ 𝑍 ) 𝑐 ) ) ) ‘ 𝑘 ) ‘ 𝑥 ) = ( 𝑘 ( .r ‘ 𝑍 ) 𝑥 ) )
103 60 102 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) ∧ 𝑥 ∈ 𝑈 ) → ( ( ( 𝑏 ∈ 𝑈 ↦ ( 𝑐 ∈ 𝑈 ↦ ( 𝑏 ( .r ‘ 𝑍 ) 𝑐 ) ) ) ‘ 𝑘 ) ‘ 𝑥 ) = ( 𝑘 ( .r ‘ 𝑍 ) 𝑥 ) )
104 89 49 101 103 56 fsumf1o ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = Σ 𝑥 ∈ 𝑈 ( 𝑋 ‘ ( 𝑘 ( .r ‘ 𝑍 ) 𝑥 ) ) )
105 49 62 56 fsummulc2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( 𝑋 ‘ 𝑘 ) · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) = Σ 𝑎 ∈ 𝑈 ( ( 𝑋 ‘ 𝑘 ) · ( 𝑋 ‘ 𝑎 ) ) )
106 88 104 105 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( 𝑋 ‘ 𝑘 ) · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) = Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) )
107 57 mullidd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( 1 · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) = Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) )
108 106 107 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( ( 𝑋 ‘ 𝑘 ) · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) − ( 1 · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) ) = ( Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) − Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) )
109 57 subidd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) − Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) = 0 )
110 108 109 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( ( 𝑋 ‘ 𝑘 ) · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) − ( 1 · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) ) = 0 )
111 1cnd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → 1 ∈ ℂ )
112 62 111 57 subdird ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( ( 𝑋 ‘ 𝑘 ) − 1 ) · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) = ( ( ( 𝑋 ‘ 𝑘 ) · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) − ( 1 · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) ) )
113 64 mul01d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( ( 𝑋 ‘ 𝑘 ) − 1 ) · 0 ) = 0 )
114 110 112 113 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → ( ( ( 𝑋 ‘ 𝑘 ) − 1 ) · Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) ) = ( ( ( 𝑋 ‘ 𝑘 ) − 1 ) · 0 ) )
115 57 58 64 69 114 mulcanad ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = 0 )
116 115 expr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( ( 𝑋 ‘ 𝑘 ) ≠ 1 → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = 0 ) )
117 48 116 sylbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( ( 𝑋 ‘ 𝑘 ) ≠ ( 1 ‘ 𝑘 ) → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = 0 ) )
118 44 117 biimtrrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( ¬ ( 𝑋 ‘ 𝑘 ) = ( 1 ‘ 𝑘 ) → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = 0 ) )
119 118 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑈 ¬ ( 𝑋 ‘ 𝑘 ) = ( 1 ‘ 𝑘 ) → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = 0 ) )
120 43 119 sylbid ⊢ ( 𝜑 → ( ¬ 𝑋 = 1 → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = 0 ) )
121 120 imp ⊢ ( ( 𝜑 ∧ ¬ 𝑋 = 1 ) → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = 0 )
122 7 8 35 121 ifbothda ⊢ ( 𝜑 → Σ 𝑎 ∈ 𝑈 ( 𝑋 ‘ 𝑎 ) = if ( 𝑋 = 1 , ( ϕ ‘ 𝑁 ) , 0 ) )