| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑙 = 𝐴 → (𝑙‘𝑖) = (𝐴‘𝑖)) | 
| 2 | 1 | oveq2d 7448 | . . . . . . 7
⊢ (𝑙 = 𝐴 → ((𝑏‘𝑖) ↑ (𝑙‘𝑖)) = ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) | 
| 3 | 2 | mpteq2dv 5243 | . . . . . 6
⊢ (𝑙 = 𝐴 → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) | 
| 4 | 3 | oveq2d 7448 | . . . . 5
⊢ (𝑙 = 𝐴 → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))) = (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) | 
| 5 | 4 | oveq2d 7448 | . . . 4
⊢ (𝑙 = 𝐴 → ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) = ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) | 
| 6 | 5 | mpteq2dv 5243 | . . 3
⊢ (𝑙 = 𝐴 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) | 
| 7 | 6 | oveq2d 7448 | . 2
⊢ (𝑙 = 𝐴 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) | 
| 8 |  | evlsvvval.q | . . . 4
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) | 
| 9 |  | evlsvvval.p | . . . 4
⊢ 𝑃 = (𝐼 mPoly 𝑈) | 
| 10 |  | evlsvvval.b | . . . 4
⊢ 𝐵 = (Base‘𝑃) | 
| 11 |  | evlsvvval.d | . . . 4
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 12 |  | evlsvvval.k | . . . 4
⊢ 𝐾 = (Base‘𝑆) | 
| 13 |  | evlsvvval.u | . . . 4
⊢ 𝑈 = (𝑆 ↾s 𝑅) | 
| 14 |  | eqid 2736 | . . . 4
⊢ (𝑆 ↑s
(𝐾 ↑m 𝐼)) = (𝑆 ↑s (𝐾 ↑m 𝐼)) | 
| 15 |  | eqid 2736 | . . . 4
⊢
(mulGrp‘(𝑆
↑s (𝐾 ↑m 𝐼))) = (mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) | 
| 16 |  | eqid 2736 | . . . 4
⊢
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) =
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) | 
| 17 |  | eqid 2736 | . . . 4
⊢
(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼))) =
(.r‘(𝑆
↑s (𝐾 ↑m 𝐼))) | 
| 18 |  | eqid 2736 | . . . 4
⊢ (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥})) | 
| 19 |  | eqid 2736 | . . . 4
⊢ (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))) | 
| 20 |  | evlsvvval.i | . . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 21 |  | evlsvvval.s | . . . 4
⊢ (𝜑 → 𝑆 ∈ CRing) | 
| 22 |  | evlsvvval.r | . . . 4
⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) | 
| 23 |  | evlsvvval.f | . . . 4
⊢ (𝜑 → 𝐹 ∈ 𝐵) | 
| 24 | 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 | evlsvval 42575 | . . 3
⊢ (𝜑 → (𝑄‘𝐹) = ((𝑆 ↑s (𝐾 ↑m 𝐼)) Σg
(𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))((mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))))))))) | 
| 25 |  | sneq 4635 | . . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑏) → {𝑥} = {(𝐹‘𝑏)}) | 
| 26 | 25 | xpeq2d 5714 | . . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑏) → ((𝐾 ↑m 𝐼) × {𝑥}) = ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})) | 
| 27 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Base‘𝑈) =
(Base‘𝑈) | 
| 28 | 9, 27, 10, 11, 23 | mplelf 22019 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐷⟶(Base‘𝑈)) | 
| 29 | 13 | subrgbas 20582 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈)) | 
| 30 | 22, 29 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅 = (Base‘𝑈)) | 
| 31 | 30 | feq3d 6722 | . . . . . . . . . 10
⊢ (𝜑 → (𝐹:𝐷⟶𝑅 ↔ 𝐹:𝐷⟶(Base‘𝑈))) | 
| 32 | 28, 31 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐷⟶𝑅) | 
| 33 | 32 | ffvelcdmda 7103 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘𝑏) ∈ 𝑅) | 
| 34 |  | ovex 7465 | . . . . . . . . . 10
⊢ (𝐾 ↑m 𝐼) ∈ V | 
| 35 |  | snex 5435 | . . . . . . . . . 10
⊢ {(𝐹‘𝑏)} ∈ V | 
| 36 | 34, 35 | xpex 7774 | . . . . . . . . 9
⊢ ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) ∈ V | 
| 37 | 36 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) ∈ V) | 
| 38 | 18, 26, 33, 37 | fvmptd3 7038 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏)) = ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})) | 
| 39 | 11 | psrbagf 21939 | . . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝐷 → 𝑏:𝐼⟶ℕ0) | 
| 40 | 39 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏:𝐼⟶ℕ0) | 
| 41 | 40 | ffnd 6736 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 Fn 𝐼) | 
| 42 | 34 | mptex 7244 | . . . . . . . . . . . . 13
⊢ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)) ∈ V | 
| 43 | 42, 19 | fnmpti 6710 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))) Fn 𝐼 | 
| 44 | 43 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))) Fn 𝐼) | 
| 45 | 20 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ 𝑉) | 
| 46 |  | inidm 4226 | . . . . . . . . . . 11
⊢ (𝐼 ∩ 𝐼) = 𝐼 | 
| 47 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝑏‘𝑖) = (𝑏‘𝑖)) | 
| 48 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑖 → (𝑎‘𝑥) = (𝑎‘𝑖)) | 
| 49 | 48 | mpteq2dv 5243 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑖 → (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)) = (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))) | 
| 50 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼) | 
| 51 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(Base‘(𝑆
↑s (𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))) | 
| 52 | 21 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → 𝑆 ∈ CRing) | 
| 53 |  | ovexd 7467 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝐾 ↑m 𝐼) ∈ V) | 
| 54 |  | elmapi 8890 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (𝐾 ↑m 𝐼) → 𝑎:𝐼⟶𝐾) | 
| 55 | 54 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼) → (𝑎‘𝑖) ∈ 𝐾) | 
| 56 | 55 | ancoms 458 | . . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ 𝐼 ∧ 𝑎 ∈ (𝐾 ↑m 𝐼)) → (𝑎‘𝑖) ∈ 𝐾) | 
| 57 | 56 | adantll 714 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑m 𝐼)) → (𝑎‘𝑖) ∈ 𝐾) | 
| 58 | 57 | fmpttd 7134 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)):(𝐾 ↑m 𝐼)⟶𝐾) | 
| 59 | 14, 12, 51, 52, 53, 58 | pwselbasr 42558 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) | 
| 60 | 19, 49, 50, 59 | fvmptd3 7038 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))‘𝑖) = (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))) | 
| 61 | 41, 44, 45, 45, 46, 47, 60 | offval 7707 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))))) | 
| 62 | 15, 51 | mgpbas 20143 | . . . . . . . . . . . . . . 15
⊢
(Base‘(𝑆
↑s (𝐾 ↑m 𝐼))) = (Base‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) | 
| 63 | 21 | crngringd 20244 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑆 ∈ Ring) | 
| 64 |  | ovexd 7467 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐾 ↑m 𝐼) ∈ V) | 
| 65 | 14 | pwsring 20322 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ Ring ∧ (𝐾 ↑m 𝐼) ∈ V) → (𝑆 ↑s
(𝐾 ↑m 𝐼)) ∈ Ring) | 
| 66 | 63, 64, 65 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑆 ↑s (𝐾 ↑m 𝐼)) ∈ Ring) | 
| 67 | 15 | ringmgp 20237 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ↑s
(𝐾 ↑m 𝐼)) ∈ Ring →
(mulGrp‘(𝑆
↑s (𝐾 ↑m 𝐼))) ∈ Mnd) | 
| 68 | 66, 67 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) ∈ Mnd) | 
| 69 | 68 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) ∈ Mnd) | 
| 70 | 40 | ffvelcdmda 7103 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝑏‘𝑖) ∈
ℕ0) | 
| 71 | 62, 16, 69, 70, 59 | mulgnn0cld 19114 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) | 
| 72 | 14, 12, 51, 52, 53, 71 | pwselbas 17535 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))):(𝐾 ↑m 𝐼)⟶𝐾) | 
| 73 | 72 | ffnd 6736 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))) Fn (𝐾 ↑m 𝐼)) | 
| 74 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) ∈ V | 
| 75 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) | 
| 76 | 74, 75 | fnmpti 6710 | . . . . . . . . . . . . 13
⊢ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) Fn (𝐾 ↑m 𝐼) | 
| 77 | 76 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) Fn (𝐾 ↑m 𝐼)) | 
| 78 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)) = (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)) | 
| 79 |  | fveq1 6904 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑝 → (𝑎‘𝑖) = (𝑝‘𝑖)) | 
| 80 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → 𝑝 ∈ (𝐾 ↑m 𝐼)) | 
| 81 |  | fvexd 6920 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → (𝑝‘𝑖) ∈ V) | 
| 82 | 78, 79, 80, 81 | fvmptd3 7038 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → ((𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))‘𝑝) = (𝑝‘𝑖)) | 
| 83 | 82 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → ((𝑏‘𝑖) ↑ ((𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))‘𝑝)) = ((𝑏‘𝑖) ↑ (𝑝‘𝑖))) | 
| 84 |  | evlsvvval.m | . . . . . . . . . . . . . 14
⊢ 𝑀 = (mulGrp‘𝑆) | 
| 85 |  | evlsvvval.w | . . . . . . . . . . . . . 14
⊢  ↑ =
(.g‘𝑀) | 
| 86 | 63 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → 𝑆 ∈ Ring) | 
| 87 |  | ovexd 7467 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → (𝐾 ↑m 𝐼) ∈ V) | 
| 88 | 70 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → (𝑏‘𝑖) ∈
ℕ0) | 
| 89 | 59 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) | 
| 90 | 14, 51, 15, 84, 16, 85, 86, 87, 88, 89, 80 | pwsexpg 20327 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → (((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)))‘𝑝) = ((𝑏‘𝑖) ↑ ((𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))‘𝑝))) | 
| 91 |  | fveq1 6904 | . . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑝 → (𝑚‘𝑖) = (𝑝‘𝑖)) | 
| 92 | 91 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑝 → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) = ((𝑏‘𝑖) ↑ (𝑝‘𝑖))) | 
| 93 |  | ovexd 7467 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → ((𝑏‘𝑖) ↑ (𝑝‘𝑖)) ∈ V) | 
| 94 | 75, 92, 80, 93 | fvmptd3 7038 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → ((𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))‘𝑝) = ((𝑏‘𝑖) ↑ (𝑝‘𝑖))) | 
| 95 | 83, 90, 94 | 3eqtr4d 2786 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → (((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)))‘𝑝) = ((𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))‘𝑝)) | 
| 96 | 73, 77, 95 | eqfnfvd 7053 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) | 
| 97 | 96 | mpteq2dva 5241 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)))) = (𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) | 
| 98 | 61, 97 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))) = (𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) | 
| 99 | 98 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))))) = ((mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) Σg
(𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))) | 
| 100 |  | eqid 2736 | . . . . . . . . 9
⊢
(1r‘(𝑆 ↑s (𝐾 ↑m 𝐼))) =
(1r‘(𝑆
↑s (𝐾 ↑m 𝐼))) | 
| 101 |  | ovexd 7467 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐾 ↑m 𝐼) ∈ V) | 
| 102 | 21 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ CRing) | 
| 103 | 84, 12 | mgpbas 20143 | . . . . . . . . . 10
⊢ 𝐾 = (Base‘𝑀) | 
| 104 | 84 | ringmgp 20237 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring → 𝑀 ∈ Mnd) | 
| 105 | 63, 104 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ Mnd) | 
| 106 | 105 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼)) → 𝑀 ∈ Mnd) | 
| 107 | 70 | adantrl 716 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼)) → (𝑏‘𝑖) ∈
ℕ0) | 
| 108 |  | elmapi 8890 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ (𝐾 ↑m 𝐼) → 𝑚:𝐼⟶𝐾) | 
| 109 | 108 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ ((𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼) → (𝑚‘𝑖) ∈ 𝐾) | 
| 110 | 109 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼)) → (𝑚‘𝑖) ∈ 𝐾) | 
| 111 | 103, 85, 106, 107, 110 | mulgnn0cld 19114 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼)) → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) ∈ 𝐾) | 
| 112 | 45 | mptexd 7245 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) ∈ V) | 
| 113 |  | fvexd 6920 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (1r‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) ∈ V) | 
| 114 |  | funmpt 6603 | . . . . . . . . . . 11
⊢ Fun
(𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) | 
| 115 | 114 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → Fun (𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) | 
| 116 | 11 | psrbagfsupp 21940 | . . . . . . . . . . 11
⊢ (𝑏 ∈ 𝐷 → 𝑏 finSupp 0) | 
| 117 | 116 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 finSupp 0) | 
| 118 |  | ssidd 4006 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 supp 0) ⊆ (𝑏 supp 0)) | 
| 119 |  | 0cnd 11255 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 0 ∈ ℂ) | 
| 120 | 40, 118, 45, 119 | suppssr 8221 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → (𝑏‘𝑖) = 0) | 
| 121 | 120 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) = (0 ↑ (𝑚‘𝑖))) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) = (0 ↑ (𝑚‘𝑖))) | 
| 123 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (𝐼 ∖ (𝑏 supp 0)) → 𝑖 ∈ 𝐼) | 
| 124 | 123, 109 | sylan2 593 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → (𝑚‘𝑖) ∈ 𝐾) | 
| 125 | 124 | ancoms 458 | . . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (𝐼 ∖ (𝑏 supp 0)) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → (𝑚‘𝑖) ∈ 𝐾) | 
| 126 | 125 | adantll 714 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → (𝑚‘𝑖) ∈ 𝐾) | 
| 127 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(1r‘𝑆) = (1r‘𝑆) | 
| 128 | 84, 127 | ringidval 20181 | . . . . . . . . . . . . . . . 16
⊢
(1r‘𝑆) = (0g‘𝑀) | 
| 129 | 103, 128,
85 | mulg0 19093 | . . . . . . . . . . . . . . 15
⊢ ((𝑚‘𝑖) ∈ 𝐾 → (0 ↑ (𝑚‘𝑖)) = (1r‘𝑆)) | 
| 130 | 126, 129 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → (0 ↑ (𝑚‘𝑖)) = (1r‘𝑆)) | 
| 131 | 122, 130 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) = (1r‘𝑆)) | 
| 132 | 131 | mpteq2dva 5241 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (1r‘𝑆))) | 
| 133 |  | fconstmpt 5746 | . . . . . . . . . . . . 13
⊢ ((𝐾 ↑m 𝐼) ×
{(1r‘𝑆)})
= (𝑚 ∈ (𝐾 ↑m 𝐼) ↦
(1r‘𝑆)) | 
| 134 | 14, 127 | pws1 20323 | . . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Ring ∧ (𝐾 ↑m 𝐼) ∈ V) → ((𝐾 ↑m 𝐼) ×
{(1r‘𝑆)})
= (1r‘(𝑆
↑s (𝐾 ↑m 𝐼)))) | 
| 135 | 63, 64, 134 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐾 ↑m 𝐼) × {(1r‘𝑆)}) =
(1r‘(𝑆
↑s (𝐾 ↑m 𝐼)))) | 
| 136 | 135 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → ((𝐾 ↑m 𝐼) × {(1r‘𝑆)}) =
(1r‘(𝑆
↑s (𝐾 ↑m 𝐼)))) | 
| 137 | 133, 136 | eqtr3id 2790 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (1r‘𝑆)) = (1r‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) | 
| 138 | 132, 137 | eqtrd 2776 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) = (1r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) | 
| 139 | 138, 45 | suppss2 8226 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) supp (1r‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) ⊆ (𝑏 supp 0)) | 
| 140 | 112, 113,
115, 117, 139 | fsuppsssuppgd 9423 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) finSupp (1r‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) | 
| 141 | 14, 12, 100, 15, 84, 101, 45, 102, 111, 140 | pwsgprod 42559 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) Σg
(𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))) | 
| 142 | 99, 141 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))) | 
| 143 | 38, 142 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))((mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))))) = (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))(𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))))) | 
| 144 | 12 | subrgss 20573 | . . . . . . . . . . . . 13
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾) | 
| 145 | 29, 144 | eqsstrrd 4018 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ (SubRing‘𝑆) → (Base‘𝑈) ⊆ 𝐾) | 
| 146 | 22, 145 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝑈) ⊆ 𝐾) | 
| 147 | 28, 146 | fssd 6752 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐷⟶𝐾) | 
| 148 | 147 | ffvelcdmda 7103 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘𝑏) ∈ 𝐾) | 
| 149 |  | fconst6g 6796 | . . . . . . . . 9
⊢ ((𝐹‘𝑏) ∈ 𝐾 → ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}):(𝐾 ↑m 𝐼)⟶𝐾) | 
| 150 | 148, 149 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}):(𝐾 ↑m 𝐼)⟶𝐾) | 
| 151 | 14, 12, 51, 102, 101, 150 | pwselbasr 42558 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) | 
| 152 | 20 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → 𝐼 ∈ 𝑉) | 
| 153 | 21 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → 𝑆 ∈ CRing) | 
| 154 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → 𝑚 ∈ (𝐾 ↑m 𝐼)) | 
| 155 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → 𝑏 ∈ 𝐷) | 
| 156 | 11, 12, 84, 85, 152, 153, 154, 155 | evlsvvvallem 42576 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) ∈ 𝐾) | 
| 157 | 156 | fmpttd 7134 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))):(𝐾 ↑m 𝐼)⟶𝐾) | 
| 158 | 14, 12, 51, 102, 101, 157 | pwselbasr 42558 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) | 
| 159 |  | evlsvvval.x | . . . . . . 7
⊢  · =
(.r‘𝑆) | 
| 160 | 14, 51, 102, 101, 151, 158, 159, 17 | pwsmulrval 17537 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))(𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))) = (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) ∘f · (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))))) | 
| 161 | 150 | ffnd 6736 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) Fn (𝐾 ↑m 𝐼)) | 
| 162 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑀 Σg
(𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) ∈ V | 
| 163 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) | 
| 164 | 162, 163 | fnmpti 6710 | . . . . . . . 8
⊢ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) Fn (𝐾 ↑m 𝐼) | 
| 165 | 164 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) Fn (𝐾 ↑m 𝐼)) | 
| 166 |  | inidm 4226 | . . . . . . 7
⊢ ((𝐾 ↑m 𝐼) ∩ (𝐾 ↑m 𝐼)) = (𝐾 ↑m 𝐼) | 
| 167 |  | fvex 6918 | . . . . . . . . 9
⊢ (𝐹‘𝑏) ∈ V | 
| 168 | 167 | fvconst2 7225 | . . . . . . . 8
⊢ (𝑙 ∈ (𝐾 ↑m 𝐼) → (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})‘𝑙) = (𝐹‘𝑏)) | 
| 169 | 168 | adantl 481 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})‘𝑙) = (𝐹‘𝑏)) | 
| 170 |  | fveq1 6904 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑙 → (𝑚‘𝑖) = (𝑙‘𝑖)) | 
| 171 | 170 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑚 = 𝑙 → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) = ((𝑏‘𝑖) ↑ (𝑙‘𝑖))) | 
| 172 | 171 | mpteq2dv 5243 | . . . . . . . . 9
⊢ (𝑚 = 𝑙 → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))) | 
| 173 | 172 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑚 = 𝑙 → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) = (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) | 
| 174 |  | simpr 484 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → 𝑙 ∈ (𝐾 ↑m 𝐼)) | 
| 175 | 20 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → 𝐼 ∈ 𝑉) | 
| 176 | 21 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → 𝑆 ∈ CRing) | 
| 177 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → 𝑏 ∈ 𝐷) | 
| 178 | 11, 12, 84, 85, 175, 176, 174, 177 | evlsvvvallem 42576 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))) ∈ 𝐾) | 
| 179 | 163, 173,
174, 178 | fvmptd3 7038 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → ((𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))‘𝑙) = (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) | 
| 180 | 161, 165,
101, 101, 166, 169, 179 | offval 7707 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) ∘f · (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))) = (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) | 
| 181 | 143, 160,
180 | 3eqtrd 2780 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))((mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))))) = (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) | 
| 182 | 181 | mpteq2dva 5241 | . . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))((mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))))))) = (𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))))) | 
| 183 | 182 | oveq2d 7448 | . . 3
⊢ (𝜑 → ((𝑆 ↑s (𝐾 ↑m 𝐼)) Σg
(𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))((mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))))))) = ((𝑆 ↑s (𝐾 ↑m 𝐼)) Σg
(𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))))) | 
| 184 |  | eqid 2736 | . . . 4
⊢
(0g‘(𝑆 ↑s (𝐾 ↑m 𝐼))) =
(0g‘(𝑆
↑s (𝐾 ↑m 𝐼))) | 
| 185 |  | ovexd 7467 | . . . . 5
⊢ (𝜑 → (ℕ0
↑m 𝐼)
∈ V) | 
| 186 | 11, 185 | rabexd 5339 | . . . 4
⊢ (𝜑 → 𝐷 ∈ V) | 
| 187 | 63 | ringcmnd 20282 | . . . 4
⊢ (𝜑 → 𝑆 ∈ CMnd) | 
| 188 | 63 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → 𝑆 ∈ Ring) | 
| 189 | 148 | adantrl 716 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → (𝐹‘𝑏) ∈ 𝐾) | 
| 190 |  | simpl 482 | . . . . . 6
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → 𝜑) | 
| 191 |  | simprr 772 | . . . . . 6
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → 𝑏 ∈ 𝐷) | 
| 192 |  | simprl 770 | . . . . . 6
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → 𝑙 ∈ (𝐾 ↑m 𝐼)) | 
| 193 | 190, 191,
192, 178 | syl21anc 837 | . . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))) ∈ 𝐾) | 
| 194 | 12, 159, 188, 189, 193 | ringcld 20258 | . . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) ∈ 𝐾) | 
| 195 | 186 | mptexd 7245 | . . . . 5
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) ∈ V) | 
| 196 |  | fvexd 6920 | . . . . 5
⊢ (𝜑 →
(0g‘(𝑆
↑s (𝐾 ↑m 𝐼))) ∈ V) | 
| 197 |  | funmpt 6603 | . . . . . 6
⊢ Fun
(𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) | 
| 198 | 197 | a1i 11 | . . . . 5
⊢ (𝜑 → Fun (𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))))) | 
| 199 |  | eqid 2736 | . . . . . 6
⊢
(0g‘𝑈) = (0g‘𝑈) | 
| 200 | 9, 10, 199, 23 | mplelsfi 22016 | . . . . 5
⊢ (𝜑 → 𝐹 finSupp (0g‘𝑈)) | 
| 201 |  | ssidd 4006 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 supp (0g‘𝑈)) ⊆ (𝐹 supp (0g‘𝑈))) | 
| 202 |  | fvexd 6920 | . . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝑈) ∈ V) | 
| 203 | 147, 201,
186, 202 | suppssr 8221 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (𝐹‘𝑏) = (0g‘𝑈)) | 
| 204 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(0g‘𝑆) = (0g‘𝑆) | 
| 205 | 13, 204 | subrg0 20580 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ (SubRing‘𝑆) →
(0g‘𝑆) =
(0g‘𝑈)) | 
| 206 | 22, 205 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝑆) = (0g‘𝑈)) | 
| 207 | 206 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (0g‘𝑆) = (0g‘𝑈)) | 
| 208 | 203, 207 | eqtr4d 2779 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (𝐹‘𝑏) = (0g‘𝑆)) | 
| 209 | 208 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → (𝐹‘𝑏) = (0g‘𝑆)) | 
| 210 | 209 | oveq1d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) = ((0g‘𝑆) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))) | 
| 211 | 63 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → 𝑆 ∈ Ring) | 
| 212 |  | eldifi 4130 | . . . . . . . . . . 11
⊢ (𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈))) → 𝑏 ∈ 𝐷) | 
| 213 | 212, 178 | sylanl2 681 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))) ∈ 𝐾) | 
| 214 | 12, 159, 204, 211, 213 | ringlzd 20293 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → ((0g‘𝑆) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) = (0g‘𝑆)) | 
| 215 | 210, 214 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) = (0g‘𝑆)) | 
| 216 | 215 | mpteq2dva 5241 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))) = (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ (0g‘𝑆))) | 
| 217 |  | fconstmpt 5746 | . . . . . . . . 9
⊢ ((𝐾 ↑m 𝐼) ×
{(0g‘𝑆)})
= (𝑙 ∈ (𝐾 ↑m 𝐼) ↦
(0g‘𝑆)) | 
| 218 | 187 | cmnmndd 19823 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ Mnd) | 
| 219 | 14, 204 | pws0g 18787 | . . . . . . . . . 10
⊢ ((𝑆 ∈ Mnd ∧ (𝐾 ↑m 𝐼) ∈ V) → ((𝐾 ↑m 𝐼) ×
{(0g‘𝑆)})
= (0g‘(𝑆
↑s (𝐾 ↑m 𝐼)))) | 
| 220 | 218, 64, 219 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → ((𝐾 ↑m 𝐼) × {(0g‘𝑆)}) =
(0g‘(𝑆
↑s (𝐾 ↑m 𝐼)))) | 
| 221 | 217, 220 | eqtr3id 2790 | . . . . . . . 8
⊢ (𝜑 → (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ (0g‘𝑆)) = (0g‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) | 
| 222 | 221 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ (0g‘𝑆)) = (0g‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) | 
| 223 | 216, 222 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))) = (0g‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) | 
| 224 | 223, 186 | suppss2 8226 | . . . . 5
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) supp (0g‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) ⊆ (𝐹 supp (0g‘𝑈))) | 
| 225 | 195, 196,
198, 200, 224 | fsuppsssuppgd 9423 | . . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) finSupp (0g‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) | 
| 226 | 14, 12, 184, 64, 186, 187, 194, 225 | pwsgsum 20001 | . . 3
⊢ (𝜑 → ((𝑆 ↑s (𝐾 ↑m 𝐼)) Σg
(𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))))) = (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))))) | 
| 227 | 24, 183, 226 | 3eqtrd 2780 | . 2
⊢ (𝜑 → (𝑄‘𝐹) = (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))))) | 
| 228 |  | evlsvvval.a | . 2
⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) | 
| 229 |  | ovexd 7467 | . 2
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) ∈ V) | 
| 230 | 7, 227, 228, 229 | fvmptd4 7039 | 1
⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) |