Metamath Proof Explorer


Theorem dchrmulcl

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

Ref Expression
Hypotheses dchrmhm.g G = DChr N
dchrmhm.z Z = /N
dchrmhm.b D = Base G
dchrmul.t · ˙ = + G
dchrmul.x φ X D
dchrmul.y φ Y D
Assertion dchrmulcl φ X · ˙ Y D

Proof

Step Hyp Ref Expression
1 dchrmhm.g G = DChr N
2 dchrmhm.z Z = /N
3 dchrmhm.b D = Base G
4 dchrmul.t · ˙ = + G
5 dchrmul.x φ X D
6 dchrmul.y φ Y D
7 1 2 3 4 5 6 dchrmul φ X · ˙ Y = X × f Y
8 mulcl x y x y
9 8 adantl φ x y x y
10 eqid Base Z = Base Z
11 1 2 3 10 5 dchrf φ X : Base Z
12 1 2 3 10 6 dchrf φ Y : Base Z
13 fvexd φ Base Z V
14 inidm Base Z Base Z = Base Z
15 9 11 12 13 13 14 off φ X × f Y : Base Z
16 eqid Unit Z = Unit Z
17 10 16 unitcl x Unit Z x Base Z
18 10 16 unitcl y Unit Z y Base Z
19 17 18 anim12i x Unit Z y Unit Z x Base Z y Base Z
20 1 3 dchrrcl X D N
21 5 20 syl φ N
22 1 2 10 16 21 3 dchrelbas2 φ X D X mulGrp Z MndHom mulGrp fld x Base Z X x 0 x Unit Z
23 5 22 mpbid φ X mulGrp Z MndHom mulGrp fld x Base Z X x 0 x Unit Z
24 23 simpld φ X mulGrp Z MndHom mulGrp fld
25 eqid mulGrp Z = mulGrp Z
26 25 10 mgpbas Base Z = Base mulGrp Z
27 eqid Z = Z
28 25 27 mgpplusg Z = + mulGrp Z
29 eqid mulGrp fld = mulGrp fld
30 cnfldmul × = fld
31 29 30 mgpplusg × = + mulGrp fld
32 26 28 31 mhmlin X mulGrp Z MndHom mulGrp fld x Base Z y Base Z X x Z y = X x X y
33 32 3expb X mulGrp Z MndHom mulGrp fld x Base Z y Base Z X x Z y = X x X y
34 24 33 sylan φ x Base Z y Base Z X x Z y = X x X y
35 1 2 10 16 21 3 dchrelbas2 φ Y D Y mulGrp Z MndHom mulGrp fld x Base Z Y x 0 x Unit Z
36 6 35 mpbid φ Y mulGrp Z MndHom mulGrp fld x Base Z Y x 0 x Unit Z
37 36 simpld φ Y mulGrp Z MndHom mulGrp fld
38 26 28 31 mhmlin Y mulGrp Z MndHom mulGrp fld x Base Z y Base Z Y x Z y = Y x Y y
39 38 3expb Y mulGrp Z MndHom mulGrp fld x Base Z y Base Z Y x Z y = Y x Y y
40 37 39 sylan φ x Base Z y Base Z Y x Z y = Y x Y y
41 34 40 oveq12d φ x Base Z y Base Z X x Z y Y x Z y = X x X y Y x Y y
42 11 ffvelrnda φ x Base Z X x
43 42 adantrr φ x Base Z y Base Z X x
44 simpr x Base Z y Base Z y Base Z
45 ffvelrn X : Base Z y Base Z X y
46 11 44 45 syl2an φ x Base Z y Base Z X y
47 12 ffvelrnda φ x Base Z Y x
48 47 adantrr φ x Base Z y Base Z Y x
49 ffvelrn Y : Base Z y Base Z Y y
50 12 44 49 syl2an φ x Base Z y Base Z Y y
51 43 46 48 50 mul4d φ x Base Z y Base Z X x X y Y x Y y = X x Y x X y Y y
52 41 51 eqtrd φ x Base Z y Base Z X x Z y Y x Z y = X x Y x X y Y y
53 11 ffnd φ X Fn Base Z
54 53 adantr φ x Base Z y Base Z X Fn Base Z
55 12 ffnd φ Y Fn Base Z
56 55 adantr φ x Base Z y Base Z Y Fn Base Z
57 fvexd φ x Base Z y Base Z Base Z V
58 21 nnnn0d φ N 0
59 2 zncrng N 0 Z CRing
60 crngring Z CRing Z Ring
61 58 59 60 3syl φ Z Ring
62 10 27 ringcl Z Ring x Base Z y Base Z x Z y Base Z
63 62 3expb Z Ring x Base Z y Base Z x Z y Base Z
64 61 63 sylan φ x Base Z y Base Z x Z y Base Z
65 fnfvof X Fn Base Z Y Fn Base Z Base Z V x Z y Base Z X × f Y x Z y = X x Z y Y x Z y
66 54 56 57 64 65 syl22anc φ x Base Z y Base Z X × f Y x Z y = X x Z y Y x Z y
67 53 adantr φ x Base Z X Fn Base Z
68 55 adantr φ x Base Z Y Fn Base Z
69 fvexd φ x Base Z Base Z V
70 simpr φ x Base Z x Base Z
71 fnfvof X Fn Base Z Y Fn Base Z Base Z V x Base Z X × f Y x = X x Y x
72 67 68 69 70 71 syl22anc φ x Base Z X × f Y x = X x Y x
73 72 adantrr φ x Base Z y Base Z X × f Y x = X x Y x
74 simprr φ x Base Z y Base Z y Base Z
75 fnfvof X Fn Base Z Y Fn Base Z Base Z V y Base Z X × f Y y = X y Y y
76 54 56 57 74 75 syl22anc φ x Base Z y Base Z X × f Y y = X y Y y
77 73 76 oveq12d φ x Base Z y Base Z X × f Y x X × f Y y = X x Y x X y Y y
78 52 66 77 3eqtr4d φ x Base Z y Base Z X × f Y x Z y = X × f Y x X × f Y y
79 19 78 sylan2 φ x Unit Z y Unit Z X × f Y x Z y = X × f Y x X × f Y y
80 79 ralrimivva φ x Unit Z y Unit Z X × f Y x Z y = X × f Y x X × f Y y
81 eqid 1 Z = 1 Z
82 10 81 ringidcl Z Ring 1 Z Base Z
83 61 82 syl φ 1 Z Base Z
84 fnfvof X Fn Base Z Y Fn Base Z Base Z V 1 Z Base Z X × f Y 1 Z = X 1 Z Y 1 Z
85 53 55 13 83 84 syl22anc φ X × f Y 1 Z = X 1 Z Y 1 Z
86 25 81 ringidval 1 Z = 0 mulGrp Z
87 cnfld1 1 = 1 fld
88 29 87 ringidval 1 = 0 mulGrp fld
89 86 88 mhm0 X mulGrp Z MndHom mulGrp fld X 1 Z = 1
90 24 89 syl φ X 1 Z = 1
91 86 88 mhm0 Y mulGrp Z MndHom mulGrp fld Y 1 Z = 1
92 37 91 syl φ Y 1 Z = 1
93 90 92 oveq12d φ X 1 Z Y 1 Z = 1 1
94 1t1e1 1 1 = 1
95 93 94 eqtrdi φ X 1 Z Y 1 Z = 1
96 85 95 eqtrd φ X × f Y 1 Z = 1
97 72 neeq1d φ x Base Z X × f Y x 0 X x Y x 0
98 42 47 mulne0bd φ x Base Z X x 0 Y x 0 X x Y x 0
99 97 98 bitr4d φ x Base Z X × f Y x 0 X x 0 Y x 0
100 23 simprd φ x Base Z X x 0 x Unit Z
101 100 r19.21bi φ x Base Z X x 0 x Unit Z
102 101 adantrd φ x Base Z X x 0 Y x 0 x Unit Z
103 99 102 sylbid φ x Base Z X × f Y x 0 x Unit Z
104 103 ralrimiva φ x Base Z X × f Y x 0 x Unit Z
105 80 96 104 3jca φ x Unit Z y Unit Z X × f Y x Z y = X × f Y x X × f Y y X × f Y 1 Z = 1 x Base Z X × f Y x 0 x Unit Z
106 1 2 10 16 21 3 dchrelbas3 φ X × f Y D X × f Y : Base Z x Unit Z y Unit Z X × f Y x Z y = X × f Y x X × f Y y X × f Y 1 Z = 1 x Base Z X × f Y x 0 x Unit Z
107 15 105 106 mpbir2and φ X × f Y D
108 7 107 eqeltrd φ X · ˙ Y D