# Metamath Proof Explorer

## Theorem dchrelbas3

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, 19-Apr-2016)

Ref Expression
Hypotheses dchrval.g ${⊢}{G}=\mathrm{DChr}\left({N}\right)$
dchrval.z ${⊢}{Z}=ℤ/{N}ℤ$
dchrval.b ${⊢}{B}={\mathrm{Base}}_{{Z}}$
dchrval.u ${⊢}{U}=\mathrm{Unit}\left({Z}\right)$
dchrval.n ${⊢}{\phi }\to {N}\in ℕ$
dchrbas.b ${⊢}{D}={\mathrm{Base}}_{{G}}$
Assertion dchrelbas3 ${⊢}{\phi }\to \left({X}\in {D}↔\left({X}:{B}⟶ℂ\wedge \left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 dchrval.g ${⊢}{G}=\mathrm{DChr}\left({N}\right)$
2 dchrval.z ${⊢}{Z}=ℤ/{N}ℤ$
3 dchrval.b ${⊢}{B}={\mathrm{Base}}_{{Z}}$
4 dchrval.u ${⊢}{U}=\mathrm{Unit}\left({Z}\right)$
5 dchrval.n ${⊢}{\phi }\to {N}\in ℕ$
6 dchrbas.b ${⊢}{D}={\mathrm{Base}}_{{G}}$
7 1 2 3 4 5 6 dchrelbas2 ${⊢}{\phi }\to \left({X}\in {D}↔\left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)\right)$
8 fveq2 ${⊢}{z}={x}\to {X}\left({z}\right)={X}\left({x}\right)$
9 8 neeq1d ${⊢}{z}={x}\to \left({X}\left({z}\right)\ne 0↔{X}\left({x}\right)\ne 0\right)$
10 eleq1 ${⊢}{z}={x}\to \left({z}\in {U}↔{x}\in {U}\right)$
11 9 10 imbi12d ${⊢}{z}={x}\to \left(\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)↔\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)$
12 11 cbvralvw ${⊢}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)$
13 5 nnnn0d ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
14 2 zncrng ${⊢}{N}\in {ℕ}_{0}\to {Z}\in \mathrm{CRing}$
15 13 14 syl ${⊢}{\phi }\to {Z}\in \mathrm{CRing}$
16 crngring ${⊢}{Z}\in \mathrm{CRing}\to {Z}\in \mathrm{Ring}$
17 15 16 syl ${⊢}{\phi }\to {Z}\in \mathrm{Ring}$
18 eqid ${⊢}{\mathrm{mulGrp}}_{{Z}}={\mathrm{mulGrp}}_{{Z}}$
19 18 ringmgp ${⊢}{Z}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{Z}}\in \mathrm{Mnd}$
20 17 19 syl ${⊢}{\phi }\to {\mathrm{mulGrp}}_{{Z}}\in \mathrm{Mnd}$
21 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
22 eqid ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$
23 22 ringmgp ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$
24 21 23 ax-mp ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$
25 18 3 mgpbas ${⊢}{B}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Z}}}$
26 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
27 22 26 mgpbas ${⊢}ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$
28 eqid ${⊢}{\cdot }_{{Z}}={\cdot }_{{Z}}$
29 18 28 mgpplusg ${⊢}{\cdot }_{{Z}}={+}_{{\mathrm{mulGrp}}_{{Z}}}$
30 cnfldmul ${⊢}×={\cdot }_{{ℂ}_{\mathrm{fld}}}$
31 22 30 mgpplusg ${⊢}×={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$
32 eqid ${⊢}{1}_{{Z}}={1}_{{Z}}$
33 18 32 ringidval ${⊢}{1}_{{Z}}={0}_{{\mathrm{mulGrp}}_{{Z}}}$
34 cnfld1 ${⊢}1={1}_{{ℂ}_{\mathrm{fld}}}$
35 22 34 ringidval ${⊢}1={0}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$
36 25 27 29 31 33 35 ismhm ${⊢}{X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)↔\left(\left({\mathrm{mulGrp}}_{{Z}}\in \mathrm{Mnd}\wedge {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}\right)\wedge \left({X}:{B}⟶ℂ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\right)$
37 36 baib ${⊢}\left({\mathrm{mulGrp}}_{{Z}}\in \mathrm{Mnd}\wedge {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}\right)\to \left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)↔\left({X}:{B}⟶ℂ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\right)$
38 20 24 37 sylancl ${⊢}{\phi }\to \left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)↔\left({X}:{B}⟶ℂ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\right)$
39 38 adantr ${⊢}\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\to \left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)↔\left({X}:{B}⟶ℂ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\right)$
40 biimt ${⊢}\left({x}\in {U}\wedge {y}\in {U}\right)\to \left({X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)↔\left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)\right)$
41 40 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge \left({x}\in {U}\wedge {y}\in {U}\right)\right)\to \left({X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)↔\left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)\right)$
42 fveq2 ${⊢}{z}={x}{\cdot }_{{Z}}{y}\to {X}\left({z}\right)={X}\left({x}{\cdot }_{{Z}}{y}\right)$
43 42 neeq1d ${⊢}{z}={x}{\cdot }_{{Z}}{y}\to \left({X}\left({z}\right)\ne 0↔{X}\left({x}{\cdot }_{{Z}}{y}\right)\ne 0\right)$
44 eleq1 ${⊢}{z}={x}{\cdot }_{{Z}}{y}\to \left({z}\in {U}↔{x}{\cdot }_{{Z}}{y}\in {U}\right)$
45 43 44 imbi12d ${⊢}{z}={x}{\cdot }_{{Z}}{y}\to \left(\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)↔\left({X}\left({x}{\cdot }_{{Z}}{y}\right)\ne 0\to {x}{\cdot }_{{Z}}{y}\in {U}\right)\right)$
46 simpllr ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)$
47 17 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {Z}\in \mathrm{Ring}$
48 simprl ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}\in {B}$
49 simprr ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {y}\in {B}$
50 3 28 ringcl ${⊢}\left({Z}\in \mathrm{Ring}\wedge {x}\in {B}\wedge {y}\in {B}\right)\to {x}{\cdot }_{{Z}}{y}\in {B}$
51 47 48 49 50 syl3anc ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{Z}}{y}\in {B}$
52 45 46 51 rspcdva ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({X}\left({x}{\cdot }_{{Z}}{y}\right)\ne 0\to {x}{\cdot }_{{Z}}{y}\in {U}\right)$
53 15 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {Z}\in \mathrm{CRing}$
54 4 28 3 unitmulclb ${⊢}\left({Z}\in \mathrm{CRing}\wedge {x}\in {B}\wedge {y}\in {B}\right)\to \left({x}{\cdot }_{{Z}}{y}\in {U}↔\left({x}\in {U}\wedge {y}\in {U}\right)\right)$
55 53 48 49 54 syl3anc ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({x}{\cdot }_{{Z}}{y}\in {U}↔\left({x}\in {U}\wedge {y}\in {U}\right)\right)$
56 52 55 sylibd ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({X}\left({x}{\cdot }_{{Z}}{y}\right)\ne 0\to \left({x}\in {U}\wedge {y}\in {U}\right)\right)$
57 56 necon1bd ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left(¬\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)=0\right)$
58 57 imp ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge ¬\left({x}\in {U}\wedge {y}\in {U}\right)\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)=0$
59 11 46 48 rspcdva ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)$
60 fveq2 ${⊢}{z}={y}\to {X}\left({z}\right)={X}\left({y}\right)$
61 60 neeq1d ${⊢}{z}={y}\to \left({X}\left({z}\right)\ne 0↔{X}\left({y}\right)\ne 0\right)$
62 eleq1 ${⊢}{z}={y}\to \left({z}\in {U}↔{y}\in {U}\right)$
63 61 62 imbi12d ${⊢}{z}={y}\to \left(\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)↔\left({X}\left({y}\right)\ne 0\to {y}\in {U}\right)\right)$
64 63 46 49 rspcdva ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({X}\left({y}\right)\ne 0\to {y}\in {U}\right)$
65 59 64 anim12d ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left(\left({X}\left({x}\right)\ne 0\wedge {X}\left({y}\right)\ne 0\right)\to \left({x}\in {U}\wedge {y}\in {U}\right)\right)$
66 65 con3dimp ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge ¬\left({x}\in {U}\wedge {y}\in {U}\right)\right)\to ¬\left({X}\left({x}\right)\ne 0\wedge {X}\left({y}\right)\ne 0\right)$
67 neanior ${⊢}\left({X}\left({x}\right)\ne 0\wedge {X}\left({y}\right)\ne 0\right)↔¬\left({X}\left({x}\right)=0\vee {X}\left({y}\right)=0\right)$
68 67 con2bii ${⊢}\left({X}\left({x}\right)=0\vee {X}\left({y}\right)=0\right)↔¬\left({X}\left({x}\right)\ne 0\wedge {X}\left({y}\right)\ne 0\right)$
69 66 68 sylibr ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge ¬\left({x}\in {U}\wedge {y}\in {U}\right)\right)\to \left({X}\left({x}\right)=0\vee {X}\left({y}\right)=0\right)$
70 simplr ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {X}:{B}⟶ℂ$
71 70 48 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {X}\left({x}\right)\in ℂ$
72 70 49 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {X}\left({y}\right)\in ℂ$
73 71 72 mul0ord ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({X}\left({x}\right){X}\left({y}\right)=0↔\left({X}\left({x}\right)=0\vee {X}\left({y}\right)=0\right)\right)$
74 73 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge ¬\left({x}\in {U}\wedge {y}\in {U}\right)\right)\to \left({X}\left({x}\right){X}\left({y}\right)=0↔\left({X}\left({x}\right)=0\vee {X}\left({y}\right)=0\right)\right)$
75 69 74 mpbird ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge ¬\left({x}\in {U}\wedge {y}\in {U}\right)\right)\to {X}\left({x}\right){X}\left({y}\right)=0$
76 58 75 eqtr4d ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge ¬\left({x}\in {U}\wedge {y}\in {U}\right)\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)$
77 76 a1d ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge ¬\left({x}\in {U}\wedge {y}\in {U}\right)\right)\to \left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)$
78 76 77 2thd ${⊢}\left(\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\wedge ¬\left({x}\in {U}\wedge {y}\in {U}\right)\right)\to \left({X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)↔\left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)\right)$
79 41 78 pm2.61dan ${⊢}\left(\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to \left({X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)↔\left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)\right)$
80 79 pm5.74da ${⊢}\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\to \left(\left(\left({x}\in {B}\wedge {y}\in {B}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)↔\left(\left({x}\in {B}\wedge {y}\in {B}\right)\to \left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)\right)\right)$
81 3 4 unitcl ${⊢}{x}\in {U}\to {x}\in {B}$
82 3 4 unitcl ${⊢}{y}\in {U}\to {y}\in {B}$
83 81 82 anim12i ${⊢}\left({x}\in {U}\wedge {y}\in {U}\right)\to \left({x}\in {B}\wedge {y}\in {B}\right)$
84 83 pm4.71ri ${⊢}\left({x}\in {U}\wedge {y}\in {U}\right)↔\left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({x}\in {U}\wedge {y}\in {U}\right)\right)$
85 84 imbi1i ${⊢}\left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)↔\left(\left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({x}\in {U}\wedge {y}\in {U}\right)\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)$
86 impexp ${⊢}\left(\left(\left({x}\in {B}\wedge {y}\in {B}\right)\wedge \left({x}\in {U}\wedge {y}\in {U}\right)\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)↔\left(\left({x}\in {B}\wedge {y}\in {B}\right)\to \left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)\right)$
87 85 86 bitri ${⊢}\left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)↔\left(\left({x}\in {B}\wedge {y}\in {B}\right)\to \left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)\right)$
88 80 87 syl6bbr ${⊢}\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\to \left(\left(\left({x}\in {B}\wedge {y}\in {B}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)↔\left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)\right)$
89 88 2albidv ${⊢}\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {B}\wedge {y}\in {B}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)\right)$
90 r2al ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {B}\wedge {y}\in {B}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)$
91 r2al ${⊢}\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {U}\wedge {y}\in {U}\right)\to {X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)$
92 89 90 91 3bitr4g ${⊢}\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge {X}:{B}⟶ℂ\right)\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)↔\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)$
93 92 adantrr ${⊢}\left(\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\wedge \left({X}:{B}⟶ℂ\wedge {X}\left({1}_{{Z}}\right)=1\right)\right)\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)↔\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)$
94 93 pm5.32da ${⊢}\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\to \left(\left(\left({X}:{B}⟶ℂ\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)↔\left(\left({X}:{B}⟶ℂ\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)\right)$
95 3anan32 ${⊢}\left({X}:{B}⟶ℂ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)↔\left(\left({X}:{B}⟶ℂ\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)$
96 an31 ${⊢}\left(\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge {X}:{B}⟶ℂ\right)↔\left(\left({X}:{B}⟶ℂ\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge \forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\right)$
97 94 95 96 3bitr4g ${⊢}\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\to \left(\left({X}:{B}⟶ℂ\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)↔\left(\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge {X}:{B}⟶ℂ\right)\right)$
98 39 97 bitrd ${⊢}\left({\phi }\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({z}\right)\ne 0\to {z}\in {U}\right)\right)\to \left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)↔\left(\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge {X}:{B}⟶ℂ\right)\right)$
99 12 98 sylan2br ${⊢}\left({\phi }\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)\to \left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)↔\left(\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge {X}:{B}⟶ℂ\right)\right)$
100 99 pm5.32da ${⊢}{\phi }\to \left(\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\wedge {X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\right)↔\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\wedge \left(\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge {X}:{B}⟶ℂ\right)\right)\right)$
101 ancom ${⊢}\left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)↔\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\wedge {X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\right)$
102 df-3an ${⊢}\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)↔\left(\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)$
103 102 anbi2i ${⊢}\left({X}:{B}⟶ℂ\wedge \left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)\right)↔\left({X}:{B}⟶ℂ\wedge \left(\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)\right)$
104 an13 ${⊢}\left({X}:{B}⟶ℂ\wedge \left(\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)\right)↔\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\wedge \left(\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge {X}:{B}⟶ℂ\right)\right)$
105 103 104 bitri ${⊢}\left({X}:{B}⟶ℂ\wedge \left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)\right)↔\left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\wedge \left(\left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\right)\wedge {X}:{B}⟶ℂ\right)\right)$
106 100 101 105 3bitr4g ${⊢}{\phi }\to \left(\left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)↔\left({X}:{B}⟶ℂ\wedge \left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)\right)\right)$
107 7 106 bitrd ${⊢}{\phi }\to \left({X}\in {D}↔\left({X}:{B}⟶ℂ\wedge \left(\forall {x}\in {U}\phantom{\rule{.4em}{0ex}}\forall {y}\in {U}\phantom{\rule{.4em}{0ex}}{X}\left({x}{\cdot }_{{Z}}{y}\right)={X}\left({x}\right){X}\left({y}\right)\wedge {X}\left({1}_{{Z}}\right)=1\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)\right)\right)$