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=DChrN
dchrmhm.z Z=/N
dchrmhm.b D=BaseG
dchrmul.t ·˙=+G
dchrmul.x φXD
dchrmul.y φYD
Assertion dchrmulcl φX·˙YD

Proof

Step Hyp Ref Expression
1 dchrmhm.g G=DChrN
2 dchrmhm.z Z=/N
3 dchrmhm.b D=BaseG
4 dchrmul.t ·˙=+G
5 dchrmul.x φXD
6 dchrmul.y φYD
7 1 2 3 4 5 6 dchrmul φX·˙Y=X×fY
8 mulcl xyxy
9 8 adantl φxyxy
10 eqid BaseZ=BaseZ
11 1 2 3 10 5 dchrf φX:BaseZ
12 1 2 3 10 6 dchrf φY:BaseZ
13 fvexd φBaseZV
14 inidm BaseZBaseZ=BaseZ
15 9 11 12 13 13 14 off φX×fY:BaseZ
16 eqid UnitZ=UnitZ
17 10 16 unitcl xUnitZxBaseZ
18 10 16 unitcl yUnitZyBaseZ
19 17 18 anim12i xUnitZyUnitZxBaseZyBaseZ
20 1 3 dchrrcl XDN
21 5 20 syl φN
22 1 2 10 16 21 3 dchrelbas2 φXDXmulGrpZMndHommulGrpfldxBaseZXx0xUnitZ
23 5 22 mpbid φXmulGrpZMndHommulGrpfldxBaseZXx0xUnitZ
24 23 simpld φXmulGrpZMndHommulGrpfld
25 eqid mulGrpZ=mulGrpZ
26 25 10 mgpbas BaseZ=BasemulGrpZ
27 eqid Z=Z
28 25 27 mgpplusg Z=+mulGrpZ
29 eqid mulGrpfld=mulGrpfld
30 cnfldmul ×=fld
31 29 30 mgpplusg ×=+mulGrpfld
32 26 28 31 mhmlin XmulGrpZMndHommulGrpfldxBaseZyBaseZXxZy=XxXy
33 32 3expb XmulGrpZMndHommulGrpfldxBaseZyBaseZXxZy=XxXy
34 24 33 sylan φxBaseZyBaseZXxZy=XxXy
35 1 2 10 16 21 3 dchrelbas2 φYDYmulGrpZMndHommulGrpfldxBaseZYx0xUnitZ
36 6 35 mpbid φYmulGrpZMndHommulGrpfldxBaseZYx0xUnitZ
37 36 simpld φYmulGrpZMndHommulGrpfld
38 26 28 31 mhmlin YmulGrpZMndHommulGrpfldxBaseZyBaseZYxZy=YxYy
39 38 3expb YmulGrpZMndHommulGrpfldxBaseZyBaseZYxZy=YxYy
40 37 39 sylan φxBaseZyBaseZYxZy=YxYy
41 34 40 oveq12d φxBaseZyBaseZXxZyYxZy=XxXyYxYy
42 11 ffvelrnda φxBaseZXx
43 42 adantrr φxBaseZyBaseZXx
44 simpr xBaseZyBaseZyBaseZ
45 ffvelrn X:BaseZyBaseZXy
46 11 44 45 syl2an φxBaseZyBaseZXy
47 12 ffvelrnda φxBaseZYx
48 47 adantrr φxBaseZyBaseZYx
49 ffvelrn Y:BaseZyBaseZYy
50 12 44 49 syl2an φxBaseZyBaseZYy
51 43 46 48 50 mul4d φxBaseZyBaseZXxXyYxYy=XxYxXyYy
52 41 51 eqtrd φxBaseZyBaseZXxZyYxZy=XxYxXyYy
53 11 ffnd φXFnBaseZ
54 53 adantr φxBaseZyBaseZXFnBaseZ
55 12 ffnd φYFnBaseZ
56 55 adantr φxBaseZyBaseZYFnBaseZ
57 fvexd φxBaseZyBaseZBaseZV
58 21 nnnn0d φN0
59 2 zncrng N0ZCRing
60 crngring ZCRingZRing
61 58 59 60 3syl φZRing
62 10 27 ringcl ZRingxBaseZyBaseZxZyBaseZ
63 62 3expb ZRingxBaseZyBaseZxZyBaseZ
64 61 63 sylan φxBaseZyBaseZxZyBaseZ
65 fnfvof XFnBaseZYFnBaseZBaseZVxZyBaseZX×fYxZy=XxZyYxZy
66 54 56 57 64 65 syl22anc φxBaseZyBaseZX×fYxZy=XxZyYxZy
67 53 adantr φxBaseZXFnBaseZ
68 55 adantr φxBaseZYFnBaseZ
69 fvexd φxBaseZBaseZV
70 simpr φxBaseZxBaseZ
71 fnfvof XFnBaseZYFnBaseZBaseZVxBaseZX×fYx=XxYx
72 67 68 69 70 71 syl22anc φxBaseZX×fYx=XxYx
73 72 adantrr φxBaseZyBaseZX×fYx=XxYx
74 simprr φxBaseZyBaseZyBaseZ
75 fnfvof XFnBaseZYFnBaseZBaseZVyBaseZX×fYy=XyYy
76 54 56 57 74 75 syl22anc φxBaseZyBaseZX×fYy=XyYy
77 73 76 oveq12d φxBaseZyBaseZX×fYxX×fYy=XxYxXyYy
78 52 66 77 3eqtr4d φxBaseZyBaseZX×fYxZy=X×fYxX×fYy
79 19 78 sylan2 φxUnitZyUnitZX×fYxZy=X×fYxX×fYy
80 79 ralrimivva φxUnitZyUnitZX×fYxZy=X×fYxX×fYy
81 eqid 1Z=1Z
82 10 81 ringidcl ZRing1ZBaseZ
83 61 82 syl φ1ZBaseZ
84 fnfvof XFnBaseZYFnBaseZBaseZV1ZBaseZX×fY1Z=X1ZY1Z
85 53 55 13 83 84 syl22anc φX×fY1Z=X1ZY1Z
86 25 81 ringidval 1Z=0mulGrpZ
87 cnfld1 1=1fld
88 29 87 ringidval 1=0mulGrpfld
89 86 88 mhm0 XmulGrpZMndHommulGrpfldX1Z=1
90 24 89 syl φX1Z=1
91 86 88 mhm0 YmulGrpZMndHommulGrpfldY1Z=1
92 37 91 syl φY1Z=1
93 90 92 oveq12d φX1ZY1Z=11
94 1t1e1 11=1
95 93 94 eqtrdi φX1ZY1Z=1
96 85 95 eqtrd φX×fY1Z=1
97 72 neeq1d φxBaseZX×fYx0XxYx0
98 42 47 mulne0bd φxBaseZXx0Yx0XxYx0
99 97 98 bitr4d φxBaseZX×fYx0Xx0Yx0
100 23 simprd φxBaseZXx0xUnitZ
101 100 r19.21bi φxBaseZXx0xUnitZ
102 101 adantrd φxBaseZXx0Yx0xUnitZ
103 99 102 sylbid φxBaseZX×fYx0xUnitZ
104 103 ralrimiva φxBaseZX×fYx0xUnitZ
105 80 96 104 3jca φxUnitZyUnitZX×fYxZy=X×fYxX×fYyX×fY1Z=1xBaseZX×fYx0xUnitZ
106 1 2 10 16 21 3 dchrelbas3 φX×fYDX×fY:BaseZxUnitZyUnitZX×fYxZy=X×fYxX×fYyX×fY1Z=1xBaseZX×fYx0xUnitZ
107 15 105 106 mpbir2and φX×fYD
108 7 107 eqeltrd φX·˙YD