Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrmulcl Structured version   Visualization version   GIF version

Theorem dchrmulcl 25144
 Description: Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
Hypotheses
Ref Expression
dchrmhm.g 𝐺 = (DChr‘𝑁)
dchrmhm.z 𝑍 = (ℤ/nℤ‘𝑁)
dchrmhm.b 𝐷 = (Base‘𝐺)
dchrmul.t · = (+g𝐺)
dchrmul.x (𝜑𝑋𝐷)
dchrmul.y (𝜑𝑌𝐷)
Assertion
Ref Expression
dchrmulcl (𝜑 → (𝑋 · 𝑌) ∈ 𝐷)

Proof of Theorem dchrmulcl
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dchrmhm.g . . 3 𝐺 = (DChr‘𝑁)
2 dchrmhm.z . . 3 𝑍 = (ℤ/nℤ‘𝑁)
3 dchrmhm.b . . 3 𝐷 = (Base‘𝐺)
4 dchrmul.t . . 3 · = (+g𝐺)
5 dchrmul.x . . 3 (𝜑𝑋𝐷)
6 dchrmul.y . . 3 (𝜑𝑌𝐷)
71, 2, 3, 4, 5, 6dchrmul 25143 . 2 (𝜑 → (𝑋 · 𝑌) = (𝑋𝑓 · 𝑌))
8 mulcl 10183 . . . . 5 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
98adantl 473 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
10 eqid 2748 . . . . 5 (Base‘𝑍) = (Base‘𝑍)
111, 2, 3, 10, 5dchrf 25137 . . . 4 (𝜑𝑋:(Base‘𝑍)⟶ℂ)
121, 2, 3, 10, 6dchrf 25137 . . . 4 (𝜑𝑌:(Base‘𝑍)⟶ℂ)
13 fvexd 6352 . . . 4 (𝜑 → (Base‘𝑍) ∈ V)
14 inidm 3953 . . . 4 ((Base‘𝑍) ∩ (Base‘𝑍)) = (Base‘𝑍)
159, 11, 12, 13, 13, 14off 7065 . . 3 (𝜑 → (𝑋𝑓 · 𝑌):(Base‘𝑍)⟶ℂ)
16 eqid 2748 . . . . . . . 8 (Unit‘𝑍) = (Unit‘𝑍)
1710, 16unitcl 18830 . . . . . . 7 (𝑥 ∈ (Unit‘𝑍) → 𝑥 ∈ (Base‘𝑍))
1810, 16unitcl 18830 . . . . . . 7 (𝑦 ∈ (Unit‘𝑍) → 𝑦 ∈ (Base‘𝑍))
1917, 18anim12i 591 . . . . . 6 ((𝑥 ∈ (Unit‘𝑍) ∧ 𝑦 ∈ (Unit‘𝑍)) → (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)))
201, 3dchrrcl 25135 . . . . . . . . . . . . . 14 (𝑋𝐷𝑁 ∈ ℕ)
215, 20syl 17 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℕ)
221, 2, 10, 16, 21, 3dchrelbas2 25132 . . . . . . . . . . . 12 (𝜑 → (𝑋𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑋𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))))
235, 22mpbid 222 . . . . . . . . . . 11 (𝜑 → (𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑋𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))))
2423simpld 477 . . . . . . . . . 10 (𝜑𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)))
25 eqid 2748 . . . . . . . . . . . . 13 (mulGrp‘𝑍) = (mulGrp‘𝑍)
2625, 10mgpbas 18666 . . . . . . . . . . . 12 (Base‘𝑍) = (Base‘(mulGrp‘𝑍))
27 eqid 2748 . . . . . . . . . . . . 13 (.r𝑍) = (.r𝑍)
2825, 27mgpplusg 18664 . . . . . . . . . . . 12 (.r𝑍) = (+g‘(mulGrp‘𝑍))
29 eqid 2748 . . . . . . . . . . . . 13 (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
30 cnfldmul 19925 . . . . . . . . . . . . 13 · = (.r‘ℂfld)
3129, 30mgpplusg 18664 . . . . . . . . . . . 12 · = (+g‘(mulGrp‘ℂfld))
3226, 28, 31mhmlin 17514 . . . . . . . . . . 11 ((𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ 𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑋‘(𝑥(.r𝑍)𝑦)) = ((𝑋𝑥) · (𝑋𝑦)))
33323expb 1113 . . . . . . . . . 10 ((𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋‘(𝑥(.r𝑍)𝑦)) = ((𝑋𝑥) · (𝑋𝑦)))
3424, 33sylan 489 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋‘(𝑥(.r𝑍)𝑦)) = ((𝑋𝑥) · (𝑋𝑦)))
351, 2, 10, 16, 21, 3dchrelbas2 25132 . . . . . . . . . . . 12 (𝜑 → (𝑌𝐷 ↔ (𝑌 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑌𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))))
366, 35mpbid 222 . . . . . . . . . . 11 (𝜑 → (𝑌 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑌𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))))
3736simpld 477 . . . . . . . . . 10 (𝜑𝑌 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)))
3826, 28, 31mhmlin 17514 . . . . . . . . . . 11 ((𝑌 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ 𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑌‘(𝑥(.r𝑍)𝑦)) = ((𝑌𝑥) · (𝑌𝑦)))
39383expb 1113 . . . . . . . . . 10 ((𝑌 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌‘(𝑥(.r𝑍)𝑦)) = ((𝑌𝑥) · (𝑌𝑦)))
4037, 39sylan 489 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌‘(𝑥(.r𝑍)𝑦)) = ((𝑌𝑥) · (𝑌𝑦)))
4134, 40oveq12d 6819 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋‘(𝑥(.r𝑍)𝑦)) · (𝑌‘(𝑥(.r𝑍)𝑦))) = (((𝑋𝑥) · (𝑋𝑦)) · ((𝑌𝑥) · (𝑌𝑦))))
4211ffvelrnda 6510 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝑍)) → (𝑋𝑥) ∈ ℂ)
4342adantrr 755 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋𝑥) ∈ ℂ)
44 simpr 479 . . . . . . . . . 10 ((𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → 𝑦 ∈ (Base‘𝑍))
45 ffvelrn 6508 . . . . . . . . . 10 ((𝑋:(Base‘𝑍)⟶ℂ ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑋𝑦) ∈ ℂ)
4611, 44, 45syl2an 495 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋𝑦) ∈ ℂ)
4712ffvelrnda 6510 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝑍)) → (𝑌𝑥) ∈ ℂ)
4847adantrr 755 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌𝑥) ∈ ℂ)
49 ffvelrn 6508 . . . . . . . . . 10 ((𝑌:(Base‘𝑍)⟶ℂ ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑌𝑦) ∈ ℂ)
5012, 44, 49syl2an 495 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌𝑦) ∈ ℂ)
5143, 46, 48, 50mul4d 10411 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (((𝑋𝑥) · (𝑋𝑦)) · ((𝑌𝑥) · (𝑌𝑦))) = (((𝑋𝑥) · (𝑌𝑥)) · ((𝑋𝑦) · (𝑌𝑦))))
5241, 51eqtrd 2782 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋‘(𝑥(.r𝑍)𝑦)) · (𝑌‘(𝑥(.r𝑍)𝑦))) = (((𝑋𝑥) · (𝑌𝑥)) · ((𝑋𝑦) · (𝑌𝑦))))
53 ffn 6194 . . . . . . . . . 10 (𝑋:(Base‘𝑍)⟶ℂ → 𝑋 Fn (Base‘𝑍))
5411, 53syl 17 . . . . . . . . 9 (𝜑𝑋 Fn (Base‘𝑍))
5554adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → 𝑋 Fn (Base‘𝑍))
56 ffn 6194 . . . . . . . . . 10 (𝑌:(Base‘𝑍)⟶ℂ → 𝑌 Fn (Base‘𝑍))
5712, 56syl 17 . . . . . . . . 9 (𝜑𝑌 Fn (Base‘𝑍))
5857adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → 𝑌 Fn (Base‘𝑍))
59 fvexd 6352 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (Base‘𝑍) ∈ V)
6021nnnn0d 11514 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
612zncrng 20066 . . . . . . . . . 10 (𝑁 ∈ ℕ0𝑍 ∈ CRing)
62 crngring 18729 . . . . . . . . . 10 (𝑍 ∈ CRing → 𝑍 ∈ Ring)
6360, 61, 623syl 18 . . . . . . . . 9 (𝜑𝑍 ∈ Ring)
6410, 27ringcl 18732 . . . . . . . . . 10 ((𝑍 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑥(.r𝑍)𝑦) ∈ (Base‘𝑍))
65643expb 1113 . . . . . . . . 9 ((𝑍 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑥(.r𝑍)𝑦) ∈ (Base‘𝑍))
6663, 65sylan 489 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑥(.r𝑍)𝑦) ∈ (Base‘𝑍))
67 fnfvof 7064 . . . . . . . 8 (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ (𝑥(.r𝑍)𝑦) ∈ (Base‘𝑍))) → ((𝑋𝑓 · 𝑌)‘(𝑥(.r𝑍)𝑦)) = ((𝑋‘(𝑥(.r𝑍)𝑦)) · (𝑌‘(𝑥(.r𝑍)𝑦))))
6855, 58, 59, 66, 67syl22anc 1464 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋𝑓 · 𝑌)‘(𝑥(.r𝑍)𝑦)) = ((𝑋‘(𝑥(.r𝑍)𝑦)) · (𝑌‘(𝑥(.r𝑍)𝑦))))
6954adantr 472 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝑍)) → 𝑋 Fn (Base‘𝑍))
7057adantr 472 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝑍)) → 𝑌 Fn (Base‘𝑍))
71 fvexd 6352 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝑍)) → (Base‘𝑍) ∈ V)
72 simpr 479 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝑍)) → 𝑥 ∈ (Base‘𝑍))
73 fnfvof 7064 . . . . . . . . . 10 (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ 𝑥 ∈ (Base‘𝑍))) → ((𝑋𝑓 · 𝑌)‘𝑥) = ((𝑋𝑥) · (𝑌𝑥)))
7469, 70, 71, 72, 73syl22anc 1464 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑍)) → ((𝑋𝑓 · 𝑌)‘𝑥) = ((𝑋𝑥) · (𝑌𝑥)))
7574adantrr 755 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋𝑓 · 𝑌)‘𝑥) = ((𝑋𝑥) · (𝑌𝑥)))
76 simprr 813 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → 𝑦 ∈ (Base‘𝑍))
77 fnfvof 7064 . . . . . . . . 9 (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋𝑓 · 𝑌)‘𝑦) = ((𝑋𝑦) · (𝑌𝑦)))
7855, 58, 59, 76, 77syl22anc 1464 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋𝑓 · 𝑌)‘𝑦) = ((𝑋𝑦) · (𝑌𝑦)))
7975, 78oveq12d 6819 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (((𝑋𝑓 · 𝑌)‘𝑥) · ((𝑋𝑓 · 𝑌)‘𝑦)) = (((𝑋𝑥) · (𝑌𝑥)) · ((𝑋𝑦) · (𝑌𝑦))))
8052, 68, 793eqtr4d 2792 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋𝑓 · 𝑌)‘(𝑥(.r𝑍)𝑦)) = (((𝑋𝑓 · 𝑌)‘𝑥) · ((𝑋𝑓 · 𝑌)‘𝑦)))
8119, 80sylan2 492 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Unit‘𝑍) ∧ 𝑦 ∈ (Unit‘𝑍))) → ((𝑋𝑓 · 𝑌)‘(𝑥(.r𝑍)𝑦)) = (((𝑋𝑓 · 𝑌)‘𝑥) · ((𝑋𝑓 · 𝑌)‘𝑦)))
8281ralrimivva 3097 . . . 4 (𝜑 → ∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)((𝑋𝑓 · 𝑌)‘(𝑥(.r𝑍)𝑦)) = (((𝑋𝑓 · 𝑌)‘𝑥) · ((𝑋𝑓 · 𝑌)‘𝑦)))
83 eqid 2748 . . . . . . . 8 (1r𝑍) = (1r𝑍)
8410, 83ringidcl 18739 . . . . . . 7 (𝑍 ∈ Ring → (1r𝑍) ∈ (Base‘𝑍))
8563, 84syl 17 . . . . . 6 (𝜑 → (1r𝑍) ∈ (Base‘𝑍))
86 fnfvof 7064 . . . . . 6 (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ (1r𝑍) ∈ (Base‘𝑍))) → ((𝑋𝑓 · 𝑌)‘(1r𝑍)) = ((𝑋‘(1r𝑍)) · (𝑌‘(1r𝑍))))
8754, 57, 13, 85, 86syl22anc 1464 . . . . 5 (𝜑 → ((𝑋𝑓 · 𝑌)‘(1r𝑍)) = ((𝑋‘(1r𝑍)) · (𝑌‘(1r𝑍))))
8825, 83ringidval 18674 . . . . . . . . 9 (1r𝑍) = (0g‘(mulGrp‘𝑍))
89 cnfld1 19944 . . . . . . . . . 10 1 = (1r‘ℂfld)
9029, 89ringidval 18674 . . . . . . . . 9 1 = (0g‘(mulGrp‘ℂfld))
9188, 90mhm0 17515 . . . . . . . 8 (𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) → (𝑋‘(1r𝑍)) = 1)
9224, 91syl 17 . . . . . . 7 (𝜑 → (𝑋‘(1r𝑍)) = 1)
9388, 90mhm0 17515 . . . . . . . 8 (𝑌 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) → (𝑌‘(1r𝑍)) = 1)
9437, 93syl 17 . . . . . . 7 (𝜑 → (𝑌‘(1r𝑍)) = 1)
9592, 94oveq12d 6819 . . . . . 6 (𝜑 → ((𝑋‘(1r𝑍)) · (𝑌‘(1r𝑍))) = (1 · 1))
96 1t1e1 11338 . . . . . 6 (1 · 1) = 1
9795, 96syl6eq 2798 . . . . 5 (𝜑 → ((𝑋‘(1r𝑍)) · (𝑌‘(1r𝑍))) = 1)
9887, 97eqtrd 2782 . . . 4 (𝜑 → ((𝑋𝑓 · 𝑌)‘(1r𝑍)) = 1)
9974neeq1d 2979 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑍)) → (((𝑋𝑓 · 𝑌)‘𝑥) ≠ 0 ↔ ((𝑋𝑥) · (𝑌𝑥)) ≠ 0))
10042, 47mulne0bd 10841 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑍)) → (((𝑋𝑥) ≠ 0 ∧ (𝑌𝑥) ≠ 0) ↔ ((𝑋𝑥) · (𝑌𝑥)) ≠ 0))
10199, 100bitr4d 271 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑍)) → (((𝑋𝑓 · 𝑌)‘𝑥) ≠ 0 ↔ ((𝑋𝑥) ≠ 0 ∧ (𝑌𝑥) ≠ 0)))
10223simprd 482 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ (Base‘𝑍)((𝑋𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))
103102r19.21bi 3058 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑍)) → ((𝑋𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))
104103adantrd 485 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑍)) → (((𝑋𝑥) ≠ 0 ∧ (𝑌𝑥) ≠ 0) → 𝑥 ∈ (Unit‘𝑍)))
105101, 104sylbid 230 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝑍)) → (((𝑋𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))
106105ralrimiva 3092 . . . 4 (𝜑 → ∀𝑥 ∈ (Base‘𝑍)(((𝑋𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))
10782, 98, 1063jca 1403 . . 3 (𝜑 → (∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)((𝑋𝑓 · 𝑌)‘(𝑥(.r𝑍)𝑦)) = (((𝑋𝑓 · 𝑌)‘𝑥) · ((𝑋𝑓 · 𝑌)‘𝑦)) ∧ ((𝑋𝑓 · 𝑌)‘(1r𝑍)) = 1 ∧ ∀𝑥 ∈ (Base‘𝑍)(((𝑋𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))))
1081, 2, 10, 16, 21, 3dchrelbas3 25133 . . 3 (𝜑 → ((𝑋𝑓 · 𝑌) ∈ 𝐷 ↔ ((𝑋𝑓 · 𝑌):(Base‘𝑍)⟶ℂ ∧ (∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)((𝑋𝑓 · 𝑌)‘(𝑥(.r𝑍)𝑦)) = (((𝑋𝑓 · 𝑌)‘𝑥) · ((𝑋𝑓 · 𝑌)‘𝑦)) ∧ ((𝑋𝑓 · 𝑌)‘(1r𝑍)) = 1 ∧ ∀𝑥 ∈ (Base‘𝑍)(((𝑋𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))))))
10915, 107, 108mpbir2and 995 . 2 (𝜑 → (𝑋𝑓 · 𝑌) ∈ 𝐷)
1107, 109eqeltrd 2827 1 (𝜑 → (𝑋 · 𝑌) ∈ 𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1620   ∈ wcel 2127   ≠ wne 2920  ∀wral 3038  Vcvv 3328   Fn wfn 6032  ⟶wf 6033  ‘cfv 6037  (class class class)co 6801   ∘𝑓 cof 7048  ℂcc 10097  0cc0 10099  1c1 10100   · cmul 10104  ℕcn 11183  ℕ0cn0 11455  Basecbs 16030  +gcplusg 16114  .rcmulr 16115   MndHom cmhm 17505  mulGrpcmgp 18660  1rcur 18672  Ringcrg 18718  CRingccrg 18719  Unitcui 18810  ℂfldccnfld 19919  ℤ/nℤczn 20024  DChrcdchr 25127 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-rep 4911  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-cnex 10155  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-mulcom 10163  ax-addass 10164  ax-mulass 10165  ax-distr 10166  ax-i2m1 10167  ax-1ne0 10168  ax-1rid 10169  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172  ax-pre-lttri 10173  ax-pre-lttrn 10174  ax-pre-ltadd 10175  ax-pre-mulgt0 10176  ax-addf 10178  ax-mulf 10179 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-reu 3045  df-rmo 3046  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-int 4616  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-of 7050  df-om 7219  df-1st 7321  df-2nd 7322  df-tpos 7509  df-wrecs 7564  df-recs 7625  df-rdg 7663  df-1o 7717  df-oadd 7721  df-er 7899  df-ec 7901  df-qs 7905  df-map 8013  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8501  df-inf 8502  df-pnf 10239  df-mnf 10240  df-xr 10241  df-ltxr 10242  df-le 10243  df-sub 10431  df-neg 10432  df-nn 11184  df-2 11242  df-3 11243  df-4 11244  df-5 11245  df-6 11246  df-7 11247  df-8 11248  df-9 11249  df-n0 11456  df-z 11541  df-dec 11657  df-uz 11851  df-fz 12491  df-struct 16032  df-ndx 16033  df-slot 16034  df-base 16036  df-sets 16037  df-ress 16038  df-plusg 16127  df-mulr 16128  df-starv 16129  df-sca 16130  df-vsca 16131  df-ip 16132  df-tset 16133  df-ple 16134  df-ds 16137  df-unif 16138  df-0g 16275  df-imas 16341  df-qus 16342  df-mgm 17414  df-sgrp 17456  df-mnd 17467  df-mhm 17507  df-grp 17597  df-minusg 17598  df-sbg 17599  df-subg 17763  df-nsg 17764  df-eqg 17765  df-cmn 18366  df-abl 18367  df-mgp 18661  df-ur 18673  df-ring 18720  df-cring 18721  df-oppr 18794  df-dvdsr 18812  df-unit 18813  df-subrg 18951  df-lmod 19038  df-lss 19106  df-lsp 19145  df-sra 19345  df-rgmod 19346  df-lidl 19347  df-rsp 19348  df-2idl 19405  df-cnfld 19920  df-zring 19992  df-zn 20028  df-dchr 25128 This theorem is referenced by:  dchrabl  25149  dchrinv  25156
 Copyright terms: Public domain W3C validator