| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | evls1fpws.r | . . . . 5
⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) | 
| 2 |  | ressply1evl2.u | . . . . . 6
⊢ 𝑈 = (𝑆 ↾s 𝑅) | 
| 3 | 2 | subrgring 20575 | . . . . 5
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring) | 
| 4 | 1, 3 | syl 17 | . . . 4
⊢ (𝜑 → 𝑈 ∈ Ring) | 
| 5 |  | evls1fpws.y | . . . 4
⊢ (𝜑 → 𝑀 ∈ 𝐵) | 
| 6 |  | ressply1evl2.w | . . . . 5
⊢ 𝑊 = (Poly1‘𝑈) | 
| 7 |  | eqid 2736 | . . . . 5
⊢
(var1‘𝑈) = (var1‘𝑈) | 
| 8 |  | ressply1evl2.b | . . . . 5
⊢ 𝐵 = (Base‘𝑊) | 
| 9 |  | eqid 2736 | . . . . 5
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) | 
| 10 |  | eqid 2736 | . . . . 5
⊢
(mulGrp‘𝑊) =
(mulGrp‘𝑊) | 
| 11 |  | eqid 2736 | . . . . 5
⊢
(.g‘(mulGrp‘𝑊)) =
(.g‘(mulGrp‘𝑊)) | 
| 12 |  | evls1fpws.a | . . . . 5
⊢ 𝐴 = (coe1‘𝑀) | 
| 13 | 6, 7, 8, 9, 10, 11, 12 | ply1coe 22303 | . . . 4
⊢ ((𝑈 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 = (𝑊 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘)(
·𝑠 ‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))))) | 
| 14 | 4, 5, 13 | syl2anc 584 | . . 3
⊢ (𝜑 → 𝑀 = (𝑊 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘)(
·𝑠 ‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))))) | 
| 15 | 14 | fveq2d 6909 | . 2
⊢ (𝜑 → (𝑄‘𝑀) = (𝑄‘(𝑊 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘)(
·𝑠 ‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))))) | 
| 16 |  | ressply1evl2.q | . . . 4
⊢ 𝑄 = (𝑆 evalSub1 𝑅) | 
| 17 |  | ressply1evl2.k | . . . 4
⊢ 𝐾 = (Base‘𝑆) | 
| 18 |  | eqid 2736 | . . . 4
⊢
(0g‘𝑊) = (0g‘𝑊) | 
| 19 |  | eqid 2736 | . . . 4
⊢ (𝑆 ↑s 𝐾) = (𝑆 ↑s 𝐾) | 
| 20 |  | evls1fpws.s | . . . 4
⊢ (𝜑 → 𝑆 ∈ CRing) | 
| 21 | 6 | ply1lmod 22254 | . . . . . . 7
⊢ (𝑈 ∈ Ring → 𝑊 ∈ LMod) | 
| 22 | 4, 21 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ LMod) | 
| 23 | 22 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑊 ∈ LMod) | 
| 24 |  | eqid 2736 | . . . . . . . 8
⊢
(Base‘𝑈) =
(Base‘𝑈) | 
| 25 | 12, 8, 6, 24 | coe1fvalcl 22215 | . . . . . . 7
⊢ ((𝑀 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘𝑈)) | 
| 26 | 5, 25 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘𝑈)) | 
| 27 | 6 | ply1sca 22255 | . . . . . . . . 9
⊢ (𝑈 ∈ Ring → 𝑈 = (Scalar‘𝑊)) | 
| 28 | 4, 27 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑈 = (Scalar‘𝑊)) | 
| 29 | 28 | fveq2d 6909 | . . . . . . 7
⊢ (𝜑 → (Base‘𝑈) =
(Base‘(Scalar‘𝑊))) | 
| 30 | 29 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(Base‘𝑈) =
(Base‘(Scalar‘𝑊))) | 
| 31 | 26, 30 | eleqtrd 2842 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑊))) | 
| 32 | 10, 8 | mgpbas 20143 | . . . . . 6
⊢ 𝐵 =
(Base‘(mulGrp‘𝑊)) | 
| 33 | 6 | ply1ring 22250 | . . . . . . . . 9
⊢ (𝑈 ∈ Ring → 𝑊 ∈ Ring) | 
| 34 | 4, 33 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ Ring) | 
| 35 | 34 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑊 ∈ Ring) | 
| 36 | 10 | ringmgp 20237 | . . . . . . 7
⊢ (𝑊 ∈ Ring →
(mulGrp‘𝑊) ∈
Mnd) | 
| 37 | 35, 36 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(mulGrp‘𝑊) ∈
Mnd) | 
| 38 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) | 
| 39 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑈 ∈ Ring) | 
| 40 | 7, 6, 8 | vr1cl 22220 | . . . . . . 7
⊢ (𝑈 ∈ Ring →
(var1‘𝑈)
∈ 𝐵) | 
| 41 | 39, 40 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(var1‘𝑈)
∈ 𝐵) | 
| 42 | 32, 11, 37, 38, 41 | mulgnn0cld 19114 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) | 
| 43 |  | eqid 2736 | . . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 44 |  | eqid 2736 | . . . . . 6
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 45 | 8, 43, 9, 44 | lmodvscl 20877 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝐴‘𝑘) ∈ (Base‘(Scalar‘𝑊)) ∧ (𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) → ((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) ∈ 𝐵) | 
| 46 | 23, 31, 42, 45 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) ∈ 𝐵) | 
| 47 |  | ssidd 4006 | . . . 4
⊢ (𝜑 → ℕ0
⊆ ℕ0) | 
| 48 |  | fvexd 6920 | . . . . 5
⊢ (𝜑 → (0g‘𝑊) ∈ V) | 
| 49 |  | fveq2 6905 | . . . . . 6
⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗)) | 
| 50 |  | oveq1 7439 | . . . . . 6
⊢ (𝑘 = 𝑗 → (𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)) = (𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) | 
| 51 | 49, 50 | oveq12d 7450 | . . . . 5
⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) | 
| 52 |  | eqid 2736 | . . . . . . . 8
⊢
(0g‘𝑈) = (0g‘𝑈) | 
| 53 | 12, 8, 6, 52 | coe1ae0 22219 | . . . . . . 7
⊢ (𝑀 ∈ 𝐵 → ∃𝑖 ∈ ℕ0 ∀𝑗 ∈ ℕ0
(𝑖 < 𝑗 → (𝐴‘𝑗) = (0g‘𝑈))) | 
| 54 | 5, 53 | syl 17 | . . . . . 6
⊢ (𝜑 → ∃𝑖 ∈ ℕ0 ∀𝑗 ∈ ℕ0
(𝑖 < 𝑗 → (𝐴‘𝑗) = (0g‘𝑈))) | 
| 55 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → (𝐴‘𝑗) = (0g‘𝑈)) | 
| 56 | 28 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → 𝑈 = (Scalar‘𝑊)) | 
| 57 | 56 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) →
(0g‘𝑈) =
(0g‘(Scalar‘𝑊))) | 
| 58 | 55, 57 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → (𝐴‘𝑗) = (0g‘(Scalar‘𝑊))) | 
| 59 | 58 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) =
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) | 
| 60 | 22 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → 𝑊 ∈ LMod) | 
| 61 | 34, 36 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (mulGrp‘𝑊) ∈ Mnd) | 
| 62 | 61 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(mulGrp‘𝑊) ∈
Mnd) | 
| 63 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
ℕ0) | 
| 64 | 4, 40 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
(var1‘𝑈)
∈ 𝐵) | 
| 65 | 64 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(var1‘𝑈)
∈ 𝐵) | 
| 66 | 32, 11, 62, 63, 65 | mulgnn0cld 19114 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) | 
| 67 | 66 | ad4ant13 751 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → (𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) | 
| 68 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) | 
| 69 | 8, 43, 9, 68, 18 | lmod0vs 20894 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈)) ∈ 𝐵) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)) | 
| 70 | 60, 67, 69 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) →
((0g‘(Scalar‘𝑊))( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)) | 
| 71 | 59, 70 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
∧ (𝐴‘𝑗) = (0g‘𝑈)) → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)) | 
| 72 | 71 | ex 412 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ ((𝐴‘𝑗) = (0g‘𝑈) → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊))) | 
| 73 | 72 | imim2d 57 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑗 ∈ ℕ0)
→ ((𝑖 < 𝑗 → (𝐴‘𝑗) = (0g‘𝑈)) → (𝑖 < 𝑗 → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)))) | 
| 74 | 73 | ralimdva 3166 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
(∀𝑗 ∈
ℕ0 (𝑖 <
𝑗 → (𝐴‘𝑗) = (0g‘𝑈)) → ∀𝑗 ∈ ℕ0 (𝑖 < 𝑗 → ((𝐴‘𝑗)( ·𝑠
‘𝑊)(𝑗(.g‘(mulGrp‘𝑊))(var1‘𝑈))) = (0g‘𝑊)))) | 
| 75 | 74 | reximdva 3167 | . . . . . 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 14040 | . . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) finSupp
(0g‘𝑊)) | 
| 78 | 16, 17, 6, 18, 2, 19, 8, 20, 1, 46, 47, 77 | evls1gsumadd 22329 | . . 3
⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘)(
·𝑠 ‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))))) = ((𝑆 ↑s 𝐾) Σg (𝑘 ∈ ℕ0
↦ (𝑄‘((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))))) | 
| 79 | 16, 17, 19, 2, 6 | evls1rhm 22327 | . . . . . . . . 9
⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑊 RingHom (𝑆 ↑s 𝐾))) | 
| 80 | 20, 1, 79 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ (𝑊 RingHom (𝑆 ↑s 𝐾))) | 
| 81 | 80 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑄 ∈ (𝑊 RingHom (𝑆 ↑s 𝐾))) | 
| 82 |  | eqid 2736 | . . . . . . . . . 10
⊢
(algSc‘𝑊) =
(algSc‘𝑊) | 
| 83 | 82, 43, 34, 22, 44, 8 | asclf 21903 | . . . . . . . . 9
⊢ (𝜑 → (algSc‘𝑊):(Base‘(Scalar‘𝑊))⟶𝐵) | 
| 84 | 83 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(algSc‘𝑊):(Base‘(Scalar‘𝑊))⟶𝐵) | 
| 85 | 84, 31 | ffvelcdmd 7104 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((algSc‘𝑊)‘(𝐴‘𝑘)) ∈ 𝐵) | 
| 86 |  | eqid 2736 | . . . . . . . 8
⊢
(.r‘𝑊) = (.r‘𝑊) | 
| 87 |  | eqid 2736 | . . . . . . . 8
⊢
(.r‘(𝑆 ↑s 𝐾)) = (.r‘(𝑆 ↑s 𝐾)) | 
| 88 | 8, 86, 87 | rhmmul 20487 | . . . . . . 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 20576 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing) | 
| 91 | 20, 1, 90 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ CRing) | 
| 92 | 6 | ply1assa 22202 | . . . . . . . . . 10
⊢ (𝑈 ∈ CRing → 𝑊 ∈ AssAlg) | 
| 93 | 91, 92 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ AssAlg) | 
| 94 | 93 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑊 ∈ AssAlg) | 
| 95 | 82, 43, 44, 8, 86, 9 | asclmul1 21907 | . . . . . . . 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 6909 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘(((algSc‘𝑊)‘(𝐴‘𝑘))(.r‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = (𝑄‘((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))) | 
| 98 |  | eqid 2736 | . . . . . . . 8
⊢
(Base‘(𝑆
↑s 𝐾)) = (Base‘(𝑆 ↑s 𝐾)) | 
| 99 | 20 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑆 ∈ CRing) | 
| 100 | 17 | fvexi 6919 | . . . . . . . . 9
⊢ 𝐾 ∈ V | 
| 101 | 100 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐾 ∈ V) | 
| 102 | 8, 98 | rhmf 20486 | . . . . . . . . . 10
⊢ (𝑄 ∈ (𝑊 RingHom (𝑆 ↑s 𝐾)) → 𝑄:𝐵⟶(Base‘(𝑆 ↑s 𝐾))) | 
| 103 | 81, 102 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑄:𝐵⟶(Base‘(𝑆 ↑s 𝐾))) | 
| 104 | 103, 85 | ffvelcdmd 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘))) ∈ (Base‘(𝑆 ↑s 𝐾))) | 
| 105 | 103, 42 | ffvelcdmd 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) ∈ (Base‘(𝑆 ↑s 𝐾))) | 
| 106 |  | evls1fpws.1 | . . . . . . . 8
⊢  · =
(.r‘𝑆) | 
| 107 | 19, 98, 99, 101, 104, 105, 106, 87 | pwsmulrval 17537 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘)))(.r‘(𝑆 ↑s 𝐾))(𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘))) ∘f · (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))) | 
| 108 | 19, 17, 98, 99, 101, 104 | pwselbas 17535 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘))):𝐾⟶𝐾) | 
| 109 | 108 | ffnd 6736 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘))) Fn 𝐾) | 
| 110 | 19, 17, 98, 99, 101, 105 | pwselbas 17535 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))):𝐾⟶𝐾) | 
| 111 | 110 | ffnd 6736 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))) Fn 𝐾) | 
| 112 |  | inidm 4226 | . . . . . . . 8
⊢ (𝐾 ∩ 𝐾) = 𝐾 | 
| 113 | 20 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → 𝑆 ∈ CRing) | 
| 114 | 1 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → 𝑅 ∈ (SubRing‘𝑆)) | 
| 115 | 17 | subrgss 20573 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾) | 
| 116 | 1, 115 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ⊆ 𝐾) | 
| 117 | 2, 17 | ressbas2 17284 | . . . . . . . . . . . . 13
⊢ (𝑅 ⊆ 𝐾 → 𝑅 = (Base‘𝑈)) | 
| 118 | 116, 117 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 = (Base‘𝑈)) | 
| 119 | 118 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑅 = (Base‘𝑈)) | 
| 120 | 26, 119 | eleqtrrd 2843 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ 𝑅) | 
| 121 | 120 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → (𝐴‘𝑘) ∈ 𝑅) | 
| 122 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → 𝑥 ∈ 𝐾) | 
| 123 | 16, 6, 2, 17, 82, 113, 114, 121, 122 | evls1scafv 22371 | . . . . . . . 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 22373 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → ((𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))‘𝑥) = (𝑘 ↑ 𝑥)) | 
| 127 | 109, 111,
101, 101, 112, 123, 126 | offval 7707 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘))) ∘f · (𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) | 
| 128 | 107, 127 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑄‘((algSc‘𝑊)‘(𝐴‘𝑘)))(.r‘(𝑆 ↑s 𝐾))(𝑄‘(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) | 
| 129 | 89, 97, 128 | 3eqtr3d 2784 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑄‘((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))) = (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) | 
| 130 | 129 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (𝑄‘((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈))))) = (𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))))) | 
| 131 | 130 | oveq2d 7448 | . . 3
⊢ (𝜑 → ((𝑆 ↑s 𝐾) Σg (𝑘 ∈ ℕ0
↦ (𝑄‘((𝐴‘𝑘)( ·𝑠
‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))))) = ((𝑆 ↑s 𝐾) Σg (𝑘 ∈ ℕ0
↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))))) | 
| 132 |  | eqid 2736 | . . . 4
⊢
(0g‘(𝑆 ↑s 𝐾)) = (0g‘(𝑆 ↑s 𝐾)) | 
| 133 | 100 | a1i 11 | . . . 4
⊢ (𝜑 → 𝐾 ∈ V) | 
| 134 |  | nn0ex 12534 | . . . . 5
⊢
ℕ0 ∈ V | 
| 135 | 134 | a1i 11 | . . . 4
⊢ (𝜑 → ℕ0 ∈
V) | 
| 136 | 20 | crngringd 20244 | . . . . 5
⊢ (𝜑 → 𝑆 ∈ Ring) | 
| 137 | 136 | ringcmnd 20282 | . . . 4
⊢ (𝜑 → 𝑆 ∈ CMnd) | 
| 138 | 136 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → 𝑆 ∈ Ring) | 
| 139 | 1 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ (SubRing‘𝑆)) | 
| 140 | 139, 115 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑅 ⊆ 𝐾) | 
| 141 | 140, 120 | sseldd 3983 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ 𝐾) | 
| 142 | 141 | adantr 480 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → (𝐴‘𝑘) ∈ 𝐾) | 
| 143 |  | eqid 2736 | . . . . . . . . . 10
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) | 
| 144 | 143, 17 | mgpbas 20143 | . . . . . . . . 9
⊢ 𝐾 =
(Base‘(mulGrp‘𝑆)) | 
| 145 | 143 | ringmgp 20237 | . . . . . . . . . . 11
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) | 
| 146 | 136, 145 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) | 
| 147 | 146 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → (mulGrp‘𝑆) ∈ Mnd) | 
| 148 | 144, 124,
147, 125, 122 | mulgnn0cld 19114 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → (𝑘 ↑ 𝑥) ∈ 𝐾) | 
| 149 | 17, 106, 138, 142, 148 | ringcld 20258 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑥 ∈ 𝐾) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) ∈ 𝐾) | 
| 150 | 149 | 3impa 1109 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝑥 ∈ 𝐾) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) ∈ 𝐾) | 
| 151 | 150 | 3com23 1126 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) ∈ 𝐾) | 
| 152 | 151 | 3expb 1120 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0)) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) ∈ 𝐾) | 
| 153 | 135 | mptexd 7245 | . . . . 5
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) ∈ V) | 
| 154 |  | funmpt 6603 | . . . . . 6
⊢ Fun
(𝑘 ∈
ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) | 
| 155 | 154 | a1i 11 | . . . . 5
⊢ (𝜑 → Fun (𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))))) | 
| 156 |  | fvexd 6920 | . . . . 5
⊢ (𝜑 →
(0g‘(𝑆
↑s 𝐾)) ∈ V) | 
| 157 | 12, 8, 6, 52 | coe1sfi 22216 | . . . . . . 7
⊢ (𝑀 ∈ 𝐵 → 𝐴 finSupp (0g‘𝑈)) | 
| 158 | 5, 157 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐴 finSupp (0g‘𝑈)) | 
| 159 | 158 | fsuppimpd 9410 | . . . . 5
⊢ (𝜑 → (𝐴 supp (0g‘𝑈)) ∈ Fin) | 
| 160 | 12, 8, 6, 24 | coe1f 22214 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ 𝐵 → 𝐴:ℕ0⟶(Base‘𝑈)) | 
| 161 | 5, 160 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴:ℕ0⟶(Base‘𝑈)) | 
| 162 | 161 | ffnd 6736 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 Fn ℕ0) | 
| 163 | 162 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → 𝐴 Fn ℕ0) | 
| 164 | 134 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → ℕ0
∈ V) | 
| 165 |  | fvexd 6920 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) →
(0g‘𝑈)
∈ V) | 
| 166 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) | 
| 167 | 163, 164,
165, 166 | fvdifsupp 8197 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝐴‘𝑘) = (0g‘𝑈)) | 
| 168 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(0g‘𝑆) = (0g‘𝑆) | 
| 169 | 2, 168 | subrg0 20580 | . . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ (SubRing‘𝑆) →
(0g‘𝑆) =
(0g‘𝑈)) | 
| 170 | 1, 169 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (0g‘𝑆) = (0g‘𝑈)) | 
| 171 | 170 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) →
(0g‘𝑆) =
(0g‘𝑈)) | 
| 172 | 167, 171 | eqtr4d 2779 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝐴‘𝑘) = (0g‘𝑆)) | 
| 173 | 172 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → (𝐴‘𝑘) = (0g‘𝑆)) | 
| 174 | 173 | oveq1d 7447 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) = ((0g‘𝑆) · (𝑘 ↑ 𝑥))) | 
| 175 | 136 | ad2antrr 726 | . . . . . . . . . . 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 3962 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → 𝑘 ∈ ℕ0) | 
| 179 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → 𝑥 ∈ 𝐾) | 
| 180 | 144, 124,
176, 178, 179 | mulgnn0cld 19114 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → (𝑘 ↑ 𝑥) ∈ 𝐾) | 
| 181 | 17, 106, 168 | ringlz 20291 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ Ring ∧ (𝑘 ↑ 𝑥) ∈ 𝐾) → ((0g‘𝑆) · (𝑘 ↑ 𝑥)) = (0g‘𝑆)) | 
| 182 | 175, 180,
181 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → ((0g‘𝑆) · (𝑘 ↑ 𝑥)) = (0g‘𝑆)) | 
| 183 | 174, 182 | eqtrd 2776 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) ∧ 𝑥 ∈ 𝐾) → ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)) = (0g‘𝑆)) | 
| 184 | 183 | mpteq2dva 5241 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))) = (𝑥 ∈ 𝐾 ↦ (0g‘𝑆))) | 
| 185 |  | fconstmpt 5746 | . . . . . . . 8
⊢ (𝐾 ×
{(0g‘𝑆)})
= (𝑥 ∈ 𝐾 ↦
(0g‘𝑆)) | 
| 186 | 184, 185 | eqtr4di 2794 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))) = (𝐾 × {(0g‘𝑆)})) | 
| 187 | 137 | cmnmndd 19823 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ Mnd) | 
| 188 | 19, 168 | pws0g 18787 | . . . . . . . . 9
⊢ ((𝑆 ∈ Mnd ∧ 𝐾 ∈ V) → (𝐾 ×
{(0g‘𝑆)})
= (0g‘(𝑆
↑s 𝐾))) | 
| 189 | 187, 133,
188 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐾 × {(0g‘𝑆)}) =
(0g‘(𝑆
↑s 𝐾))) | 
| 190 | 189 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝐾 × {(0g‘𝑆)}) =
(0g‘(𝑆
↑s 𝐾))) | 
| 191 | 186, 190 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℕ0 ∖ (𝐴 supp (0g‘𝑈)))) → (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))) = (0g‘(𝑆 ↑s 𝐾))) | 
| 192 | 191, 135 | suppss2 8226 | . . . . 5
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))) supp (0g‘(𝑆 ↑s 𝐾))) ⊆ (𝐴 supp (0g‘𝑈))) | 
| 193 |  | suppssfifsupp 9421 | . . . . 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 20001 | . . 3
⊢ (𝜑 → ((𝑆 ↑s 𝐾) Σg (𝑘 ∈ ℕ0
↦ (𝑥 ∈ 𝐾 ↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥))))) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))))) | 
| 196 | 78, 131, 195 | 3eqtrd 2780 | . 2
⊢ (𝜑 → (𝑄‘(𝑊 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘)(
·𝑠 ‘𝑊)(𝑘(.g‘(mulGrp‘𝑊))(var1‘𝑈)))))) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))))) | 
| 197 | 15, 196 | eqtrd 2776 | 1
⊢ (𝜑 → (𝑄‘𝑀) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σg (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑘 ↑ 𝑥)))))) |