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 24973 |
. 2
⊢ (𝜑 → (𝑋 · 𝑌) = (𝑋 ∘𝑓 · 𝑌)) |
8 | | mulcl 10020 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
9 | 8 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ) |
10 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝑍) =
(Base‘𝑍) |
11 | 1, 2, 3, 10, 5 | dchrf 24967 |
. . . 4
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ) |
12 | 1, 2, 3, 10, 6 | dchrf 24967 |
. . . 4
⊢ (𝜑 → 𝑌:(Base‘𝑍)⟶ℂ) |
13 | | fvexd 6203 |
. . . 4
⊢ (𝜑 → (Base‘𝑍) ∈ V) |
14 | | inidm 3822 |
. . . 4
⊢
((Base‘𝑍)
∩ (Base‘𝑍)) =
(Base‘𝑍) |
15 | 9, 11, 12, 13, 13, 14 | off 6912 |
. . 3
⊢ (𝜑 → (𝑋 ∘𝑓 · 𝑌):(Base‘𝑍)⟶ℂ) |
16 | | eqid 2622 |
. . . . . . . 8
⊢
(Unit‘𝑍) =
(Unit‘𝑍) |
17 | 10, 16 | unitcl 18659 |
. . . . . . 7
⊢ (𝑥 ∈ (Unit‘𝑍) → 𝑥 ∈ (Base‘𝑍)) |
18 | 10, 16 | unitcl 18659 |
. . . . . . 7
⊢ (𝑦 ∈ (Unit‘𝑍) → 𝑦 ∈ (Base‘𝑍)) |
19 | 17, 18 | anim12i 590 |
. . . . . 6
⊢ ((𝑥 ∈ (Unit‘𝑍) ∧ 𝑦 ∈ (Unit‘𝑍)) → (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) |
20 | 1, 3 | dchrrcl 24965 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ) |
21 | 5, 20 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℕ) |
22 | 1, 2, 10, 16, 21, 3 | dchrelbas2 24962 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))))) |
23 | 5, 22 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))) |
24 | 23 | simpld 475 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
25 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
26 | 25, 10 | mgpbas 18495 |
. . . . . . . . . . . 12
⊢
(Base‘𝑍) =
(Base‘(mulGrp‘𝑍)) |
27 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑍) = (.r‘𝑍) |
28 | 25, 27 | mgpplusg 18493 |
. . . . . . . . . . . 12
⊢
(.r‘𝑍) = (+g‘(mulGrp‘𝑍)) |
29 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
30 | | cnfldmul 19752 |
. . . . . . . . . . . . 13
⊢ ·
= (.r‘ℂfld) |
31 | 29, 30 | mgpplusg 18493 |
. . . . . . . . . . . 12
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
32 | 26, 28, 31 | mhmlin 17342 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ 𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
33 | 32 | 3expb 1266 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
34 | 24, 33 | sylan 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
35 | 1, 2, 10, 16, 21, 3 | dchrelbas2 24962 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ∈ 𝐷 ↔ (𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑌‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))))) |
36 | 6, 35 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ (Base‘𝑍)((𝑌‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))) |
37 | 36 | simpld 475 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
38 | 26, 28, 31 | mhmlin 17342 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ 𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑌‘(𝑥(.r‘𝑍)𝑦)) = ((𝑌‘𝑥) · (𝑌‘𝑦))) |
39 | 38 | 3expb 1266 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌‘(𝑥(.r‘𝑍)𝑦)) = ((𝑌‘𝑥) · (𝑌‘𝑦))) |
40 | 37, 39 | sylan 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌‘(𝑥(.r‘𝑍)𝑦)) = ((𝑌‘𝑥) · (𝑌‘𝑦))) |
41 | 34, 40 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) · (𝑌‘(𝑥(.r‘𝑍)𝑦))) = (((𝑋‘𝑥) · (𝑋‘𝑦)) · ((𝑌‘𝑥) · (𝑌‘𝑦)))) |
42 | 11 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (𝑋‘𝑥) ∈ ℂ) |
43 | 42 | adantrr 753 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋‘𝑥) ∈ ℂ) |
44 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → 𝑦 ∈ (Base‘𝑍)) |
45 | | ffvelrn 6357 |
. . . . . . . . . 10
⊢ ((𝑋:(Base‘𝑍)⟶ℂ ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑋‘𝑦) ∈ ℂ) |
46 | 11, 44, 45 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑋‘𝑦) ∈ ℂ) |
47 | 12 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (𝑌‘𝑥) ∈ ℂ) |
48 | 47 | adantrr 753 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌‘𝑥) ∈ ℂ) |
49 | | ffvelrn 6357 |
. . . . . . . . . 10
⊢ ((𝑌:(Base‘𝑍)⟶ℂ ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑌‘𝑦) ∈ ℂ) |
50 | 12, 44, 49 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑌‘𝑦) ∈ ℂ) |
51 | 43, 46, 48, 50 | mul4d 10248 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (((𝑋‘𝑥) · (𝑋‘𝑦)) · ((𝑌‘𝑥) · (𝑌‘𝑦))) = (((𝑋‘𝑥) · (𝑌‘𝑥)) · ((𝑋‘𝑦) · (𝑌‘𝑦)))) |
52 | 41, 51 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) · (𝑌‘(𝑥(.r‘𝑍)𝑦))) = (((𝑋‘𝑥) · (𝑌‘𝑥)) · ((𝑋‘𝑦) · (𝑌‘𝑦)))) |
53 | | ffn 6045 |
. . . . . . . . . 10
⊢ (𝑋:(Base‘𝑍)⟶ℂ → 𝑋 Fn (Base‘𝑍)) |
54 | 11, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 Fn (Base‘𝑍)) |
55 | 54 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → 𝑋 Fn (Base‘𝑍)) |
56 | | ffn 6045 |
. . . . . . . . . 10
⊢ (𝑌:(Base‘𝑍)⟶ℂ → 𝑌 Fn (Base‘𝑍)) |
57 | 12, 56 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 Fn (Base‘𝑍)) |
58 | 57 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → 𝑌 Fn (Base‘𝑍)) |
59 | | fvexd 6203 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (Base‘𝑍) ∈ V) |
60 | 21 | nnnn0d 11351 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
61 | 2 | zncrng 19893 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
62 | | crngring 18558 |
. . . . . . . . . 10
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
63 | 60, 61, 62 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ Ring) |
64 | 10, 27 | ringcl 18561 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍)) → (𝑥(.r‘𝑍)𝑦) ∈ (Base‘𝑍)) |
65 | 64 | 3expb 1266 |
. . . . . . . . 9
⊢ ((𝑍 ∈ Ring ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑥(.r‘𝑍)𝑦) ∈ (Base‘𝑍)) |
66 | 63, 65 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (𝑥(.r‘𝑍)𝑦) ∈ (Base‘𝑍)) |
67 | | fnfvof 6911 |
. . . . . . . 8
⊢ (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ (𝑥(.r‘𝑍)𝑦) ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘(𝑥(.r‘𝑍)𝑦)) · (𝑌‘(𝑥(.r‘𝑍)𝑦)))) |
68 | 55, 58, 59, 66, 67 | syl22anc 1327 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘(𝑥(.r‘𝑍)𝑦)) · (𝑌‘(𝑥(.r‘𝑍)𝑦)))) |
69 | 54 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → 𝑋 Fn (Base‘𝑍)) |
70 | 57 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → 𝑌 Fn (Base‘𝑍)) |
71 | | fvexd 6203 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (Base‘𝑍) ∈ V) |
72 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → 𝑥 ∈ (Base‘𝑍)) |
73 | | fnfvof 6911 |
. . . . . . . . . 10
⊢ (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ 𝑥 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘𝑥) = ((𝑋‘𝑥) · (𝑌‘𝑥))) |
74 | 69, 70, 71, 72, 73 | syl22anc 1327 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → ((𝑋 ∘𝑓 · 𝑌)‘𝑥) = ((𝑋‘𝑥) · (𝑌‘𝑥))) |
75 | 74 | adantrr 753 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘𝑥) = ((𝑋‘𝑥) · (𝑌‘𝑥))) |
76 | | simprr 796 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → 𝑦 ∈ (Base‘𝑍)) |
77 | | fnfvof 6911 |
. . . . . . . . 9
⊢ (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘𝑦) = ((𝑋‘𝑦) · (𝑌‘𝑦))) |
78 | 55, 58, 59, 76, 77 | syl22anc 1327 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘𝑦) = ((𝑋‘𝑦) · (𝑌‘𝑦))) |
79 | 75, 78 | oveq12d 6668 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦)) = (((𝑋‘𝑥) · (𝑌‘𝑥)) · ((𝑋‘𝑦) · (𝑌‘𝑦)))) |
80 | 52, 68, 79 | 3eqtr4d 2666 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝑍) ∧ 𝑦 ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦))) |
81 | 19, 80 | sylan2 491 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Unit‘𝑍) ∧ 𝑦 ∈ (Unit‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦))) |
82 | 81 | ralrimivva 2971 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦))) |
83 | | eqid 2622 |
. . . . . . . 8
⊢
(1r‘𝑍) = (1r‘𝑍) |
84 | 10, 83 | ringidcl 18568 |
. . . . . . 7
⊢ (𝑍 ∈ Ring →
(1r‘𝑍)
∈ (Base‘𝑍)) |
85 | 63, 84 | syl 17 |
. . . . . 6
⊢ (𝜑 → (1r‘𝑍) ∈ (Base‘𝑍)) |
86 | | fnfvof 6911 |
. . . . . 6
⊢ (((𝑋 Fn (Base‘𝑍) ∧ 𝑌 Fn (Base‘𝑍)) ∧ ((Base‘𝑍) ∈ V ∧ (1r‘𝑍) ∈ (Base‘𝑍))) → ((𝑋 ∘𝑓 · 𝑌)‘(1r‘𝑍)) = ((𝑋‘(1r‘𝑍)) · (𝑌‘(1r‘𝑍)))) |
87 | 54, 57, 13, 85, 86 | syl22anc 1327 |
. . . . 5
⊢ (𝜑 → ((𝑋 ∘𝑓 · 𝑌)‘(1r‘𝑍)) = ((𝑋‘(1r‘𝑍)) · (𝑌‘(1r‘𝑍)))) |
88 | 25, 83 | ringidval 18503 |
. . . . . . . . 9
⊢
(1r‘𝑍) = (0g‘(mulGrp‘𝑍)) |
89 | | cnfld1 19771 |
. . . . . . . . . 10
⊢ 1 =
(1r‘ℂfld) |
90 | 29, 89 | ringidval 18503 |
. . . . . . . . 9
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
91 | 88, 90 | mhm0 17343 |
. . . . . . . 8
⊢ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) → (𝑋‘(1r‘𝑍)) = 1) |
92 | 24, 91 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑋‘(1r‘𝑍)) = 1) |
93 | 88, 90 | mhm0 17343 |
. . . . . . . 8
⊢ (𝑌 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) → (𝑌‘(1r‘𝑍)) = 1) |
94 | 37, 93 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑌‘(1r‘𝑍)) = 1) |
95 | 92, 94 | oveq12d 6668 |
. . . . . 6
⊢ (𝜑 → ((𝑋‘(1r‘𝑍)) · (𝑌‘(1r‘𝑍))) = (1 ·
1)) |
96 | | 1t1e1 11175 |
. . . . . 6
⊢ (1
· 1) = 1 |
97 | 95, 96 | syl6eq 2672 |
. . . . 5
⊢ (𝜑 → ((𝑋‘(1r‘𝑍)) · (𝑌‘(1r‘𝑍))) = 1) |
98 | 87, 97 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → ((𝑋 ∘𝑓 · 𝑌)‘(1r‘𝑍)) = 1) |
99 | 74 | neeq1d 2853 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 ↔ ((𝑋‘𝑥) · (𝑌‘𝑥)) ≠ 0)) |
100 | 42, 47 | mulne0bd 10678 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (((𝑋‘𝑥) ≠ 0 ∧ (𝑌‘𝑥) ≠ 0) ↔ ((𝑋‘𝑥) · (𝑌‘𝑥)) ≠ 0)) |
101 | 99, 100 | bitr4d 271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 ↔ ((𝑋‘𝑥) ≠ 0 ∧ (𝑌‘𝑥) ≠ 0))) |
102 | 23 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑍)((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
103 | 102 | r19.21bi 2932 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
104 | 103 | adantrd 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (((𝑋‘𝑥) ≠ 0 ∧ (𝑌‘𝑥) ≠ 0) → 𝑥 ∈ (Unit‘𝑍))) |
105 | 101, 104 | sylbid 230 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑍)) → (((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
106 | 105 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑍)(((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
107 | 82, 98, 106 | 3jca 1242 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦)) ∧ ((𝑋 ∘𝑓 · 𝑌)‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ (Base‘𝑍)(((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))) |
108 | 1, 2, 10, 16, 21, 3 | dchrelbas3 24963 |
. . 3
⊢ (𝜑 → ((𝑋 ∘𝑓 · 𝑌) ∈ 𝐷 ↔ ((𝑋 ∘𝑓 · 𝑌):(Base‘𝑍)⟶ℂ ∧ (∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)((𝑋 ∘𝑓 · 𝑌)‘(𝑥(.r‘𝑍)𝑦)) = (((𝑋 ∘𝑓 · 𝑌)‘𝑥) · ((𝑋 ∘𝑓 · 𝑌)‘𝑦)) ∧ ((𝑋 ∘𝑓 · 𝑌)‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ (Base‘𝑍)(((𝑋 ∘𝑓 · 𝑌)‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))))) |
109 | 15, 107, 108 | mpbir2and 957 |
. 2
⊢ (𝜑 → (𝑋 ∘𝑓 · 𝑌) ∈ 𝐷) |
110 | 7, 109 | eqeltrd 2701 |
1
⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐷) |