Step | Hyp | Ref
| Expression |
1 | | dchrval.g |
. . 3
⊢ 𝐺 = (DChr‘𝑁) |
2 | | dchrval.z |
. . 3
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
3 | | dchrval.b |
. . 3
⊢ 𝐵 = (Base‘𝑍) |
4 | | dchrval.u |
. . 3
⊢ 𝑈 = (Unit‘𝑍) |
5 | | dchrval.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | | dchrbas.b |
. . 3
⊢ 𝐷 = (Base‘𝐺) |
7 | 1, 2, 3, 4, 5, 6 | dchrelbas2 24962 |
. 2
⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)))) |
8 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑋‘𝑧) = (𝑋‘𝑥)) |
9 | 8 | neeq1d 2853 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → ((𝑋‘𝑧) ≠ 0 ↔ (𝑋‘𝑥) ≠ 0)) |
10 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝑈 ↔ 𝑥 ∈ 𝑈)) |
11 | 9, 10 | imbi12d 334 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈) ↔ ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
12 | 11 | cbvralv 3171 |
. . . . 5
⊢
(∀𝑧 ∈
𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈) ↔ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) |
13 | 5 | nnnn0d 11351 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
14 | 2 | zncrng 19893 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ CRing) |
16 | | crngring 18558 |
. . . . . . . . . 10
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ∈ Ring) |
18 | | eqid 2622 |
. . . . . . . . . 10
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
19 | 18 | ringmgp 18553 |
. . . . . . . . 9
⊢ (𝑍 ∈ Ring →
(mulGrp‘𝑍) ∈
Mnd) |
20 | 17, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (mulGrp‘𝑍) ∈ Mnd) |
21 | | cnring 19768 |
. . . . . . . . 9
⊢
ℂfld ∈ Ring |
22 | | eqid 2622 |
. . . . . . . . . 10
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
23 | 22 | ringmgp 18553 |
. . . . . . . . 9
⊢
(ℂfld ∈ Ring →
(mulGrp‘ℂfld) ∈ Mnd) |
24 | 21, 23 | ax-mp 5 |
. . . . . . . 8
⊢
(mulGrp‘ℂfld) ∈ Mnd |
25 | 18, 3 | mgpbas 18495 |
. . . . . . . . . 10
⊢ 𝐵 =
(Base‘(mulGrp‘𝑍)) |
26 | | cnfldbas 19750 |
. . . . . . . . . . 11
⊢ ℂ =
(Base‘ℂfld) |
27 | 22, 26 | mgpbas 18495 |
. . . . . . . . . 10
⊢ ℂ =
(Base‘(mulGrp‘ℂfld)) |
28 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(.r‘𝑍) = (.r‘𝑍) |
29 | 18, 28 | mgpplusg 18493 |
. . . . . . . . . 10
⊢
(.r‘𝑍) = (+g‘(mulGrp‘𝑍)) |
30 | | cnfldmul 19752 |
. . . . . . . . . . 11
⊢ ·
= (.r‘ℂfld) |
31 | 22, 30 | mgpplusg 18493 |
. . . . . . . . . 10
⊢ ·
= (+g‘(mulGrp‘ℂfld)) |
32 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(1r‘𝑍) = (1r‘𝑍) |
33 | 18, 32 | ringidval 18503 |
. . . . . . . . . 10
⊢
(1r‘𝑍) = (0g‘(mulGrp‘𝑍)) |
34 | | cnfld1 19771 |
. . . . . . . . . . 11
⊢ 1 =
(1r‘ℂfld) |
35 | 22, 34 | ringidval 18503 |
. . . . . . . . . 10
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
36 | 25, 27, 29, 31, 33, 35 | ismhm 17337 |
. . . . . . . . 9
⊢ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ↔ (((mulGrp‘𝑍) ∈ Mnd ∧
(mulGrp‘ℂfld) ∈ Mnd) ∧ (𝑋:𝐵⟶ℂ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1))) |
37 | 36 | baib 944 |
. . . . . . . 8
⊢
(((mulGrp‘𝑍)
∈ Mnd ∧ (mulGrp‘ℂfld) ∈ Mnd) → (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ↔ (𝑋:𝐵⟶ℂ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1))) |
38 | 20, 24, 37 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ↔ (𝑋:𝐵⟶ℂ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1))) |
39 | 38 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) → (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ↔ (𝑋:𝐵⟶ℂ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1))) |
40 | | biimt 350 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ↔ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))) |
41 | 40 | adantl 482 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ↔ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))) |
42 | 17 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑍 ∈ Ring) |
43 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
44 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
45 | 3, 28 | ringcl 18561 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑍 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝑍)𝑦) ∈ 𝐵) |
46 | 42, 43, 44, 45 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝑍)𝑦) ∈ 𝐵) |
47 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) |
48 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝑥(.r‘𝑍)𝑦) → (𝑋‘𝑧) = (𝑋‘(𝑥(.r‘𝑍)𝑦))) |
49 | 48 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (𝑥(.r‘𝑍)𝑦) → ((𝑋‘𝑧) ≠ 0 ↔ (𝑋‘(𝑥(.r‘𝑍)𝑦)) ≠ 0)) |
50 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = (𝑥(.r‘𝑍)𝑦) → (𝑧 ∈ 𝑈 ↔ (𝑥(.r‘𝑍)𝑦) ∈ 𝑈)) |
51 | 49, 50 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = (𝑥(.r‘𝑍)𝑦) → (((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈) ↔ ((𝑋‘(𝑥(.r‘𝑍)𝑦)) ≠ 0 → (𝑥(.r‘𝑍)𝑦) ∈ 𝑈))) |
52 | 51 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥(.r‘𝑍)𝑦) ∈ 𝐵 → (∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) ≠ 0 → (𝑥(.r‘𝑍)𝑦) ∈ 𝑈))) |
53 | 46, 47, 52 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) ≠ 0 → (𝑥(.r‘𝑍)𝑦) ∈ 𝑈)) |
54 | 15 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑍 ∈ CRing) |
55 | 4, 28, 3 | unitmulclb 18665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑍 ∈ CRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥(.r‘𝑍)𝑦) ∈ 𝑈 ↔ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))) |
56 | 54, 43, 44, 55 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥(.r‘𝑍)𝑦) ∈ 𝑈 ↔ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))) |
57 | 53, 56 | sylibd 229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) ≠ 0 → (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))) |
58 | 57 | necon1bd 2812 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (¬ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = 0)) |
59 | 58 | imp 445 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ¬ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = 0) |
60 | 11 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝐵 → (∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈) → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
61 | 43, 47, 60 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) |
62 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑦 → (𝑋‘𝑧) = (𝑋‘𝑦)) |
63 | 62 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑦 → ((𝑋‘𝑧) ≠ 0 ↔ (𝑋‘𝑦) ≠ 0)) |
64 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝑈 ↔ 𝑦 ∈ 𝑈)) |
65 | 63, 64 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑦 → (((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈) ↔ ((𝑋‘𝑦) ≠ 0 → 𝑦 ∈ 𝑈))) |
66 | 65 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ 𝐵 → (∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈) → ((𝑋‘𝑦) ≠ 0 → 𝑦 ∈ 𝑈))) |
67 | 44, 47, 66 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋‘𝑦) ≠ 0 → 𝑦 ∈ 𝑈)) |
68 | 61, 67 | anim12d 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑋‘𝑥) ≠ 0 ∧ (𝑋‘𝑦) ≠ 0) → (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))) |
69 | 68 | con3dimp 457 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ¬ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ¬ ((𝑋‘𝑥) ≠ 0 ∧ (𝑋‘𝑦) ≠ 0)) |
70 | | neanior 2886 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋‘𝑥) ≠ 0 ∧ (𝑋‘𝑦) ≠ 0) ↔ ¬ ((𝑋‘𝑥) = 0 ∨ (𝑋‘𝑦) = 0)) |
71 | 70 | con2bii 347 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋‘𝑥) = 0 ∨ (𝑋‘𝑦) = 0) ↔ ¬ ((𝑋‘𝑥) ≠ 0 ∧ (𝑋‘𝑦) ≠ 0)) |
72 | 69, 71 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ¬ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑋‘𝑥) = 0 ∨ (𝑋‘𝑦) = 0)) |
73 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑋:𝐵⟶ℂ) |
74 | 73, 43 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑋‘𝑥) ∈ ℂ) |
75 | 73, 44 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑋‘𝑦) ∈ ℂ) |
76 | 74, 75 | mul0ord 10677 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑋‘𝑥) · (𝑋‘𝑦)) = 0 ↔ ((𝑋‘𝑥) = 0 ∨ (𝑋‘𝑦) = 0))) |
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ¬ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (((𝑋‘𝑥) · (𝑋‘𝑦)) = 0 ↔ ((𝑋‘𝑥) = 0 ∨ (𝑋‘𝑦) = 0))) |
78 | 72, 77 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ¬ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑋‘𝑥) · (𝑋‘𝑦)) = 0) |
79 | 59, 78 | eqtr4d 2659 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ¬ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
80 | 79 | a1d 25 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ¬ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
81 | 79, 80 | 2thd 255 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ¬ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ↔ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))) |
82 | 41, 81 | pm2.61dan 832 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ↔ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))) |
83 | 82 | pm5.74da 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))))) |
84 | 3, 4 | unitcl 18659 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝑈 → 𝑥 ∈ 𝐵) |
85 | 3, 4 | unitcl 18659 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑈 → 𝑦 ∈ 𝐵) |
86 | 84, 85 | anim12i 590 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
87 | 86 | pm4.71ri 665 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈))) |
88 | 87 | imbi1i 339 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) ↔ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
89 | | impexp 462 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))) |
90 | 88, 89 | bitri 264 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))) |
91 | 83, 90 | syl6bbr 278 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) ↔ ((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))) |
92 | 91 | 2albidv 1851 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) → (∀𝑥∀𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))) |
93 | | r2al 2939 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
94 | | r2al 2939 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
95 | 92, 93, 94 | 3bitr4g 303 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ 𝑋:𝐵⟶ℂ) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ↔ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
96 | 95 | adantrr 753 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) ∧ (𝑋:𝐵⟶ℂ ∧ (𝑋‘(1r‘𝑍)) = 1)) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ↔ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
97 | 96 | pm5.32da 673 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) → (((𝑋:𝐵⟶ℂ ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) ↔ ((𝑋:𝐵⟶ℂ ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))))) |
98 | | 3anan32 1050 |
. . . . . . 7
⊢ ((𝑋:𝐵⟶ℂ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ↔ ((𝑋:𝐵⟶ℂ ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
99 | | an31 841 |
. . . . . . 7
⊢
(((∀𝑥 ∈
𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ 𝑋:𝐵⟶ℂ) ↔ ((𝑋:𝐵⟶ℂ ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
100 | 97, 98, 99 | 3bitr4g 303 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) → ((𝑋:𝐵⟶ℂ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ↔ ((∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ 𝑋:𝐵⟶ℂ))) |
101 | 39, 100 | bitrd 268 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑧 ∈ 𝐵 ((𝑋‘𝑧) ≠ 0 → 𝑧 ∈ 𝑈)) → (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ↔ ((∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ 𝑋:𝐵⟶ℂ))) |
102 | 12, 101 | sylan2br 493 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) → (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ↔ ((∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ 𝑋:𝐵⟶ℂ))) |
103 | 102 | pm5.32da 673 |
. . 3
⊢ (𝜑 → ((∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈) ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ↔ (∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈) ∧ ((∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ 𝑋:𝐵⟶ℂ)))) |
104 | | ancom 466 |
. . 3
⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) ↔ (∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈) ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)))) |
105 | | df-3an 1039 |
. . . . 5
⊢
((∀𝑥 ∈
𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) ↔ ((∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) |
106 | 105 | anbi2i 730 |
. . . 4
⊢ ((𝑋:𝐵⟶ℂ ∧ (∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) ↔ (𝑋:𝐵⟶ℂ ∧ ((∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)))) |
107 | | an13 840 |
. . . 4
⊢ ((𝑋:𝐵⟶ℂ ∧ ((∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) ↔ (∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈) ∧ ((∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ 𝑋:𝐵⟶ℂ))) |
108 | 106, 107 | bitri 264 |
. . 3
⊢ ((𝑋:𝐵⟶ℂ ∧ (∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))) ↔ (∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈) ∧ ((∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1) ∧ 𝑋:𝐵⟶ℂ))) |
109 | 103, 104,
108 | 3bitr4g 303 |
. 2
⊢ (𝜑 → ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈)) ↔ (𝑋:𝐵⟶ℂ ∧ (∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))))) |
110 | 7, 109 | bitrd 268 |
1
⊢ (𝜑 → (𝑋 ∈ 𝐷 ↔ (𝑋:𝐵⟶ℂ ∧ (∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ 𝑈))))) |