Metamath Proof Explorer


Theorem dchrinvcl

Description: Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g G=DChrN
dchrmhm.z Z=/N
dchrmhm.b D=BaseG
dchrn0.b B=BaseZ
dchrn0.u U=UnitZ
dchr1cl.o 1˙=kBifkU10
dchrmulid2.t ·˙=+G
dchrmulid2.x φXD
dchrinvcl.n K=kBifkU1Xk0
Assertion dchrinvcl φKDK·˙X=1˙

Proof

Step Hyp Ref Expression
1 dchrmhm.g G=DChrN
2 dchrmhm.z Z=/N
3 dchrmhm.b D=BaseG
4 dchrn0.b B=BaseZ
5 dchrn0.u U=UnitZ
6 dchr1cl.o 1˙=kBifkU10
7 dchrmulid2.t ·˙=+G
8 dchrmulid2.x φXD
9 dchrinvcl.n K=kBifkU1Xk0
10 1 3 dchrrcl XDN
11 8 10 syl φN
12 fveq2 k=xXk=Xx
13 12 oveq2d k=x1Xk=1Xx
14 fveq2 k=yXk=Xy
15 14 oveq2d k=y1Xk=1Xy
16 fveq2 k=xZyXk=XxZy
17 16 oveq2d k=xZy1Xk=1XxZy
18 fveq2 k=1ZXk=X1Z
19 18 oveq2d k=1Z1Xk=1X1Z
20 1 2 3 4 8 dchrf φX:B
21 4 5 unitss UB
22 21 sseli kUkB
23 ffvelrn X:BkBXk
24 20 22 23 syl2an φkUXk
25 simpr φkUkU
26 8 adantr φkUXD
27 22 adantl φkUkB
28 1 2 3 4 5 26 27 dchrn0 φkUXk0kU
29 25 28 mpbird φkUXk0
30 24 29 reccld φkU1Xk
31 1t1e1 11=1
32 31 eqcomi 1=11
33 32 a1i φxUyU1=11
34 1 2 3 dchrmhm DmulGrpZMndHommulGrpfld
35 8 adantr φxUyUXD
36 34 35 sselid φxUyUXmulGrpZMndHommulGrpfld
37 simprl φxUyUxU
38 21 37 sselid φxUyUxB
39 simprr φxUyUyU
40 21 39 sselid φxUyUyB
41 eqid mulGrpZ=mulGrpZ
42 41 4 mgpbas B=BasemulGrpZ
43 eqid Z=Z
44 41 43 mgpplusg Z=+mulGrpZ
45 eqid mulGrpfld=mulGrpfld
46 cnfldmul ×=fld
47 45 46 mgpplusg ×=+mulGrpfld
48 42 44 47 mhmlin XmulGrpZMndHommulGrpfldxByBXxZy=XxXy
49 36 38 40 48 syl3anc φxUyUXxZy=XxXy
50 33 49 oveq12d φxUyU1XxZy=11XxXy
51 1cnd φxUyU1
52 20 adantr φxUyUX:B
53 52 38 ffvelrnd φxUyUXx
54 52 40 ffvelrnd φxUyUXy
55 1 2 3 4 5 35 38 dchrn0 φxUyUXx0xU
56 37 55 mpbird φxUyUXx0
57 1 2 3 4 5 35 40 dchrn0 φxUyUXy0yU
58 39 57 mpbird φxUyUXy0
59 51 53 51 54 56 58 divmuldivd φxUyU1Xx1Xy=11XxXy
60 50 59 eqtr4d φxUyU1XxZy=1Xx1Xy
61 34 8 sselid φXmulGrpZMndHommulGrpfld
62 eqid 1Z=1Z
63 41 62 ringidval 1Z=0mulGrpZ
64 cnfld1 1=1fld
65 45 64 ringidval 1=0mulGrpfld
66 63 65 mhm0 XmulGrpZMndHommulGrpfldX1Z=1
67 61 66 syl φX1Z=1
68 67 oveq2d φ1X1Z=11
69 1div1e1 11=1
70 68 69 eqtrdi φ1X1Z=1
71 1 2 4 5 11 3 13 15 17 19 30 60 70 dchrelbasd φkBifkU1Xk0D
72 9 71 eqeltrid φKD
73 1 2 3 7 72 8 dchrmul φK·˙X=K×fX
74 4 fvexi BV
75 74 a1i φBV
76 ovex 1XkV
77 c0ex 0V
78 76 77 ifex ifkU1Xk0V
79 78 a1i φkBifkU1Xk0V
80 20 ffvelrnda φkBXk
81 9 a1i φK=kBifkU1Xk0
82 20 feqmptd φX=kBXk
83 75 79 80 81 82 offval2 φK×fX=kBifkU1Xk0Xk
84 ovif ifkU1Xk0Xk=ifkU1XkXk0Xk
85 80 adantr φkBkUXk
86 8 adantr φkBXD
87 simpr φkBkB
88 1 2 3 4 5 86 87 dchrn0 φkBXk0kU
89 88 biimpar φkBkUXk0
90 85 89 recid2d φkBkU1XkXk=1
91 90 ifeq1da φkBifkU1XkXk0Xk=ifkU10Xk
92 80 mul02d φkB0Xk=0
93 92 ifeq2d φkBifkU10Xk=ifkU10
94 91 93 eqtrd φkBifkU1XkXk0Xk=ifkU10
95 84 94 eqtrid φkBifkU1Xk0Xk=ifkU10
96 95 mpteq2dva φkBifkU1Xk0Xk=kBifkU10
97 6 96 eqtr4id φ1˙=kBifkU1Xk0Xk
98 83 97 eqtr4d φK×fX=1˙
99 73 98 eqtrd φK·˙X=1˙
100 72 99 jca φKDK·˙X=1˙