Step |
Hyp |
Ref |
Expression |
1 |
|
sum2dchr.g |
⊢ 𝐺 = ( DChr ‘ 𝑁 ) |
2 |
|
sum2dchr.d |
⊢ 𝐷 = ( Base ‘ 𝐺 ) |
3 |
|
sum2dchr.z |
⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 ) |
4 |
|
sum2dchr.b |
⊢ 𝐵 = ( Base ‘ 𝑍 ) |
5 |
|
sum2dchr.u |
⊢ 𝑈 = ( Unit ‘ 𝑍 ) |
6 |
|
sum2dchr.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
7 |
|
sum2dchr.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) |
8 |
|
sum2dchr.c |
⊢ ( 𝜑 → 𝐶 ∈ 𝑈 ) |
9 |
|
eqid |
⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 ) |
10 |
6
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
11 |
3
|
zncrng |
⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing ) |
12 |
|
crngring |
⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring ) |
13 |
10 11 12
|
3syl |
⊢ ( 𝜑 → 𝑍 ∈ Ring ) |
14 |
|
eqid |
⊢ ( /r ‘ 𝑍 ) = ( /r ‘ 𝑍 ) |
15 |
4 5 14
|
dvrcl |
⊢ ( ( 𝑍 ∈ Ring ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ∈ 𝐵 ) |
16 |
13 7 8 15
|
syl3anc |
⊢ ( 𝜑 → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ∈ 𝐵 ) |
17 |
1 2 3 9 4 6 16
|
sumdchr |
⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = if ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) , ( ϕ ‘ 𝑁 ) , 0 ) ) |
18 |
|
eqid |
⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 ) |
19 |
|
eqid |
⊢ ( invr ‘ 𝑍 ) = ( invr ‘ 𝑍 ) |
20 |
4 18 5 19 14
|
dvrval |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) |
21 |
7 8 20
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) |
22 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) |
23 |
22
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = ( 𝑥 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) ) |
24 |
1 3 2
|
dchrmhm |
⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) |
25 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 ) |
26 |
24 25
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ) |
27 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝐵 ) |
28 |
4 5
|
unitss |
⊢ 𝑈 ⊆ 𝐵 |
29 |
5 19
|
unitinvcl |
⊢ ( ( 𝑍 ∈ Ring ∧ 𝐶 ∈ 𝑈 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝑈 ) |
30 |
13 8 29
|
syl2anc |
⊢ ( 𝜑 → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝑈 ) |
31 |
30
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝑈 ) |
32 |
28 31
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝐵 ) |
33 |
|
eqid |
⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 ) |
34 |
33 4
|
mgpbas |
⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑍 ) ) |
35 |
33 18
|
mgpplusg |
⊢ ( .r ‘ 𝑍 ) = ( +g ‘ ( mulGrp ‘ 𝑍 ) ) |
36 |
|
eqid |
⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld ) |
37 |
|
cnfldmul |
⊢ · = ( .r ‘ ℂfld ) |
38 |
36 37
|
mgpplusg |
⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) ) |
39 |
34 35 38
|
mhmlin |
⊢ ( ( 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝐴 ∈ 𝐵 ∧ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ∈ 𝐵 ) → ( 𝑥 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) ) |
40 |
26 27 32 39
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) ) |
41 |
|
eqid |
⊢ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) |
42 |
|
eqid |
⊢ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) |
43 |
1 3 2 5 41 42 25
|
dchrghm |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↾ 𝑈 ) ∈ ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ) |
44 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐶 ∈ 𝑈 ) |
45 |
5 41
|
unitgrpbas |
⊢ 𝑈 = ( Base ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) |
46 |
5 41 19
|
invrfval |
⊢ ( invr ‘ 𝑍 ) = ( invg ‘ ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) ) |
47 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
48 |
|
cnfld0 |
⊢ 0 = ( 0g ‘ ℂfld ) |
49 |
|
cndrng |
⊢ ℂfld ∈ DivRing |
50 |
47 48 49
|
drngui |
⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld ) |
51 |
|
eqid |
⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld ) |
52 |
50 42 51
|
invrfval |
⊢ ( invr ‘ ℂfld ) = ( invg ‘ ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) |
53 |
45 46 52
|
ghminv |
⊢ ( ( ( 𝑥 ↾ 𝑈 ) ∈ ( ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 ) GrpHom ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) ) ) ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) ) |
54 |
43 44 53
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) ) |
55 |
31
|
fvresd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) |
56 |
44
|
fvresd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) = ( 𝑥 ‘ 𝐶 ) ) |
57 |
56
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) = ( ( invr ‘ ℂfld ) ‘ ( 𝑥 ‘ 𝐶 ) ) ) |
58 |
1 3 2 4 25
|
dchrf |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 : 𝐵 ⟶ ℂ ) |
59 |
28 44
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐶 ∈ 𝐵 ) |
60 |
58 59
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ 𝐶 ) ∈ ℂ ) |
61 |
1 3 2 4 5 25 59
|
dchrn0 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ‘ 𝐶 ) ≠ 0 ↔ 𝐶 ∈ 𝑈 ) ) |
62 |
44 61
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ 𝐶 ) ≠ 0 ) |
63 |
|
cnfldinv |
⊢ ( ( ( 𝑥 ‘ 𝐶 ) ∈ ℂ ∧ ( 𝑥 ‘ 𝐶 ) ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ ( 𝑥 ‘ 𝐶 ) ) = ( 1 / ( 𝑥 ‘ 𝐶 ) ) ) |
64 |
60 62 63
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ ℂfld ) ‘ ( 𝑥 ‘ 𝐶 ) ) = ( 1 / ( 𝑥 ‘ 𝐶 ) ) ) |
65 |
|
recval |
⊢ ( ( ( 𝑥 ‘ 𝐶 ) ∈ ℂ ∧ ( 𝑥 ‘ 𝐶 ) ≠ 0 ) → ( 1 / ( 𝑥 ‘ 𝐶 ) ) = ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) ) ) |
66 |
60 62 65
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 1 / ( 𝑥 ‘ 𝐶 ) ) = ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) ) ) |
67 |
1 2 25 3 5 44
|
dchrabs |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) = 1 ) |
68 |
67
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) = ( 1 ↑ 2 ) ) |
69 |
|
sq1 |
⊢ ( 1 ↑ 2 ) = 1 |
70 |
68 69
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) = 1 ) |
71 |
70
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / ( ( abs ‘ ( 𝑥 ‘ 𝐶 ) ) ↑ 2 ) ) = ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / 1 ) ) |
72 |
60
|
cjcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ∈ ℂ ) |
73 |
72
|
div1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) / 1 ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) |
74 |
66 71 73
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 1 / ( 𝑥 ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) |
75 |
57 64 74
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( invr ‘ ℂfld ) ‘ ( ( 𝑥 ↾ 𝑈 ) ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) |
76 |
54 55 75
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) = ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) |
77 |
76
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑥 ‘ 𝐴 ) · ( 𝑥 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐶 ) ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) ) |
78 |
23 40 77
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) ) |
79 |
78
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( 𝑥 ‘ ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) ) = Σ 𝑥 ∈ 𝐷 ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) ) |
80 |
4 5 14 9
|
dvreq1 |
⊢ ( ( 𝑍 ∈ Ring ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝑈 ) → ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) ↔ 𝐴 = 𝐶 ) ) |
81 |
13 7 8 80
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) ↔ 𝐴 = 𝐶 ) ) |
82 |
81
|
ifbid |
⊢ ( 𝜑 → if ( ( 𝐴 ( /r ‘ 𝑍 ) 𝐶 ) = ( 1r ‘ 𝑍 ) , ( ϕ ‘ 𝑁 ) , 0 ) = if ( 𝐴 = 𝐶 , ( ϕ ‘ 𝑁 ) , 0 ) ) |
83 |
17 79 82
|
3eqtr3d |
⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐷 ( ( 𝑥 ‘ 𝐴 ) · ( ∗ ‘ ( 𝑥 ‘ 𝐶 ) ) ) = if ( 𝐴 = 𝐶 , ( ϕ ‘ 𝑁 ) , 0 ) ) |