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

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 ⊢ 𝐺 = ( 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 → 𝑥 ∈ 𝑈 ) ) ) ) )