Metamath Proof Explorer


Theorem dchrinv

Description: The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of X are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrabs.g G=DChrN
dchrabs.d D=BaseG
dchrabs.x φXD
dchrinv.i I=invgG
Assertion dchrinv φIX=*X

Proof

Step Hyp Ref Expression
1 dchrabs.g G=DChrN
2 dchrabs.d D=BaseG
3 dchrabs.x φXD
4 dchrinv.i I=invgG
5 eqid /N=/N
6 eqid +G=+G
7 cjf *:
8 eqid Base/N=Base/N
9 1 5 2 8 3 dchrf φX:Base/N
10 fco *:X:Base/N*X:Base/N
11 7 9 10 sylancr φ*X:Base/N
12 eqid Unit/N=Unit/N
13 1 2 dchrrcl XDN
14 3 13 syl φN
15 1 5 8 12 14 2 dchrelbas3 φXDX:Base/NxUnit/NyUnit/NXx/Ny=XxXyX1/N=1xBase/NXx0xUnit/N
16 3 15 mpbid φX:Base/NxUnit/NyUnit/NXx/Ny=XxXyX1/N=1xBase/NXx0xUnit/N
17 16 simprd φxUnit/NyUnit/NXx/Ny=XxXyX1/N=1xBase/NXx0xUnit/N
18 17 simp1d φxUnit/NyUnit/NXx/Ny=XxXy
19 18 r19.21bi φxUnit/NyUnit/NXx/Ny=XxXy
20 19 r19.21bi φxUnit/NyUnit/NXx/Ny=XxXy
21 20 anasss φxUnit/NyUnit/NXx/Ny=XxXy
22 21 fveq2d φxUnit/NyUnit/NXx/Ny=XxXy
23 9 adantr φxUnit/NyUnit/NX:Base/N
24 8 12 unitss Unit/NBase/N
25 simprl φxUnit/NyUnit/NxUnit/N
26 24 25 sselid φxUnit/NyUnit/NxBase/N
27 23 26 ffvelrnd φxUnit/NyUnit/NXx
28 simprr φxUnit/NyUnit/NyUnit/N
29 24 28 sselid φxUnit/NyUnit/NyBase/N
30 23 29 ffvelrnd φxUnit/NyUnit/NXy
31 27 30 cjmuld φxUnit/NyUnit/NXxXy=XxXy
32 22 31 eqtrd φxUnit/NyUnit/NXx/Ny=XxXy
33 14 nnnn0d φN0
34 5 zncrng N0/NCRing
35 crngring /NCRing/NRing
36 33 34 35 3syl φ/NRing
37 36 adantr φxUnit/NyUnit/N/NRing
38 eqid /N=/N
39 8 38 ringcl /NRingxBase/NyBase/Nx/NyBase/N
40 37 26 29 39 syl3anc φxUnit/NyUnit/Nx/NyBase/N
41 fvco3 X:Base/Nx/NyBase/N*Xx/Ny=Xx/Ny
42 23 40 41 syl2anc φxUnit/NyUnit/N*Xx/Ny=Xx/Ny
43 fvco3 X:Base/NxBase/N*Xx=Xx
44 23 26 43 syl2anc φxUnit/NyUnit/N*Xx=Xx
45 fvco3 X:Base/NyBase/N*Xy=Xy
46 23 29 45 syl2anc φxUnit/NyUnit/N*Xy=Xy
47 44 46 oveq12d φxUnit/NyUnit/N*Xx*Xy=XxXy
48 32 42 47 3eqtr4d φxUnit/NyUnit/N*Xx/Ny=*Xx*Xy
49 48 ralrimivva φxUnit/NyUnit/N*Xx/Ny=*Xx*Xy
50 eqid 1/N=1/N
51 8 50 ringidcl /NRing1/NBase/N
52 36 51 syl φ1/NBase/N
53 fvco3 X:Base/N1/NBase/N*X1/N=X1/N
54 9 52 53 syl2anc φ*X1/N=X1/N
55 17 simp2d φX1/N=1
56 55 fveq2d φX1/N=1
57 1re 1
58 cjre 11=1
59 57 58 ax-mp 1=1
60 56 59 eqtrdi φX1/N=1
61 54 60 eqtrd φ*X1/N=1
62 17 simp3d φxBase/NXx0xUnit/N
63 9 43 sylan φxBase/N*Xx=Xx
64 cj0 0=0
65 64 eqcomi 0=0
66 65 a1i φxBase/N0=0
67 63 66 eqeq12d φxBase/N*Xx=0Xx=0
68 9 ffvelrnda φxBase/NXx
69 0cn 0
70 cj11 Xx0Xx=0Xx=0
71 68 69 70 sylancl φxBase/NXx=0Xx=0
72 67 71 bitrd φxBase/N*Xx=0Xx=0
73 72 necon3bid φxBase/N*Xx0Xx0
74 73 imbi1d φxBase/N*Xx0xUnit/NXx0xUnit/N
75 74 ralbidva φxBase/N*Xx0xUnit/NxBase/NXx0xUnit/N
76 62 75 mpbird φxBase/N*Xx0xUnit/N
77 49 61 76 3jca φxUnit/NyUnit/N*Xx/Ny=*Xx*Xy*X1/N=1xBase/N*Xx0xUnit/N
78 1 5 8 12 14 2 dchrelbas3 φ*XD*X:Base/NxUnit/NyUnit/N*Xx/Ny=*Xx*Xy*X1/N=1xBase/N*Xx0xUnit/N
79 11 77 78 mpbir2and φ*XD
80 1 5 2 6 3 79 dchrmul φX+G*X=X×f*X
81 80 adantr φxUnit/NX+G*X=X×f*X
82 81 fveq1d φxUnit/NX+G*Xx=X×f*Xx
83 24 sseli xUnit/NxBase/N
84 83 63 sylan2 φxUnit/N*Xx=Xx
85 84 oveq2d φxUnit/NXx*Xx=XxXx
86 83 68 sylan2 φxUnit/NXx
87 86 absvalsqd φxUnit/NXx2=XxXx
88 3 adantr φxUnit/NXD
89 simpr φxUnit/NxUnit/N
90 1 2 88 5 12 89 dchrabs φxUnit/NXx=1
91 90 oveq1d φxUnit/NXx2=12
92 sq1 12=1
93 91 92 eqtrdi φxUnit/NXx2=1
94 85 87 93 3eqtr2d φxUnit/NXx*Xx=1
95 9 adantr φxUnit/NX:Base/N
96 95 ffnd φxUnit/NXFnBase/N
97 11 ffnd φ*XFnBase/N
98 97 adantr φxUnit/N*XFnBase/N
99 fvexd φxUnit/NBase/NV
100 83 adantl φxUnit/NxBase/N
101 fnfvof XFnBase/N*XFnBase/NBase/NVxBase/NX×f*Xx=Xx*Xx
102 96 98 99 100 101 syl22anc φxUnit/NX×f*Xx=Xx*Xx
103 eqid 0G=0G
104 14 adantr φxUnit/NN
105 1 5 103 12 104 89 dchr1 φxUnit/N0Gx=1
106 94 102 105 3eqtr4d φxUnit/NX×f*Xx=0Gx
107 82 106 eqtrd φxUnit/NX+G*Xx=0Gx
108 107 ralrimiva φxUnit/NX+G*Xx=0Gx
109 1 5 2 6 3 79 dchrmulcl φX+G*XD
110 1 dchrabl NGAbel
111 ablgrp GAbelGGrp
112 14 110 111 3syl φGGrp
113 2 103 grpidcl GGrp0GD
114 112 113 syl φ0GD
115 1 5 2 12 109 114 dchreq φX+G*X=0GxUnit/NX+G*Xx=0Gx
116 108 115 mpbird φX+G*X=0G
117 2 6 103 4 grpinvid1 GGrpXD*XDIX=*XX+G*X=0G
118 112 3 79 117 syl3anc φIX=*XX+G*X=0G
119 116 118 mpbird φIX=*X