Step | Hyp | Ref
| 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
⊢ (𝜑 → 𝑌 ∈ 𝐷) |
7 | 1, 2, 3, 4, 5, 6 | dchrmul 24773 |
. 2
⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 ∘𝑓 · 𝑌)) |
8 | | mulcl 9899 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
9 | 8 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
10 | | eqid 2610 |
. . . . 5
⊢
(Base‘𝑍) =
(Base‘𝑍) |
11 | 1, 2, 3, 10, 5 | dchrf 24767 |
. . . 4
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ) |
12 | 1, 2, 3, 10, 6 | dchrf 24767 |
. . . 4
⊢ (𝜑 → 𝑌:(Base‘𝑍)⟶ℂ) |
13 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑍)
∈ V |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝜑 → (Base‘𝑍) ∈ V) |
15 | | inidm 3784 |
. . . 4
⊢
((Base‘𝑍)
∩ (Base‘𝑍)) =
(Base‘𝑍) |
16 | 9, 11, 12, 14, 14, 15 | off 6810 |
. . 3
⊢ (𝜑 → (𝑋 ∘𝑓 · 𝑌):(Base‘𝑍)⟶ℂ) |
17 | | eqid 2610 |
. . . . . . . 8
⊢
(Unit‘𝑍) =
(Unit‘𝑍) |
18 | 10, 17 | unitcl 18482 |
. . . . . . 7
⊢ (𝑥 ∈ (Unit‘𝑍) → 𝑥 ∈ (Base‘𝑍)) |
19 | 10, 17 | unitcl 18482 |
. . . . . . 7
⊢ (𝑦 ∈ (Unit‘𝑍) → 𝑦 ∈ (Base‘𝑍)) |
20 | 18, 19 | anim12i 588 |
. . . . . 6
⊢ ((𝑥 ∈ (Unit‘𝑍) ∧ 𝑦 ∈ (Unit‘𝑍)) → (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) |
21 | 1, 3 | dchrrcl 24765 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ) |
22 | 5, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) |
23 | 1, 2, 10, 17, 22, 3 | dchrelbas2 24762 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))))) |
24 | 5, 23 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))) |
25 | 24 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
26 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
27 | 26, 10 | mgpbas 18318 |
. . . . . . . . . . . 12
⊢
(Base‘𝑍) =
(Base‘(mulGrp‘𝑍)) |
28 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑍) = (.r‘𝑍) |
29 | 26, 28 | mgpplusg 18316 |
. . . . . . . . . . . 12
⊢
(.r‘𝑍) = (+g‘(mulGrp‘𝑍)) |
30 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
31 | | cnfldmul 19573 |
. . . . . . . . . . . . 13
⊢ ·
= (.r‘ℂfld) |
32 | 30, 31 | mgpplusg 18316 |
. . . . . . . . . . . 12
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
33 | 27, 29, 32 | mhmlin 17165 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ 𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
34 | 33 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
35 | 25, 34 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
36 | 1, 2, 10, 17, 22, 3 | dchrelbas2 24762 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ∈ 𝐷 ↔ (𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑌‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))))) |
37 | 6, 36 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑌‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))) |
38 | 37 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
39 | 27, 29, 32 | mhmlin 17165 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ 𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑌‘(𝑥(.r‘𝑍)𝑦)) = ((𝑌‘𝑥) · (𝑌‘𝑦))) |
40 | 39 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌‘(𝑥(.r‘𝑍)𝑦)) = ((𝑌‘𝑥) · (𝑌‘𝑦))) |
41 | 38, 40 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌‘(𝑥(.r‘𝑍)𝑦)) = ((𝑌‘𝑥) · (𝑌‘𝑦))) |
42 | 35, 41 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) · (𝑌‘(𝑥(.r‘𝑍)𝑦))) = (((𝑋‘𝑥) · (𝑋‘𝑦)) · ((𝑌‘𝑥) · (𝑌‘𝑦)))) |
43 | 11 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (𝑋‘𝑥) ∈ ℂ) |
44 | 43 | adantrr 749 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋‘𝑥) ∈ ℂ) |
45 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → 𝑦 ∈ (Base‘𝑍)) |
46 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢ ((𝑋:(Base‘𝑍)⟶ℂ ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑋‘𝑦) ∈ ℂ) |
47 | 11, 45, 46 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋‘𝑦) ∈ ℂ) |
48 | 12 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (𝑌‘𝑥) ∈ ℂ) |
49 | 48 | adantrr 749 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌‘𝑥) ∈ ℂ) |
50 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢ ((𝑌:(Base‘𝑍)⟶ℂ ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑌‘𝑦) ∈ ℂ) |
51 | 12, 45, 50 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌‘𝑦) ∈ ℂ) |
52 | 44, 47, 49, 51 | mul4d 10127 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (((𝑋‘𝑥) · (𝑋‘𝑦)) · ((𝑌‘𝑥) · (𝑌‘𝑦))) = (((𝑋‘𝑥) · (𝑌‘𝑥)) · ((𝑋‘𝑦) · (𝑌‘𝑦)))) |
53 | 42, 52 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) · (𝑌‘(𝑥(.r‘𝑍)𝑦))) = (((𝑋‘𝑥) · (𝑌‘𝑥)) · ((𝑋‘𝑦) · (𝑌‘𝑦)))) |
54 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝑋:(Base‘𝑍)⟶ℂ → 𝑋 Fn (Base‘𝑍)) |
55 | 11, 54 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 Fn (Base‘𝑍)) |
56 | 55 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → 𝑋 Fn (Base‘𝑍)) |
57 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝑌:(Base‘𝑍)⟶ℂ → 𝑌 Fn (Base‘𝑍)) |
58 | 12, 57 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 Fn (Base‘𝑍)) |
59 | 58 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → 𝑌 Fn (Base‘𝑍)) |
60 | 13 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (Base‘𝑍) ∈ V) |
61 | 22 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
62 | 2 | zncrng 19712 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
63 | | crngring 18381 |
. . . . . . . . . 10
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
64 | 61, 62, 63 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ Ring) |
65 | 10, 28 | ringcl 18384 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑥(.r‘𝑍)𝑦) ∈ (Base‘𝑍)) |
66 | 65 | 3expb 1258 |
. . . . . . . . 9
⊢ ((𝑍 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑥(.r‘𝑍)𝑦) ∈ (Base‘𝑍)) |
67 | 64, 66 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑥(.r‘𝑍)𝑦) ∈ (Base‘𝑍)) |
68 | | fnfvof 6809 |
. . . . . . . 8
⊢ (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ (𝑥(.r‘𝑍)𝑦) ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘(𝑥(.r‘𝑍)𝑦)) · (𝑌‘(𝑥(.r‘𝑍)𝑦)))) |
69 | 56, 59, 60, 67, 68 | syl22anc 1319 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘(𝑥(.r‘𝑍)𝑦)) · (𝑌‘(𝑥(.r‘𝑍)𝑦)))) |
70 | 55 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → 𝑋 Fn (Base‘𝑍)) |
71 | 58 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → 𝑌 Fn (Base‘𝑍)) |
72 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (Base‘𝑍) ∈ V) |
73 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → 𝑥 ∈ (Base‘𝑍)) |
74 | | fnfvof 6809 |
. . . . . . . . . 10
⊢ (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ 𝑥 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘𝑥) = ((𝑋‘𝑥) · (𝑌‘𝑥))) |
75 | 70, 71, 72, 73, 74 | syl22anc 1319 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → ((𝑋 ∘𝑓 · 𝑌)‘𝑥) = ((𝑋‘𝑥) · (𝑌‘𝑥))) |
76 | 75 | adantrr 749 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘𝑥) = ((𝑋‘𝑥) · (𝑌‘𝑥))) |
77 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → 𝑦 ∈ (Base‘𝑍)) |
78 | | fnfvof 6809 |
. . . . . . . . 9
⊢ (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘𝑦) = ((𝑋‘𝑦) · (𝑌‘𝑦))) |
79 | 56, 59, 60, 77, 78 | syl22anc 1319 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘𝑦) = ((𝑋‘𝑦) · (𝑌‘𝑦))) |
80 | 76, 79 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦)) = (((𝑋‘𝑥) · (𝑌‘𝑥)) · ((𝑋‘𝑦) · (𝑌‘𝑦)))) |
81 | 53, 69, 80 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦))) |
82 | 20, 81 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Unit‘𝑍) ∧ 𝑦 ∈ (Unit‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦))) |
83 | 82 | ralrimivva 2954 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦))) |
84 | | eqid 2610 |
. . . . . . . 8
⊢
(1r‘𝑍) = (1r‘𝑍) |
85 | 10, 84 | ringidcl 18391 |
. . . . . . 7
⊢ (𝑍 ∈ Ring →
(1r‘𝑍)
∈ (Base‘𝑍)) |
86 | 64, 85 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1r‘𝑍) ∈ (Base‘𝑍)) |
87 | | fnfvof 6809 |
. . . . . 6
⊢ (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ (1r‘𝑍) ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘(1r‘𝑍)) = ((𝑋‘(1r‘𝑍)) · (𝑌‘(1r‘𝑍)))) |
88 | 55, 58, 14, 86, 87 | syl22anc 1319 |
. . . . 5
⊢ (𝜑 → ((𝑋 ∘𝑓 · 𝑌)‘(1r‘𝑍)) = ((𝑋‘(1r‘𝑍)) · (𝑌‘(1r‘𝑍)))) |
89 | 26, 84 | ringidval 18326 |
. . . . . . . . 9
⊢
(1r‘𝑍) = (0g‘(mulGrp‘𝑍)) |
90 | | cnfld1 19590 |
. . . . . . . . . 10
⊢ 1 =
(1r‘ℂfld) |
91 | 30, 90 | ringidval 18326 |
. . . . . . . . 9
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
92 | 89, 91 | mhm0 17166 |
. . . . . . . 8
⊢ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) → (𝑋‘(1r‘𝑍)) = 1) |
93 | 25, 92 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑋‘(1r‘𝑍)) = 1) |
94 | 89, 91 | mhm0 17166 |
. . . . . . . 8
⊢ (𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) → (𝑌‘(1r‘𝑍)) = 1) |
95 | 38, 94 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑌‘(1r‘𝑍)) = 1) |
96 | 93, 95 | oveq12d 6567 |
. . . . . 6
⊢ (𝜑 → ((𝑋‘(1r‘𝑍)) · (𝑌‘(1r‘𝑍))) = (1 ·
1)) |
97 | | 1t1e1 11052 |
. . . . . 6
⊢ (1
· 1) = 1 |
98 | 96, 97 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 → ((𝑋‘(1r‘𝑍)) · (𝑌‘(1r‘𝑍))) = 1) |
99 | 88, 98 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((𝑋 ∘𝑓 · 𝑌)‘(1r‘𝑍)) = 1) |
100 | 75 | neeq1d 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 ↔ ((𝑋‘𝑥) · (𝑌‘𝑥)) ≠ 0)) |
101 | 43, 48 | mulne0bd 10557 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (((𝑋‘𝑥) ≠ 0 ∧ (𝑌‘𝑥) ≠ 0) ↔ ((𝑋‘𝑥) · (𝑌‘𝑥)) ≠ 0)) |
102 | 100, 101 | bitr4d 270 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 ↔ ((𝑋‘𝑥) ≠ 0 ∧ (𝑌‘𝑥) ≠ 0))) |
103 | 24 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑍)((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
104 | 103 | r19.21bi 2916 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
105 | 104 | adantrd 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (((𝑋‘𝑥) ≠ 0 ∧ (𝑌‘𝑥) ≠ 0) → 𝑥 ∈ (Unit‘𝑍))) |
106 | 102, 105 | sylbid 229 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
107 | 106 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑍)(((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
108 | 83, 99, 107 | 3jca 1235 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦)) ∧ ((𝑋 ∘𝑓 · 𝑌)‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ (Base‘𝑍)(((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))) |
109 | 1, 2, 10, 17, 22, 3 | dchrelbas3 24763 |
. . 3
⊢ (𝜑 → ((𝑋 ∘𝑓 · 𝑌) ∈ 𝐷 ↔ ((𝑋 ∘𝑓 · 𝑌):(Base‘𝑍)⟶ℂ ∧ (∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦)) ∧ ((𝑋 ∘𝑓 · 𝑌)‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ (Base‘𝑍)(((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))))) |
110 | 16, 108, 109 | mpbir2and 959 |
. 2
⊢ (𝜑 → (𝑋 ∘𝑓 · 𝑌) ∈ 𝐷) |
111 | 7, 110 | eqeltrd 2688 |
1
⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐷) |