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	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrval.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrval.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
	dchrval.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
	dchrval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dchrbas.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
Assertion	dchrelbas3	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 : 𝐵 ⟶ ℂ ∧ ( ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) ) ) )

Proof

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