Step | Hyp | Ref
| Expression |
1 | | evls1fpws.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) |
2 | | ressply1evl.u |
. . . . . 6
⊢ 𝑈 = (𝑆 ↾s 𝑅) |
3 | 2 | subrgring 20343 |
. . . . 5
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring) |
4 | 1, 3 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ Ring) |
5 | | evls1fpws.y |
. . . 4
⊢ (𝜑 → 𝑀 ∈ 𝐵) |
6 | | ressply1evl.w |
. . . . 5
⊢ 𝑊 = (Poly1‘𝑈) |
7 | | eqid 2733 |
. . . . 5
⊢
(var1‘𝑈) = (var1‘𝑈) |
8 | | ressply1evl.b |
. . . . 5
⊢ 𝐵 = (Base‘𝑊) |
9 | | eqid 2733 |
. . . . 5
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
10 | | eqid 2733 |
. . . . 5
⊢
(mulGrp‘𝑊) =
(mulGrp‘𝑊) |
11 | | eqid 2733 |
. . . . 5
⊢
(.g‘(mulGrp‘𝑊)) =
(.g‘(mulGrp‘𝑊)) |
12 | | evls1fpws.a |
. . . . 5
⊢ 𝐴 = (coe1‘𝑀) |
13 | 6, 7, 8, 9, 10, 11, 12 | ply1coe 21789 |
. . . 4
⊢ ((𝑈 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 = (𝑊 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘)(
·𝑠 ‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))))) |
14 | 4, 5, 13 | syl2anc 585 |
. . 3
⊢ (𝜑 → 𝑀 = (𝑊 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘)(
·𝑠 ‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))))) |
15 | 14 | fveq2d 6885 |
. 2
⊢ (𝜑 → (𝑄‘𝑀) = (𝑄‘(𝑊 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘)(
·𝑠 ‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))))) |
16 | | ressply1evl.q |
. . . 4
⊢ 𝑄 = (𝑆 evalSub1 𝑅) |
17 | | ressply1evl.k |
. . . 4
⊢ 𝐾 = (Base‘𝑆) |
18 | | eqid 2733 |
. . . 4
⊢
(0g‘𝑊) = (0g‘𝑊) |
19 | | eqid 2733 |
. . . 4
⊢ (𝑆 ↑s 𝐾) = (𝑆 ↑s 𝐾) |
20 | | evls1fpws.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ CRing) |
21 | 6 | ply1lmod 21745 |
. . . . . . 7
⊢ (𝑈 ∈ Ring → 𝑊 ∈ LMod) |
22 | 4, 21 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ LMod) |
23 | 22 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑊 ∈ LMod) |
24 | | eqid 2733 |
. . . . . . . 8
⊢
(Base‘𝑈) =
(Base‘𝑈) |
25 | 12, 8, 6, 24 | coe1fvalcl 21705 |
. . . . . . 7
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘𝑈)) |
26 | 5, 25 | sylan 581 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘𝑈)) |
27 | 6 | ply1sca 21746 |
. . . . . . . . 9
⊢ (𝑈 ∈ Ring → 𝑈 = (Scalar‘𝑊)) |
28 | 4, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 = (Scalar‘𝑊)) |
29 | 28 | fveq2d 6885 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑈) =
(Base‘(Scalar‘𝑊))) |
30 | 29 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(Base‘𝑈) =
(Base‘(Scalar‘𝑊))) |
31 | 26, 30 | eleqtrd 2836 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑊))) |
32 | 10, 8 | mgpbas 19976 |
. . . . . 6
⊢ 𝐵 =
(Base‘(mulGrp‘𝑊)) |
33 | 6 | ply1ring 21741 |
. . . . . . . . 9
⊢ (𝑈 ∈ Ring → 𝑊 ∈ Ring) |
34 | 4, 33 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Ring) |
35 | 34 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑊 ∈ Ring) |
36 | 10 | ringmgp 20044 |
. . . . . . 7
⊢ (𝑊 ∈ Ring →
(mulGrp‘𝑊) ∈
Mnd) |
37 | 35, 36 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(mulGrp‘𝑊) ∈
Mnd) |
38 | | simpr 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
39 | 4 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑈 ∈ Ring) |
40 | 7, 6, 8 | vr1cl 21710 |
. . . . . . 7
⊢ (𝑈 ∈ Ring →
(var1‘𝑈)
∈ 𝐵) |
41 | 39, 40 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(var1‘𝑈)
∈ 𝐵) |
42 | 32, 11, 37, 38, 41 | mulgnn0cld 18960 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) |
43 | | eqid 2733 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
44 | | eqid 2733 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
45 | 8, 43, 9, 44 | lmodvscl 20466 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) → ((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) ∈ 𝐵) |
46 | 23, 31, 42, 45 | syl3anc 1372 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) ∈ 𝐵) |
47 | | ssidd 4003 |
. . . 4
⊢ (𝜑 → ℕ0
⊆ ℕ0) |
48 | | fvexd 6896 |
. . . . 5
⊢ (𝜑 → (0g‘𝑊) ∈ V) |
49 | | fveq2 6881 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗)) |
50 | | oveq1 7403 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)) = (𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) |
51 | 49, 50 | oveq12d 7414 |
. . . . 5
⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) |
52 | | eqid 2733 |
. . . . . . . 8
⊢
(0g‘𝑈) = (0g‘𝑈) |
53 | 12, 8, 6, 52 | coe1ae0 21709 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → ∃𝑖 ∈ ℕ0 ∀𝑗 ∈ ℕ0
(𝑖 < 𝑗 → (𝐴‘𝑗) = (0g‘𝑈))) |
54 | 5, 53 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∃𝑖 ∈ ℕ0 ∀𝑗 ∈ ℕ0
(𝑖 < 𝑗 → (𝐴‘𝑗) = (0g‘𝑈))) |
55 | | simpr 486 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → (𝐴‘𝑗) = (0g‘𝑈)) |
56 | 28 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → 𝑈 = (Scalar‘𝑊)) |
57 | 56 | fveq2d 6885 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) →
(0g‘𝑈) =
(0g‘(Scalar‘𝑊))) |
58 | 55, 57 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → (𝐴‘𝑗) = (0g‘(Scalar‘𝑊))) |
59 | 58 | oveq1d 7411 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) =
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) |
60 | 22 | ad3antrrr 729 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → 𝑊 ∈ LMod) |
61 | 34, 36 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (mulGrp‘𝑊) ∈ Mnd) |
62 | 61 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(mulGrp‘𝑊) ∈
Mnd) |
63 | | simpr 486 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
ℕ0) |
64 | 4, 40 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(var1‘𝑈)
∈ 𝐵) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(var1‘𝑈)
∈ 𝐵) |
66 | 32, 11, 62, 63, 65 | mulgnn0cld 18960 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) |
67 | 66 | ad4ant13 750 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → (𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) |
68 | | eqid 2733 |
. . . . . . . . . . . . 13
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
69 | 8, 43, 9, 68, 18 | lmod0vs 20482 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)) |
70 | 60, 67, 69 | syl2anc 585 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)) |
71 | 59, 70 | eqtrd 2773 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)) |
72 | 71 | ex 414 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ ((𝐴‘𝑗) = (0g‘𝑈) → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊))) |
73 | 72 | imim2d 57 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ ((𝑖 < 𝑗 → (𝐴‘𝑗) = (0g‘𝑈)) → (𝑖 < 𝑗 → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)))) |
74 | 73 | ralimdva 3168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
(∀𝑗 ∈
ℕ0 (𝑖 <
𝑗 → (𝐴‘𝑗) = (0g‘𝑈)) → ∀𝑗 ∈ ℕ0 (𝑖 < 𝑗 → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)))) |
75 | 74 | reximdva 3169 |
. . . . . 6
⊢ (𝜑 → (∃𝑖 ∈ ℕ0 ∀𝑗 ∈ ℕ0
(𝑖 < 𝑗 → (𝐴‘𝑗) = (0g‘𝑈)) → ∃𝑖 ∈ ℕ0 ∀𝑗 ∈ ℕ0
(𝑖 < 𝑗 → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)))) |
76 | 54, 75 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∃𝑖 ∈ ℕ0 ∀𝑗 ∈ ℕ0
(𝑖 < 𝑗 → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊))) |
77 | 48, 46, 51, 76 | mptnn0fsuppd 13950 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) finSupp
(0g‘𝑊)) |
78 | 16, 17, 6, 18, 2, 19, 8, 20, 1, 46, 47, 77 | evls1gsumadd 21812 |
. . 3
⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘)(
·𝑠 ‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))))) = ((𝑆 ↑s 𝐾) Σg (𝑘 ∈ ℕ0
↦ (𝑄‘((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))))) |
79 | 16, 17, 19, 2, 6 | evls1rhm 21810 |
. . . . . . . . 9
⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑊 RingHom (𝑆 ↑s 𝐾))) |
80 | 20, 1, 79 | syl2anc 585 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ (𝑊 RingHom (𝑆 ↑s 𝐾))) |
81 | 80 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑄 ∈ (𝑊 RingHom (𝑆 ↑s 𝐾))) |
82 | | eqid 2733 |
. . . . . . . . . 10
⊢
(algSc‘𝑊) =
(algSc‘𝑊) |
83 | 82, 43, 34, 22, 44, 8 | asclf 21407 |
. . . . . . . . 9
⊢ (𝜑 → (algSc‘𝑊):(Base‘(Scalar‘𝑊))⟶𝐵) |
84 | 83 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(algSc‘𝑊):(Base‘(Scalar‘𝑊))⟶𝐵) |
85 | 84, 31 | ffvelcdmd 7075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((algSc‘𝑊)‘(𝐴‘𝑘)) ∈ 𝐵) |
86 | | eqid 2733 |
. . . . . . . 8
⊢
(.r‘𝑊) = (.r‘𝑊) |
87 | | eqid 2733 |
. . . . . . . 8
⊢
(.r‘(𝑆 ↑s 𝐾)) = (.r‘(𝑆 ↑s 𝐾)) |
88 | 8, 86, 87 | rhmmul 20242 |
. . . . . . 7
⊢ ((𝑄 ∈ (𝑊 RingHom (𝑆 ↑s 𝐾)) ∧ ((algSc‘𝑊)‘(𝐴‘𝑘)) ∈ 𝐵 ∧ (𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) → (𝑄‘(((algSc‘𝑊)‘(𝐴‘𝑘))(.r‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘)))(.r‘(𝑆 ↑s 𝐾))(𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))) |
89 | 81, 85, 42, 88 | syl3anc 1372 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘(((algSc‘𝑊)‘(𝐴‘𝑘))(.r‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘)))(.r‘(𝑆 ↑s 𝐾))(𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))) |
90 | 2 | subrgcrng 20344 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing) |
91 | 20, 1, 90 | syl2anc 585 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ CRing) |
92 | 6 | ply1assa 21692 |
. . . . . . . . . 10
⊢ (𝑈 ∈ CRing → 𝑊 ∈ AssAlg) |
93 | 91, 92 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ AssAlg) |
94 | 93 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑊 ∈ AssAlg) |
95 | 82, 43, 44, 8, 86, 9 | asclmul1 21411 |
. . . . . . . 8
⊢ ((𝑊 ∈ AssAlg ∧ (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) → (((algSc‘𝑊)‘(𝐴‘𝑘))(.r‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = ((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) |
96 | 94, 31, 42, 95 | syl3anc 1372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(((algSc‘𝑊)‘(𝐴‘𝑘))(.r‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = ((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) |
97 | 96 | fveq2d 6885 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘(((algSc‘𝑊)‘(𝐴‘𝑘))(.r‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = (𝑄‘((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))) |
98 | | eqid 2733 |
. . . . . . . 8
⊢
(Base‘(𝑆
↑s 𝐾)) = (Base‘(𝑆 ↑s 𝐾)) |
99 | 20 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑆 ∈ CRing) |
100 | 17 | fvexi 6895 |
. . . . . . . . 9
⊢ 𝐾 ∈ V |
101 | 100 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐾 ∈ V) |
102 | 8, 98 | rhmf 20241 |
. . . . . . . . . 10
⊢ (𝑄 ∈ (𝑊 RingHom (𝑆 ↑s 𝐾)) → 𝑄:𝐵⟶(Base‘(𝑆 ↑s 𝐾))) |
103 | 81, 102 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑄:𝐵⟶(Base‘(𝑆 ↑s 𝐾))) |
104 | 103, 85 | ffvelcdmd 7075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘))) ∈ (Base‘(𝑆 ↑s 𝐾))) |
105 | 103, 42 | ffvelcdmd 7075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) ∈ (Base‘(𝑆 ↑s 𝐾))) |
106 | | evls1fpws.1 |
. . . . . . . 8
⊢ · =
(.r‘𝑆) |
107 | 19, 98, 99, 101, 104, 105, 106, 87 | pwsmulrval 17424 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘)))(.r‘(𝑆 ↑s 𝐾))(𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘))) ∘f · (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))) |
108 | 19, 17, 98, 99, 101, 104 | pwselbas 17422 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘))):𝐾⟶𝐾) |
109 | 108 | ffnd 6708 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘))) Fn 𝐾) |
110 | 19, 17, 98, 99, 101, 105 | pwselbas 17422 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))):𝐾⟶𝐾) |
111 | 110 | ffnd 6708 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) Fn 𝐾) |
112 | | inidm 4216 |
. . . . . . . 8
⊢ (𝐾 ∩ 𝐾) = 𝐾 |
113 | 20 | ad2antrr 725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → 𝑆 ∈ CRing) |
114 | 1 | ad2antrr 725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → 𝑅 ∈ (SubRing‘𝑆)) |
115 | 17 | subrgss 20341 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾) |
116 | 1, 115 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ⊆ 𝐾) |
117 | 2, 17 | ressbas2 17169 |
. . . . . . . . . . . . 13
⊢ (𝑅 ⊆ 𝐾 → 𝑅 = (Base‘𝑈)) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 = (Base‘𝑈)) |
119 | 118 | adantr 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑅 = (Base‘𝑈)) |
120 | 26, 119 | eleqtrrd 2837 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ 𝑅) |
121 | 120 | adantr 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → (𝐴‘𝑘) ∈ 𝑅) |
122 | | simpr 486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → 𝑥 ∈ 𝐾) |
123 | 16, 6, 2, 17, 82, 113, 114, 121, 122 | evls1scafv 32586 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘)))‘𝑥) = (𝐴‘𝑘)) |
124 | | evls1fpws.2 |
. . . . . . . . 9
⊢ ↑ =
(.g‘(mulGrp‘𝑆)) |
125 | | simplr 768 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → 𝑘 ∈ ℕ0) |
126 | 16, 2, 6, 7, 17, 11, 124, 113, 114, 125, 122 | evls1varpwval 32588 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → ((𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))‘𝑥) = (𝑘 ↑ 𝑥)) |
127 | 109, 111,
101, 101, 112, 123, 126 | offval 7666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘))) ∘f · (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) |
128 | 107, 127 | eqtrd 2773 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘)))(.r‘(𝑆 ↑s 𝐾))(𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) |
129 | 89, 97, 128 | 3eqtr3d 2781 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) |
130 | 129 | mpteq2dva 5244 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (𝑄‘((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))) = (𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))))) |
131 | 130 | oveq2d 7412 |
. . 3
⊢ (𝜑 → ((𝑆 ↑s 𝐾) Σg (𝑘 ∈ ℕ0
↦ (𝑄‘((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))))) = ((𝑆 ↑s 𝐾) Σg (𝑘 ∈ ℕ0
↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))))) |
132 | | eqid 2733 |
. . . 4
⊢
(0g‘(𝑆 ↑s 𝐾)) = (0g‘(𝑆 ↑s 𝐾)) |
133 | 100 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ V) |
134 | | nn0ex 12465 |
. . . . 5
⊢
ℕ0 ∈ V |
135 | 134 | a1i 11 |
. . . 4
⊢ (𝜑 → ℕ0 ∈
V) |
136 | 20 | crngringd 20051 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ Ring) |
137 | 136 | ringcmnd 20082 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ CMnd) |
138 | 136 | ad2antrr 725 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → 𝑆 ∈ Ring) |
139 | 1 | adantr 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ (SubRing‘𝑆)) |
140 | 139, 115 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑅 ⊆ 𝐾) |
141 | 140, 120 | sseldd 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ 𝐾) |
142 | 141 | adantr 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → (𝐴‘𝑘) ∈ 𝐾) |
143 | | eqid 2733 |
. . . . . . . . . 10
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
144 | 143, 17 | mgpbas 19976 |
. . . . . . . . 9
⊢ 𝐾 =
(Base‘(mulGrp‘𝑆)) |
145 | 143 | ringmgp 20044 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) |
146 | 136, 145 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) |
147 | 146 | ad2antrr 725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → (mulGrp‘𝑆) ∈ Mnd) |
148 | 144, 124,
147, 125, 122 | mulgnn0cld 18960 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → (𝑘 ↑ 𝑥) ∈ 𝐾) |
149 | 17, 106, 138, 142, 148 | ringcld 20061 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) ∈ 𝐾) |
150 | 149 | 3impa 1111 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝑥 ∈ 𝐾) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) ∈ 𝐾) |
151 | 150 | 3com23 1127 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) ∈ 𝐾) |
152 | 151 | 3expb 1121 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0)) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) ∈ 𝐾) |
153 | 135 | mptexd 7213 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) ∈ V) |
154 | | funmpt 6578 |
. . . . . 6
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) |
155 | 154 | a1i 11 |
. . . . 5
⊢ (𝜑 → Fun (𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))))) |
156 | | fvexd 6896 |
. . . . 5
⊢ (𝜑 →
(0g‘(𝑆
↑s 𝐾)) ∈ V) |
157 | 12, 8, 6, 52 | coe1sfi 21706 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐵 → 𝐴 finSupp (0g‘𝑈)) |
158 | 5, 157 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴 finSupp (0g‘𝑈)) |
159 | 158 | fsuppimpd 9357 |
. . . . 5
⊢ (𝜑 → (𝐴 supp (0g‘𝑈)) ∈ Fin) |
160 | 12, 8, 6, 24 | coe1f 21704 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ 𝐵 → 𝐴:ℕ0⟶(Base‘𝑈)) |
161 | 5, 160 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴:ℕ0⟶(Base‘𝑈)) |
162 | 161 | ffnd 6708 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 Fn ℕ0) |
163 | 162 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → 𝐴 Fn ℕ0) |
164 | 134 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → ℕ0
∈ V) |
165 | | fvexd 6896 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) →
(0g‘𝑈)
∈ V) |
166 | | simpr 486 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) |
167 | 163, 164,
165, 166 | fvdifsupp 31877 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝐴‘𝑘) = (0g‘𝑈)) |
168 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
⊢
(0g‘𝑆) = (0g‘𝑆) |
169 | 2, 168 | subrg0 20347 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ (SubRing‘𝑆) →
(0g‘𝑆) =
(0g‘𝑈)) |
170 | 1, 169 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝑆) = (0g‘𝑈)) |
171 | 170 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) →
(0g‘𝑆) =
(0g‘𝑈)) |
172 | 167, 171 | eqtr4d 2776 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝐴‘𝑘) = (0g‘𝑆)) |
173 | 172 | adantr 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → (𝐴‘𝑘) = (0g‘𝑆)) |
174 | 173 | oveq1d 7411 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) = ((0g‘𝑆) · (𝑘 ↑ 𝑥))) |
175 | 136 | ad2antrr 725 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → 𝑆 ∈ Ring) |
176 | 175, 145 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → (mulGrp‘𝑆) ∈ Mnd) |
177 | | simplr 768 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) |
178 | 177 | eldifad 3958 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → 𝑘 ∈ ℕ0) |
179 | | simpr 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → 𝑥 ∈ 𝐾) |
180 | 144, 124,
176, 178, 179 | mulgnn0cld 18960 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → (𝑘 ↑ 𝑥) ∈ 𝐾) |
181 | 17, 106, 168 | ringlz 20088 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Ring ∧ (𝑘 ↑ 𝑥) ∈ 𝐾) → ((0g‘𝑆) · (𝑘 ↑ 𝑥)) = (0g‘𝑆)) |
182 | 175, 180,
181 | syl2anc 585 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → ((0g‘𝑆) · (𝑘 ↑ 𝑥)) = (0g‘𝑆)) |
183 | 174, 182 | eqtrd 2773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) = (0g‘𝑆)) |
184 | 183 | mpteq2dva 5244 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))) = (𝑥 ∈ 𝐾 ↦ (0g‘𝑆))) |
185 | | fconstmpt 5733 |
. . . . . . . 8
⊢ (𝐾 ×
{(0g‘𝑆)})
= (𝑥 ∈ 𝐾 ↦
(0g‘𝑆)) |
186 | 184, 185 | eqtr4di 2791 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))) = (𝐾 × {(0g‘𝑆)})) |
187 | 137 | cmnmndd 19656 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ Mnd) |
188 | 19, 168 | pws0g 18648 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Mnd ∧ 𝐾 ∈ V) → (𝐾 ×
{(0g‘𝑆)})
= (0g‘(𝑆
↑s 𝐾))) |
189 | 187, 133,
188 | syl2anc 585 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 × {(0g‘𝑆)}) =
(0g‘(𝑆
↑s 𝐾))) |
190 | 189 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝐾 × {(0g‘𝑆)}) =
(0g‘(𝑆
↑s 𝐾))) |
191 | 186, 190 | eqtrd 2773 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))) = (0g‘(𝑆 ↑s 𝐾))) |
192 | 191, 135 | suppss2 8172 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) supp (0g‘(𝑆 ↑s 𝐾))) ⊆ (𝐴 supp (0g‘𝑈))) |
193 | | suppssfifsupp 9366 |
. . . . 5
⊢ ((((𝑘 ∈ ℕ0
↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) ∈ V ∧ Fun (𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) ∧ (0g‘(𝑆 ↑s 𝐾)) ∈ V) ∧ ((𝐴 supp (0g‘𝑈)) ∈ Fin ∧ ((𝑘 ∈ ℕ0
↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) supp (0g‘(𝑆 ↑s 𝐾))) ⊆ (𝐴 supp (0g‘𝑈)))) → (𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) finSupp (0g‘(𝑆 ↑s 𝐾))) |
194 | 153, 155,
156, 159, 192, 193 | syl32anc 1379 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) finSupp (0g‘(𝑆 ↑s 𝐾))) |
195 | 19, 17, 132, 133, 135, 137, 152, 194 | pwsgsum 19833 |
. . 3
⊢ (𝜑 → ((𝑆 ↑s 𝐾) Σg (𝑘 ∈ ℕ0
↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))))) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))))) |
196 | 78, 131, 195 | 3eqtrd 2777 |
. 2
⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘)(
·𝑠 ‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))))) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))))) |
197 | 15, 196 | eqtrd 2773 |
1
⊢ (𝜑 → (𝑄‘𝑀) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))))) |