Metamath Proof Explorer


Theorem dchrelbas2

Description: A Dirichlet character is a monoid homomorphism from the multiplicative monoid on Z/nZ to the multiplicative monoid of CC , which is zero off the group of units of Z/nZ . (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrval.g G=DChrN
dchrval.z Z=/N
dchrval.b B=BaseZ
dchrval.u U=UnitZ
dchrval.n φN
dchrbas.b D=BaseG
Assertion dchrelbas2 φXDXmulGrpZMndHommulGrpfldxBXx0xU

Proof

Step Hyp Ref Expression
1 dchrval.g G=DChrN
2 dchrval.z Z=/N
3 dchrval.b B=BaseZ
4 dchrval.u U=UnitZ
5 dchrval.n φN
6 dchrbas.b D=BaseG
7 1 2 3 4 5 6 dchrelbas φXDXmulGrpZMndHommulGrpfldBU×0X
8 eqid mulGrpZ=mulGrpZ
9 8 3 mgpbas B=BasemulGrpZ
10 eqid mulGrpfld=mulGrpfld
11 cnfldbas =Basefld
12 10 11 mgpbas =BasemulGrpfld
13 9 12 mhmf XmulGrpZMndHommulGrpfldX:B
14 13 adantl φXmulGrpZMndHommulGrpfldX:B
15 14 ffund φXmulGrpZMndHommulGrpfldFunX
16 funssres FunXBU×0XXdomBU×0=BU×0
17 15 16 sylan φXmulGrpZMndHommulGrpfldBU×0XXdomBU×0=BU×0
18 simpr φXmulGrpZMndHommulGrpfldXdomBU×0=BU×0XdomBU×0=BU×0
19 resss XdomBU×0X
20 18 19 eqsstrrdi φXmulGrpZMndHommulGrpfldXdomBU×0=BU×0BU×0X
21 17 20 impbida φXmulGrpZMndHommulGrpfldBU×0XXdomBU×0=BU×0
22 0cn 0
23 fconst6g 0BU×0:BU
24 22 23 mp1i φXmulGrpZMndHommulGrpfldBU×0:BU
25 24 fdmd φXmulGrpZMndHommulGrpflddomBU×0=BU
26 25 reseq2d φXmulGrpZMndHommulGrpfldXdomBU×0=XBU
27 26 eqeq1d φXmulGrpZMndHommulGrpfldXdomBU×0=BU×0XBU=BU×0
28 difss BUB
29 fssres X:BBUBXBU:BU
30 14 28 29 sylancl φXmulGrpZMndHommulGrpfldXBU:BU
31 30 ffnd φXmulGrpZMndHommulGrpfldXBUFnBU
32 24 ffnd φXmulGrpZMndHommulGrpfldBU×0FnBU
33 eqfnfv XBUFnBUBU×0FnBUXBU=BU×0xBUXBUx=BU×0x
34 31 32 33 syl2anc φXmulGrpZMndHommulGrpfldXBU=BU×0xBUXBUx=BU×0x
35 fvres xBUXBUx=Xx
36 c0ex 0V
37 36 fvconst2 xBUBU×0x=0
38 35 37 eqeq12d xBUXBUx=BU×0xXx=0
39 38 ralbiia xBUXBUx=BU×0xxBUXx=0
40 eldif xBUxB¬xU
41 40 imbi1i xBUXx=0xB¬xUXx=0
42 impexp xB¬xUXx=0xB¬xUXx=0
43 con1b ¬xUXx=0¬Xx=0xU
44 df-ne Xx0¬Xx=0
45 44 imbi1i Xx0xU¬Xx=0xU
46 43 45 bitr4i ¬xUXx=0Xx0xU
47 46 imbi2i xB¬xUXx=0xBXx0xU
48 41 42 47 3bitri xBUXx=0xBXx0xU
49 48 ralbii2 xBUXx=0xBXx0xU
50 39 49 bitri xBUXBUx=BU×0xxBXx0xU
51 34 50 bitrdi φXmulGrpZMndHommulGrpfldXBU=BU×0xBXx0xU
52 21 27 51 3bitrd φXmulGrpZMndHommulGrpfldBU×0XxBXx0xU
53 52 pm5.32da φXmulGrpZMndHommulGrpfldBU×0XXmulGrpZMndHommulGrpfldxBXx0xU
54 7 53 bitrd φXDXmulGrpZMndHommulGrpfldxBXx0xU