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 = ( 0_g ‘ 𝐺 )
	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 = ( 0_g ‘ 𝐺 )
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	⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ₀ )
22	19 21	eqeltrd	⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) ∈ ℕ₀ )
23	6	fvexi	⊢ 𝑈 ∈ V
24		hashclb	⊢ ( 𝑈 ∈ V → ( 𝑈 ∈ Fin ↔ ( ♯ ‘ 𝑈 ) ∈ ℕ₀ ) )
25	23 24	ax-mp	⊢ ( 𝑈 ∈ Fin ↔ ( ♯ ‘ 𝑈 ) ∈ ℕ₀ )
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	mulid1d	⊢ ( 𝜑 → ( ( ϕ ‘ 𝑁 ) · 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		ffvelrn	⊢ ( ( 𝑋 : ( 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	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 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	syl5eq	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 1 ) ) → Σ 𝑥 ∈ 𝑈 ( 𝑋 ‘ ( 𝑘 ( ._r ‘ 𝑍 ) 𝑥 ) ) = Σ 𝑎 ∈ 𝑈 ( ( 𝑋 ‘ 𝑘 ) · ( 𝑋 ‘ 𝑎 ) ) )
89		fveq2	⊢ ( 𝑎 = ( 𝑘 ( ._r ‘ 𝑍 ) 𝑥 ) → ( 𝑋 ‘ 𝑎 ) = ( 𝑋 ‘ ( 𝑘 ( ._r ‘ 𝑍 ) 𝑥 ) ) )
90	11	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
91	2	zncrng	⊢ ( 𝑁 ∈ ℕ₀ → 𝑍 ∈ 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	mulid2d	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑈 ∧ ( 𝑋 ‘ 𝑘 ) ≠ 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	syl5bir	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → ( ¬ ( 𝑋 ‘ 𝑘 ) = ( 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 ) )

Metamath Proof Explorer

Theorem dchrsum2

Proof