This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( Z/nZ ` N )
dchrmhm.b 
|- D = ( Base ` G )
dchrmul.t 
|- .x. = ( +g ` G )
dchrmul.x 
|- ( ph -> X e. D )
dchrmul.y 
|- ( ph -> Y e. D )
Assertion dchrmulcl 
|- ( ph -> ( X .x. Y ) e. D )

Proof

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