Step | Hyp | Ref
| Expression |
1 | | mhphf.i |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
2 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝐼 ∈ 𝑉) |
3 | | mhphf.l |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ 𝑅) |
4 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝐿 ∈ 𝑅) |
5 | | mhphf.a |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) |
6 | | elmapi 8849 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (𝐾 ↑m 𝐼) → 𝐴:𝐼⟶𝐾) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴:𝐼⟶𝐾) |
8 | 7 | ffnd 6718 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 Fn 𝐼) |
9 | 8 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝐴 Fn 𝐼) |
10 | | eqidd 2732 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (𝐴‘𝑖) = (𝐴‘𝑖)) |
11 | 2, 4, 9, 10 | ofc1 7700 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖) = (𝐿 · (𝐴‘𝑖))) |
12 | 11 | oveq2d 7428 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)) = ((𝑏‘𝑖) ↑ (𝐿 · (𝐴‘𝑖)))) |
13 | | mhphf.s |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ CRing) |
14 | | eqid 2731 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
15 | 14 | crngmgp 20142 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ CRing →
(mulGrp‘𝑆) ∈
CMnd) |
16 | 13, 15 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (mulGrp‘𝑆) ∈ CMnd) |
17 | 16 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (mulGrp‘𝑆) ∈ CMnd) |
18 | | elrabi 3677 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} → 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
19 | | eqid 2731 |
. . . . . . . . . . . . . . . 16
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
20 | 19 | psrbagf 21781 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑏:𝐼⟶ℕ0) |
21 | 18, 20 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} → 𝑏:𝐼⟶ℕ0) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝑏:𝐼⟶ℕ0) |
23 | 22 | ffvelcdmda 7086 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (𝑏‘𝑖) ∈
ℕ0) |
24 | | mhphf.r |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) |
25 | | mhphf.k |
. . . . . . . . . . . . . . . 16
⊢ 𝐾 = (Base‘𝑆) |
26 | 25 | subrgss 20470 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾) |
27 | 24, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ⊆ 𝐾) |
28 | 27, 3 | sseldd 3983 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ 𝐾) |
29 | 28 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → 𝐿 ∈ 𝐾) |
30 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝐴:𝐼⟶𝐾) |
31 | 30 | ffvelcdmda 7086 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (𝐴‘𝑖) ∈ 𝐾) |
32 | 14, 25 | mgpbas 20041 |
. . . . . . . . . . . . 13
⊢ 𝐾 =
(Base‘(mulGrp‘𝑆)) |
33 | | mhphf.e |
. . . . . . . . . . . . 13
⊢ ↑ =
(.g‘(mulGrp‘𝑆)) |
34 | | mhphf.m |
. . . . . . . . . . . . . 14
⊢ · =
(.r‘𝑆) |
35 | 14, 34 | mgpplusg 20039 |
. . . . . . . . . . . . 13
⊢ · =
(+g‘(mulGrp‘𝑆)) |
36 | 32, 33, 35 | mulgnn0di 19741 |
. . . . . . . . . . . 12
⊢
(((mulGrp‘𝑆)
∈ CMnd ∧ ((𝑏‘𝑖) ∈ ℕ0 ∧ 𝐿 ∈ 𝐾 ∧ (𝐴‘𝑖) ∈ 𝐾)) → ((𝑏‘𝑖) ↑ (𝐿 · (𝐴‘𝑖))) = (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) |
37 | 17, 23, 29, 31, 36 | syl13anc 1371 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (𝐿 · (𝐴‘𝑖))) = (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) |
38 | 12, 37 | eqtrd 2771 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)) = (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) |
39 | 38 | mpteq2dva 5248 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))) = (𝑖 ∈ 𝐼 ↦ (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) |
40 | 39 | oveq2d 7428 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))) = ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) |
41 | | eqid 2731 |
. . . . . . . . . 10
⊢
(1r‘𝑆) = (1r‘𝑆) |
42 | 14, 41 | ringidval 20084 |
. . . . . . . . 9
⊢
(1r‘𝑆) = (0g‘(mulGrp‘𝑆)) |
43 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝑆 ∈ CRing) |
44 | 43, 15 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (mulGrp‘𝑆) ∈ CMnd) |
45 | 13 | crngringd 20147 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Ring) |
46 | 14 | ringmgp 20140 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) |
48 | 47 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → (mulGrp‘𝑆) ∈ Mnd) |
49 | 32, 33, 48, 23, 29 | mulgnn0cld 19018 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ 𝐿) ∈ 𝐾) |
50 | 32, 33, 48, 23, 31 | mulgnn0cld 19018 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖) ↑ (𝐴‘𝑖)) ∈ 𝐾) |
51 | | eqidd 2732 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) |
52 | | eqidd 2732 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) |
53 | 1 | mptexd 7228 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) ∈ V) |
54 | 53 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) ∈ V) |
55 | | fvexd 6906 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (1r‘𝑆) ∈ V) |
56 | | funmpt 6586 |
. . . . . . . . . . 11
⊢ Fun
(𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) |
57 | 56 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → Fun (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) |
58 | 19 | psrbagfsupp 21783 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑏 finSupp 0) |
59 | 18, 58 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} → 𝑏 finSupp 0) |
60 | 59 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝑏 finSupp 0) |
61 | 22 | feqmptd 6960 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝑏 = (𝑖 ∈ 𝐼 ↦ (𝑏‘𝑖))) |
62 | 61 | oveq1d 7427 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑏 supp 0) = ((𝑖 ∈ 𝐼 ↦ (𝑏‘𝑖)) supp 0)) |
63 | 62 | eqimsscd 4039 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑖 ∈ 𝐼 ↦ (𝑏‘𝑖)) supp 0) ⊆ (𝑏 supp 0)) |
64 | 32, 42, 33 | mulg0 19000 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐾 → (0 ↑ 𝑘) = (1r‘𝑆)) |
65 | 64 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑘 ∈ 𝐾) → (0 ↑ 𝑘) = (1r‘𝑆)) |
66 | | 0zd 12577 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 0 ∈ ℤ) |
67 | 63, 65, 23, 29, 66 | suppssov1 8188 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) supp (1r‘𝑆)) ⊆ (𝑏 supp 0)) |
68 | 54, 55, 57, 60, 67 | fsuppsssuppgd 41533 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿)) finSupp (1r‘𝑆)) |
69 | 1 | mptexd 7228 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) ∈ V) |
70 | 69 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) ∈ V) |
71 | | funmpt 6586 |
. . . . . . . . . . 11
⊢ Fun
(𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) |
72 | 71 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → Fun (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) |
73 | 63, 65, 23, 31, 66 | suppssov1 8188 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) supp (1r‘𝑆)) ⊆ (𝑏 supp 0)) |
74 | 70, 55, 72, 60, 73 | fsuppsssuppgd 41533 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) finSupp (1r‘𝑆)) |
75 | 32, 42, 35, 44, 2, 49, 50, 51, 52, 68, 74 | gsummptfsadd 19840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ (((𝑏‘𝑖) ↑ 𝐿) · ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) = (((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) |
76 | | eqid 2731 |
. . . . . . . . . 10
⊢ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} = {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} |
77 | | mhphf.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
78 | 19, 76, 32, 33, 1, 47, 28, 77 | mhphflem 41633 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) = (𝑁 ↑ 𝐿)) |
79 | 78 | oveq1d 7427 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ 𝐿))) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) = ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) |
80 | 40, 75, 79 | 3eqtrd 2775 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))) = ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) |
81 | 80 | oveq2d 7428 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))) = ((𝑋‘𝑏) · ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) |
82 | | eqid 2731 |
. . . . . . . . . . 11
⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly 𝑈) |
83 | | eqid 2731 |
. . . . . . . . . . 11
⊢
(Base‘𝑈) =
(Base‘𝑈) |
84 | | eqid 2731 |
. . . . . . . . . . 11
⊢
(Base‘(𝐼 mPoly
𝑈)) = (Base‘(𝐼 mPoly 𝑈)) |
85 | | mhphf.h |
. . . . . . . . . . . 12
⊢ 𝐻 = (𝐼 mHomP 𝑈) |
86 | | mhphf.u |
. . . . . . . . . . . . . 14
⊢ 𝑈 = (𝑆 ↾s 𝑅) |
87 | 86 | ovexi 7446 |
. . . . . . . . . . . . 13
⊢ 𝑈 ∈ V |
88 | 87 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ V) |
89 | | mhphf.x |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) |
90 | 85, 82, 84, 1, 88, 77, 89 | mhpmpl 21996 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (Base‘(𝐼 mPoly 𝑈))) |
91 | 82, 83, 84, 19, 90 | mplelf 21868 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑈)) |
92 | 86 | subrgbas 20479 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈)) |
93 | 92, 26 | eqsstrrd 4021 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ (SubRing‘𝑆) → (Base‘𝑈) ⊆ 𝐾) |
94 | 24, 93 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑈) ⊆ 𝐾) |
95 | 91, 94 | fssd 6735 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋:{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}⟶𝐾) |
96 | 95 | ffvelcdmda 7086 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑋‘𝑏) ∈ 𝐾) |
97 | 18, 96 | sylan2 592 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑋‘𝑏) ∈ 𝐾) |
98 | 32, 33, 47, 77, 28 | mulgnn0cld 19018 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ 𝐾) |
99 | 98 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑁 ↑ 𝐿) ∈ 𝐾) |
100 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐼 ∈ 𝑉) |
101 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑆 ∈ CRing) |
102 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝐴 ∈ (𝐾 ↑m 𝐼)) |
103 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
104 | 19, 25, 14, 33, 100, 101, 102, 103 | evlsvvvallem 41598 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) →
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) ∈ 𝐾) |
105 | 18, 104 | sylan2 592 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) ∈ 𝐾) |
106 | 25, 34, 43, 97, 99, 105 | crng12d 41555 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) · ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) = ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) |
107 | 81, 106 | eqtrd 2771 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))) = ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) |
108 | 107 | mpteq2dva 5248 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))))) = (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) |
109 | 108 | oveq2d 7428 |
. . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))))) = (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))) |
110 | | eqid 2731 |
. . . 4
⊢
(0g‘𝑆) = (0g‘𝑆) |
111 | | ovex 7445 |
. . . . . . 7
⊢
(ℕ0 ↑m 𝐼) ∈ V |
112 | 111 | rabex 5332 |
. . . . . 6
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V |
113 | 112 | rabex 5332 |
. . . . 5
⊢ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∈ V |
114 | 113 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∈ V) |
115 | 45 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑆 ∈ Ring) |
116 | 25, 34, 115, 96, 104 | ringcld 20158 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) ∈ 𝐾) |
117 | 18, 116 | sylan2 592 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) ∈ 𝐾) |
118 | | ssrab2 4077 |
. . . . . 6
⊢ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ⊆ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
119 | | mptss 6042 |
. . . . . 6
⊢ ({𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ⊆ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) ⊆ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) |
120 | 118, 119 | mp1i 13 |
. . . . 5
⊢ (𝜑 → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) ⊆ (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) |
121 | 19, 82, 86, 84, 25, 14, 33, 34, 1, 13, 24, 90, 5 | evlsvvvallem2 41599 |
. . . . 5
⊢ (𝜑 → (𝑏 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) finSupp (0g‘𝑆)) |
122 | 120, 121 | fsuppss 41534 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) finSupp (0g‘𝑆)) |
123 | 25, 110, 34, 45, 114, 98, 117, 122 | gsummulc2 20212 |
. . 3
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑁 ↑ 𝐿) · ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) = ((𝑁 ↑ 𝐿) · (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))) |
124 | 109, 123 | eqtrd 2771 |
. 2
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖))))))) = ((𝑁 ↑ 𝐿) · (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))) |
125 | | mhphf.q |
. . 3
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) |
126 | 25 | fvexi 6905 |
. . . . 5
⊢ 𝐾 ∈ V |
127 | 126 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ V) |
128 | 25, 34 | ringcl 20151 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾) |
129 | 45, 128 | syl3an1 1162 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾) |
130 | 129 | 3expb 1119 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾)) → (𝑗 · 𝑘) ∈ 𝐾) |
131 | | fconst6g 6780 |
. . . . . 6
⊢ (𝐿 ∈ 𝐾 → (𝐼 × {𝐿}):𝐼⟶𝐾) |
132 | 28, 131 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐼 × {𝐿}):𝐼⟶𝐾) |
133 | | inidm 4218 |
. . . . 5
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
134 | 130, 132,
7, 1, 1, 133 | off 7692 |
. . . 4
⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼⟶𝐾) |
135 | 127, 1, 134 | elmapdd 8841 |
. . 3
⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼)) |
136 | 125, 85, 86, 19, 76, 25, 14, 33, 34, 1, 13, 24, 77, 89, 135 | evlsmhpvvval 41632 |
. 2
⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑖)))))))) |
137 | 125, 85, 86, 19, 76, 25, 14, 33, 34, 1, 13, 24, 77, 89, 5 | evlsmhpvvval 41632 |
. . 3
⊢ (𝜑 → ((𝑄‘𝑋)‘𝐴) = (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) |
138 | 137 | oveq2d 7428 |
. 2
⊢ (𝜑 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)) = ((𝑁 ↑ 𝐿) · (𝑆 Σg (𝑏 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ↦ ((𝑋‘𝑏) ·
((mulGrp‘𝑆)
Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))))) |
139 | 124, 136,
138 | 3eqtr4d 2781 |
1
⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) |