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 = DChr (N)$
	dchrval.z	$⊢ Z = ℤ / N ℤ$
	dchrval.b	$⊢ B = {Base}_{Z}$
	dchrval.u	$⊢ U = Unit (Z)$
	dchrval.n	$⊢ φ \to N \in ℕ$
	dchrbas.b	$⊢ D = {Base}_{G}$
Assertion	dchrelbas3	$⊢ φ \to (X \in D \leftrightarrow (X : B ⟶ ℂ \land (\forall x \in U \forall y \in U X (x \cdot_{Z} y) = X (x) X (y) \land X (1_{Z}) = 1 \land \forall x \in B (X (x) \neq 0 \to x \in U))))$

Proof

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

Metamath Proof Explorer

Theorem dchrelbas3

Proof