Step | Hyp | Ref
| Expression |
1 | | sum2dchr.g |
. . 3
β’ πΊ = (DChrβπ) |
2 | | sum2dchr.d |
. . 3
β’ π· = (BaseβπΊ) |
3 | | sum2dchr.z |
. . 3
β’ π =
(β€/nβ€βπ) |
4 | | eqid 2737 |
. . 3
β’
(1rβπ) = (1rβπ) |
5 | | sum2dchr.b |
. . 3
β’ π΅ = (Baseβπ) |
6 | | sum2dchr.n |
. . 3
β’ (π β π β β) |
7 | 6 | nnnn0d 12480 |
. . . . 5
β’ (π β π β
β0) |
8 | 3 | zncrng 20967 |
. . . . 5
β’ (π β β0
β π β
CRing) |
9 | | crngring 19983 |
. . . . 5
β’ (π β CRing β π β Ring) |
10 | 7, 8, 9 | 3syl 18 |
. . . 4
β’ (π β π β Ring) |
11 | | sum2dchr.a |
. . . 4
β’ (π β π΄ β π΅) |
12 | | sum2dchr.c |
. . . 4
β’ (π β πΆ β π) |
13 | | sum2dchr.u |
. . . . 5
β’ π = (Unitβπ) |
14 | | eqid 2737 |
. . . . 5
β’
(/rβπ) = (/rβπ) |
15 | 5, 13, 14 | dvrcl 20122 |
. . . 4
β’ ((π β Ring β§ π΄ β π΅ β§ πΆ β π) β (π΄(/rβπ)πΆ) β π΅) |
16 | 10, 11, 12, 15 | syl3anc 1372 |
. . 3
β’ (π β (π΄(/rβπ)πΆ) β π΅) |
17 | 1, 2, 3, 4, 5, 6, 16 | sumdchr 26636 |
. 2
β’ (π β Ξ£π₯ β π· (π₯β(π΄(/rβπ)πΆ)) = if((π΄(/rβπ)πΆ) = (1rβπ), (Οβπ), 0)) |
18 | | eqid 2737 |
. . . . . . . 8
β’
(.rβπ) = (.rβπ) |
19 | | eqid 2737 |
. . . . . . . 8
β’
(invrβπ) = (invrβπ) |
20 | 5, 18, 13, 19, 14 | dvrval 20121 |
. . . . . . 7
β’ ((π΄ β π΅ β§ πΆ β π) β (π΄(/rβπ)πΆ) = (π΄(.rβπ)((invrβπ)βπΆ))) |
21 | 11, 12, 20 | syl2anc 585 |
. . . . . 6
β’ (π β (π΄(/rβπ)πΆ) = (π΄(.rβπ)((invrβπ)βπΆ))) |
22 | 21 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π·) β (π΄(/rβπ)πΆ) = (π΄(.rβπ)((invrβπ)βπΆ))) |
23 | 22 | fveq2d 6851 |
. . . 4
β’ ((π β§ π₯ β π·) β (π₯β(π΄(/rβπ)πΆ)) = (π₯β(π΄(.rβπ)((invrβπ)βπΆ)))) |
24 | 1, 3, 2 | dchrmhm 26605 |
. . . . . 6
β’ π· β ((mulGrpβπ) MndHom
(mulGrpββfld)) |
25 | | simpr 486 |
. . . . . 6
β’ ((π β§ π₯ β π·) β π₯ β π·) |
26 | 24, 25 | sselid 3947 |
. . . . 5
β’ ((π β§ π₯ β π·) β π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
27 | 11 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π·) β π΄ β π΅) |
28 | 5, 13 | unitss 20096 |
. . . . . 6
β’ π β π΅ |
29 | 13, 19 | unitinvcl 20110 |
. . . . . . . 8
β’ ((π β Ring β§ πΆ β π) β ((invrβπ)βπΆ) β π) |
30 | 10, 12, 29 | syl2anc 585 |
. . . . . . 7
β’ (π β
((invrβπ)βπΆ) β π) |
31 | 30 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π·) β ((invrβπ)βπΆ) β π) |
32 | 28, 31 | sselid 3947 |
. . . . 5
β’ ((π β§ π₯ β π·) β ((invrβπ)βπΆ) β π΅) |
33 | | eqid 2737 |
. . . . . . 7
β’
(mulGrpβπ) =
(mulGrpβπ) |
34 | 33, 5 | mgpbas 19909 |
. . . . . 6
β’ π΅ =
(Baseβ(mulGrpβπ)) |
35 | 33, 18 | mgpplusg 19907 |
. . . . . 6
β’
(.rβπ) = (+gβ(mulGrpβπ)) |
36 | | eqid 2737 |
. . . . . . 7
β’
(mulGrpββfld) =
(mulGrpββfld) |
37 | | cnfldmul 20818 |
. . . . . . 7
β’ Β·
= (.rββfld) |
38 | 36, 37 | mgpplusg 19907 |
. . . . . 6
β’ Β·
= (+gβ(mulGrpββfld)) |
39 | 34, 35, 38 | mhmlin 18616 |
. . . . 5
β’ ((π₯ β ((mulGrpβπ) MndHom
(mulGrpββfld)) β§ π΄ β π΅ β§ ((invrβπ)βπΆ) β π΅) β (π₯β(π΄(.rβπ)((invrβπ)βπΆ))) = ((π₯βπ΄) Β· (π₯β((invrβπ)βπΆ)))) |
40 | 26, 27, 32, 39 | syl3anc 1372 |
. . . 4
β’ ((π β§ π₯ β π·) β (π₯β(π΄(.rβπ)((invrβπ)βπΆ))) = ((π₯βπ΄) Β· (π₯β((invrβπ)βπΆ)))) |
41 | | eqid 2737 |
. . . . . . . 8
β’
((mulGrpβπ)
βΎs π) =
((mulGrpβπ)
βΎs π) |
42 | | eqid 2737 |
. . . . . . . 8
β’
((mulGrpββfld) βΎs (β
β {0})) = ((mulGrpββfld) βΎs
(β β {0})) |
43 | 1, 3, 2, 13, 41, 42, 25 | dchrghm 26620 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β (π₯ βΎ π) β (((mulGrpβπ) βΎs π) GrpHom
((mulGrpββfld) βΎs (β β
{0})))) |
44 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β πΆ β π) |
45 | 13, 41 | unitgrpbas 20102 |
. . . . . . . 8
β’ π =
(Baseβ((mulGrpβπ) βΎs π)) |
46 | 13, 41, 19 | invrfval 20109 |
. . . . . . . 8
β’
(invrβπ) =
(invgβ((mulGrpβπ) βΎs π)) |
47 | | cnfldbas 20816 |
. . . . . . . . . 10
β’ β =
(Baseββfld) |
48 | | cnfld0 20837 |
. . . . . . . . . 10
β’ 0 =
(0gββfld) |
49 | | cndrng 20842 |
. . . . . . . . . 10
β’
βfld β DivRing |
50 | 47, 48, 49 | drngui 20205 |
. . . . . . . . 9
β’ (β
β {0}) = (Unitββfld) |
51 | | eqid 2737 |
. . . . . . . . 9
β’
(invrββfld) =
(invrββfld) |
52 | 50, 42, 51 | invrfval 20109 |
. . . . . . . 8
β’
(invrββfld) =
(invgβ((mulGrpββfld)
βΎs (β β {0}))) |
53 | 45, 46, 52 | ghminv 19022 |
. . . . . . 7
β’ (((π₯ βΎ π) β (((mulGrpβπ) βΎs π) GrpHom
((mulGrpββfld) βΎs (β β
{0}))) β§ πΆ β π) β ((π₯ βΎ π)β((invrβπ)βπΆ)) =
((invrββfld)β((π₯ βΎ π)βπΆ))) |
54 | 43, 44, 53 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π₯ β π·) β ((π₯ βΎ π)β((invrβπ)βπΆ)) =
((invrββfld)β((π₯ βΎ π)βπΆ))) |
55 | 31 | fvresd 6867 |
. . . . . 6
β’ ((π β§ π₯ β π·) β ((π₯ βΎ π)β((invrβπ)βπΆ)) = (π₯β((invrβπ)βπΆ))) |
56 | 44 | fvresd 6867 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β ((π₯ βΎ π)βπΆ) = (π₯βπΆ)) |
57 | 56 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β
((invrββfld)β((π₯ βΎ π)βπΆ)) =
((invrββfld)β(π₯βπΆ))) |
58 | 1, 3, 2, 5, 25 | dchrf 26606 |
. . . . . . . . 9
β’ ((π β§ π₯ β π·) β π₯:π΅βΆβ) |
59 | 28, 44 | sselid 3947 |
. . . . . . . . 9
β’ ((π β§ π₯ β π·) β πΆ β π΅) |
60 | 58, 59 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β (π₯βπΆ) β β) |
61 | 1, 3, 2, 5, 13, 25, 59 | dchrn0 26614 |
. . . . . . . . 9
β’ ((π β§ π₯ β π·) β ((π₯βπΆ) β 0 β πΆ β π)) |
62 | 44, 61 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β (π₯βπΆ) β 0) |
63 | | cnfldinv 20844 |
. . . . . . . 8
β’ (((π₯βπΆ) β β β§ (π₯βπΆ) β 0) β
((invrββfld)β(π₯βπΆ)) = (1 / (π₯βπΆ))) |
64 | 60, 62, 63 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β
((invrββfld)β(π₯βπΆ)) = (1 / (π₯βπΆ))) |
65 | | recval 15214 |
. . . . . . . . 9
β’ (((π₯βπΆ) β β β§ (π₯βπΆ) β 0) β (1 / (π₯βπΆ)) = ((ββ(π₯βπΆ)) / ((absβ(π₯βπΆ))β2))) |
66 | 60, 62, 65 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β (1 / (π₯βπΆ)) = ((ββ(π₯βπΆ)) / ((absβ(π₯βπΆ))β2))) |
67 | 1, 2, 25, 3, 13, 44 | dchrabs 26624 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π·) β (absβ(π₯βπΆ)) = 1) |
68 | 67 | oveq1d 7377 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π·) β ((absβ(π₯βπΆ))β2) = (1β2)) |
69 | | sq1 14106 |
. . . . . . . . . 10
β’
(1β2) = 1 |
70 | 68, 69 | eqtrdi 2793 |
. . . . . . . . 9
β’ ((π β§ π₯ β π·) β ((absβ(π₯βπΆ))β2) = 1) |
71 | 70 | oveq2d 7378 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β ((ββ(π₯βπΆ)) / ((absβ(π₯βπΆ))β2)) = ((ββ(π₯βπΆ)) / 1)) |
72 | 60 | cjcld 15088 |
. . . . . . . . 9
β’ ((π β§ π₯ β π·) β (ββ(π₯βπΆ)) β β) |
73 | 72 | div1d 11930 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β ((ββ(π₯βπΆ)) / 1) = (ββ(π₯βπΆ))) |
74 | 66, 71, 73 | 3eqtrd 2781 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β (1 / (π₯βπΆ)) = (ββ(π₯βπΆ))) |
75 | 57, 64, 74 | 3eqtrd 2781 |
. . . . . 6
β’ ((π β§ π₯ β π·) β
((invrββfld)β((π₯ βΎ π)βπΆ)) = (ββ(π₯βπΆ))) |
76 | 54, 55, 75 | 3eqtr3d 2785 |
. . . . 5
β’ ((π β§ π₯ β π·) β (π₯β((invrβπ)βπΆ)) = (ββ(π₯βπΆ))) |
77 | 76 | oveq2d 7378 |
. . . 4
β’ ((π β§ π₯ β π·) β ((π₯βπ΄) Β· (π₯β((invrβπ)βπΆ))) = ((π₯βπ΄) Β· (ββ(π₯βπΆ)))) |
78 | 23, 40, 77 | 3eqtrd 2781 |
. . 3
β’ ((π β§ π₯ β π·) β (π₯β(π΄(/rβπ)πΆ)) = ((π₯βπ΄) Β· (ββ(π₯βπΆ)))) |
79 | 78 | sumeq2dv 15595 |
. 2
β’ (π β Ξ£π₯ β π· (π₯β(π΄(/rβπ)πΆ)) = Ξ£π₯ β π· ((π₯βπ΄) Β· (ββ(π₯βπΆ)))) |
80 | 5, 13, 14, 4 | dvreq1 20129 |
. . . 4
β’ ((π β Ring β§ π΄ β π΅ β§ πΆ β π) β ((π΄(/rβπ)πΆ) = (1rβπ) β π΄ = πΆ)) |
81 | 10, 11, 12, 80 | syl3anc 1372 |
. . 3
β’ (π β ((π΄(/rβπ)πΆ) = (1rβπ) β π΄ = πΆ)) |
82 | 81 | ifbid 4514 |
. 2
β’ (π β if((π΄(/rβπ)πΆ) = (1rβπ), (Οβπ), 0) = if(π΄ = πΆ, (Οβπ), 0)) |
83 | 17, 79, 82 | 3eqtr3d 2785 |
1
β’ (π β Ξ£π₯ β π· ((π₯βπ΄) Β· (ββ(π₯βπΆ))) = if(π΄ = πΆ, (Οβπ), 0)) |