Metamath Proof Explorer


Theorem dchrmulcl

Description: Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g 𝐺 = ( DChr ‘ 𝑁 )
dchrmhm.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrmhm.b 𝐷 = ( Base ‘ 𝐺 )
dchrmul.t · = ( +g𝐺 )
dchrmul.x ( 𝜑𝑋𝐷 )
dchrmul.y ( 𝜑𝑌𝐷 )
Assertion dchrmulcl ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 dchrmhm.g 𝐺 = ( DChr ‘ 𝑁 )
2 dchrmhm.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrmhm.b 𝐷 = ( Base ‘ 𝐺 )
4 dchrmul.t · = ( +g𝐺 )
5 dchrmul.x ( 𝜑𝑋𝐷 )
6 dchrmul.y ( 𝜑𝑌𝐷 )
7 1 2 3 4 5 6 dchrmul ( 𝜑 → ( 𝑋 · 𝑌 ) = ( 𝑋f · 𝑌 ) )
8 mulcl ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
9 8 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
10 eqid ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
11 1 2 3 10 5 dchrf ( 𝜑𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
12 1 2 3 10 6 dchrf ( 𝜑𝑌 : ( Base ‘ 𝑍 ) ⟶ ℂ )
13 fvexd ( 𝜑 → ( Base ‘ 𝑍 ) ∈ V )
14 inidm ( ( Base ‘ 𝑍 ) ∩ ( Base ‘ 𝑍 ) ) = ( Base ‘ 𝑍 )
15 9 11 12 13 13 14 off ( 𝜑 → ( 𝑋f · 𝑌 ) : ( Base ‘ 𝑍 ) ⟶ ℂ )
16 eqid ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
17 10 16 unitcl ( 𝑥 ∈ ( Unit ‘ 𝑍 ) → 𝑥 ∈ ( Base ‘ 𝑍 ) )
18 10 16 unitcl ( 𝑦 ∈ ( Unit ‘ 𝑍 ) → 𝑦 ∈ ( Base ‘ 𝑍 ) )
19 17 18 anim12i ( ( 𝑥 ∈ ( Unit ‘ 𝑍 ) ∧ 𝑦 ∈ ( Unit ‘ 𝑍 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) )
20 1 3 dchrrcl ( 𝑋𝐷𝑁 ∈ ℕ )
21 5 20 syl ( 𝜑𝑁 ∈ ℕ )
22 1 2 10 16 21 3 dchrelbas2 ( 𝜑 → ( 𝑋𝐷 ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( ( 𝑋𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) ) )
23 5 22 mpbid ( 𝜑 → ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( ( 𝑋𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) )
24 23 simpld ( 𝜑𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
25 eqid ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
26 25 10 mgpbas ( Base ‘ 𝑍 ) = ( Base ‘ ( mulGrp ‘ 𝑍 ) )
27 eqid ( .r𝑍 ) = ( .r𝑍 )
28 25 27 mgpplusg ( .r𝑍 ) = ( +g ‘ ( mulGrp ‘ 𝑍 ) )
29 eqid ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
30 cnfldmul · = ( .r ‘ ℂfld )
31 29 30 mgpplusg · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
32 26 28 31 mhmlin ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( 𝑋𝑥 ) · ( 𝑋𝑦 ) ) )
33 32 3expb ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( 𝑋𝑥 ) · ( 𝑋𝑦 ) ) )
34 24 33 sylan ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( 𝑋𝑥 ) · ( 𝑋𝑦 ) ) )
35 1 2 10 16 21 3 dchrelbas2 ( 𝜑 → ( 𝑌𝐷 ↔ ( 𝑌 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( ( 𝑌𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) ) )
36 6 35 mpbid ( 𝜑 → ( 𝑌 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( ( 𝑌𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) )
37 36 simpld ( 𝜑𝑌 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
38 26 28 31 mhmlin ( ( 𝑌 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑌 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( 𝑌𝑥 ) · ( 𝑌𝑦 ) ) )
39 38 3expb ( ( 𝑌 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑌 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( 𝑌𝑥 ) · ( 𝑌𝑦 ) ) )
40 37 39 sylan ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑌 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( 𝑌𝑥 ) · ( 𝑌𝑦 ) ) )
41 34 40 oveq12d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) · ( 𝑌 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) ) = ( ( ( 𝑋𝑥 ) · ( 𝑋𝑦 ) ) · ( ( 𝑌𝑥 ) · ( 𝑌𝑦 ) ) ) )
42 11 ffvelrnda ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋𝑥 ) ∈ ℂ )
43 42 adantrr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑋𝑥 ) ∈ ℂ )
44 simpr ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) → 𝑦 ∈ ( Base ‘ 𝑍 ) )
45 ffvelrn ( ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋𝑦 ) ∈ ℂ )
46 11 44 45 syl2an ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑋𝑦 ) ∈ ℂ )
47 12 ffvelrnda ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑌𝑥 ) ∈ ℂ )
48 47 adantrr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑌𝑥 ) ∈ ℂ )
49 ffvelrn ( ( 𝑌 : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑌𝑦 ) ∈ ℂ )
50 12 44 49 syl2an ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑌𝑦 ) ∈ ℂ )
51 43 46 48 50 mul4d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( ( ( 𝑋𝑥 ) · ( 𝑋𝑦 ) ) · ( ( 𝑌𝑥 ) · ( 𝑌𝑦 ) ) ) = ( ( ( 𝑋𝑥 ) · ( 𝑌𝑥 ) ) · ( ( 𝑋𝑦 ) · ( 𝑌𝑦 ) ) ) )
52 41 51 eqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) · ( 𝑌 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) ) = ( ( ( 𝑋𝑥 ) · ( 𝑌𝑥 ) ) · ( ( 𝑋𝑦 ) · ( 𝑌𝑦 ) ) ) )
53 11 ffnd ( 𝜑𝑋 Fn ( Base ‘ 𝑍 ) )
54 53 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → 𝑋 Fn ( Base ‘ 𝑍 ) )
55 12 ffnd ( 𝜑𝑌 Fn ( Base ‘ 𝑍 ) )
56 55 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → 𝑌 Fn ( Base ‘ 𝑍 ) )
57 fvexd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( Base ‘ 𝑍 ) ∈ V )
58 21 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
59 2 zncrng ( 𝑁 ∈ ℕ0𝑍 ∈ CRing )
60 crngring ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
61 58 59 60 3syl ( 𝜑𝑍 ∈ Ring )
62 10 27 ringcl ( ( 𝑍 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ ( Base ‘ 𝑍 ) )
63 62 3expb ( ( 𝑍 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ ( Base ‘ 𝑍 ) )
64 61 63 sylan ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ ( Base ‘ 𝑍 ) )
65 fnfvof ( ( ( 𝑋 Fn ( Base ‘ 𝑍 ) ∧ 𝑌 Fn ( Base ‘ 𝑍 ) ) ∧ ( ( Base ‘ 𝑍 ) ∈ V ∧ ( 𝑥 ( .r𝑍 ) 𝑦 ) ∈ ( Base ‘ 𝑍 ) ) ) → ( ( 𝑋f · 𝑌 ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) · ( 𝑌 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) ) )
66 54 56 57 64 65 syl22anc ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( ( 𝑋f · 𝑌 ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) · ( 𝑌 ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) ) )
67 53 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → 𝑋 Fn ( Base ‘ 𝑍 ) )
68 55 adantr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → 𝑌 Fn ( Base ‘ 𝑍 ) )
69 fvexd ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( Base ‘ 𝑍 ) ∈ V )
70 simpr ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → 𝑥 ∈ ( Base ‘ 𝑍 ) )
71 fnfvof ( ( ( 𝑋 Fn ( Base ‘ 𝑍 ) ∧ 𝑌 Fn ( Base ‘ 𝑍 ) ) ∧ ( ( Base ‘ 𝑍 ) ∈ V ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) ) → ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) = ( ( 𝑋𝑥 ) · ( 𝑌𝑥 ) ) )
72 67 68 69 70 71 syl22anc ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) = ( ( 𝑋𝑥 ) · ( 𝑌𝑥 ) ) )
73 72 adantrr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) = ( ( 𝑋𝑥 ) · ( 𝑌𝑥 ) ) )
74 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑍 ) )
75 fnfvof ( ( ( 𝑋 Fn ( Base ‘ 𝑍 ) ∧ 𝑌 Fn ( Base ‘ 𝑍 ) ) ∧ ( ( Base ‘ 𝑍 ) ∈ V ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( ( 𝑋f · 𝑌 ) ‘ 𝑦 ) = ( ( 𝑋𝑦 ) · ( 𝑌𝑦 ) ) )
76 54 56 57 74 75 syl22anc ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( ( 𝑋f · 𝑌 ) ‘ 𝑦 ) = ( ( 𝑋𝑦 ) · ( 𝑌𝑦 ) ) )
77 73 76 oveq12d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) · ( ( 𝑋f · 𝑌 ) ‘ 𝑦 ) ) = ( ( ( 𝑋𝑥 ) · ( 𝑌𝑥 ) ) · ( ( 𝑋𝑦 ) · ( 𝑌𝑦 ) ) ) )
78 52 66 77 3eqtr4d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( ( 𝑋f · 𝑌 ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) · ( ( 𝑋f · 𝑌 ) ‘ 𝑦 ) ) )
79 19 78 sylan2 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Unit ‘ 𝑍 ) ∧ 𝑦 ∈ ( Unit ‘ 𝑍 ) ) ) → ( ( 𝑋f · 𝑌 ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) · ( ( 𝑋f · 𝑌 ) ‘ 𝑦 ) ) )
80 79 ralrimivva ( 𝜑 → ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( ( 𝑋f · 𝑌 ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) · ( ( 𝑋f · 𝑌 ) ‘ 𝑦 ) ) )
81 eqid ( 1r𝑍 ) = ( 1r𝑍 )
82 10 81 ringidcl ( 𝑍 ∈ Ring → ( 1r𝑍 ) ∈ ( Base ‘ 𝑍 ) )
83 61 82 syl ( 𝜑 → ( 1r𝑍 ) ∈ ( Base ‘ 𝑍 ) )
84 fnfvof ( ( ( 𝑋 Fn ( Base ‘ 𝑍 ) ∧ 𝑌 Fn ( Base ‘ 𝑍 ) ) ∧ ( ( Base ‘ 𝑍 ) ∈ V ∧ ( 1r𝑍 ) ∈ ( Base ‘ 𝑍 ) ) ) → ( ( 𝑋f · 𝑌 ) ‘ ( 1r𝑍 ) ) = ( ( 𝑋 ‘ ( 1r𝑍 ) ) · ( 𝑌 ‘ ( 1r𝑍 ) ) ) )
85 53 55 13 83 84 syl22anc ( 𝜑 → ( ( 𝑋f · 𝑌 ) ‘ ( 1r𝑍 ) ) = ( ( 𝑋 ‘ ( 1r𝑍 ) ) · ( 𝑌 ‘ ( 1r𝑍 ) ) ) )
86 25 81 ringidval ( 1r𝑍 ) = ( 0g ‘ ( mulGrp ‘ 𝑍 ) )
87 cnfld1 1 = ( 1r ‘ ℂfld )
88 29 87 ringidval 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
89 86 88 mhm0 ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑋 ‘ ( 1r𝑍 ) ) = 1 )
90 24 89 syl ( 𝜑 → ( 𝑋 ‘ ( 1r𝑍 ) ) = 1 )
91 86 88 mhm0 ( 𝑌 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑌 ‘ ( 1r𝑍 ) ) = 1 )
92 37 91 syl ( 𝜑 → ( 𝑌 ‘ ( 1r𝑍 ) ) = 1 )
93 90 92 oveq12d ( 𝜑 → ( ( 𝑋 ‘ ( 1r𝑍 ) ) · ( 𝑌 ‘ ( 1r𝑍 ) ) ) = ( 1 · 1 ) )
94 1t1e1 ( 1 · 1 ) = 1
95 93 94 eqtrdi ( 𝜑 → ( ( 𝑋 ‘ ( 1r𝑍 ) ) · ( 𝑌 ‘ ( 1r𝑍 ) ) ) = 1 )
96 85 95 eqtrd ( 𝜑 → ( ( 𝑋f · 𝑌 ) ‘ ( 1r𝑍 ) ) = 1 )
97 72 neeq1d ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) ≠ 0 ↔ ( ( 𝑋𝑥 ) · ( 𝑌𝑥 ) ) ≠ 0 ) )
98 42 47 mulne0bd ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ( 𝑋𝑥 ) ≠ 0 ∧ ( 𝑌𝑥 ) ≠ 0 ) ↔ ( ( 𝑋𝑥 ) · ( 𝑌𝑥 ) ) ≠ 0 ) )
99 97 98 bitr4d ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) ≠ 0 ↔ ( ( 𝑋𝑥 ) ≠ 0 ∧ ( 𝑌𝑥 ) ≠ 0 ) ) )
100 23 simprd ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( ( 𝑋𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
101 100 r19.21bi ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( 𝑋𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
102 101 adantrd ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ( 𝑋𝑥 ) ≠ 0 ∧ ( 𝑌𝑥 ) ≠ 0 ) → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
103 99 102 sylbid ( ( 𝜑𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
104 103 ralrimiva ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
105 80 96 104 3jca ( 𝜑 → ( ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( ( 𝑋f · 𝑌 ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) · ( ( 𝑋f · 𝑌 ) ‘ 𝑦 ) ) ∧ ( ( 𝑋f · 𝑌 ) ‘ ( 1r𝑍 ) ) = 1 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) )
106 1 2 10 16 21 3 dchrelbas3 ( 𝜑 → ( ( 𝑋f · 𝑌 ) ∈ 𝐷 ↔ ( ( 𝑋f · 𝑌 ) : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ ( ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( ( 𝑋f · 𝑌 ) ‘ ( 𝑥 ( .r𝑍 ) 𝑦 ) ) = ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) · ( ( 𝑋f · 𝑌 ) ‘ 𝑦 ) ) ∧ ( ( 𝑋f · 𝑌 ) ‘ ( 1r𝑍 ) ) = 1 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑍 ) ( ( ( 𝑋f · 𝑌 ) ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) ) ) )
107 15 105 106 mpbir2and ( 𝜑 → ( 𝑋f · 𝑌 ) ∈ 𝐷 )
108 7 107 eqeltrd ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐷 )