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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
43 42 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
44 simpr ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) → 𝑦 ∈ ( Base ‘ 𝑍 ) )
45 ffvelcdm ⊢ ( ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ 𝑦 ) ∈ ℂ )
46 11 44 45 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑋 ‘ 𝑦 ) ∈ ℂ )
47 12 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑌 ‘ 𝑥 ) ∈ ℂ )
48 47 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ∧ 𝑦 ∈ ( Base ‘ 𝑍 ) ) ) → ( 𝑌 ‘ 𝑥 ) ∈ ℂ )
49 ffvelcdm ⊢ ( ( 𝑌 : ( 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 ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐷 )