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