Step | Hyp | Ref
| Expression |
1 | | fveq1 6880 |
. . . . . . . 8
⊢ (𝑙 = 𝐴 → (𝑙‘𝑖) = (𝐴‘𝑖)) |
2 | 1 | oveq2d 7417 |
. . . . . . 7
⊢ (𝑙 = 𝐴 → ((𝑏‘𝑖) ↑ (𝑙‘𝑖)) = ((𝑏‘𝑖) ↑ (𝐴‘𝑖))) |
3 | 2 | mpteq2dv 5240 |
. . . . . 6
⊢ (𝑙 = 𝐴 → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))) |
4 | 3 | oveq2d 7417 |
. . . . 5
⊢ (𝑙 = 𝐴 → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))) = (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))) |
5 | 4 | oveq2d 7417 |
. . . 4
⊢ (𝑙 = 𝐴 → ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) = ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))) |
6 | 5 | mpteq2dv 5240 |
. . 3
⊢ (𝑙 = 𝐴 → (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))) = (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) |
7 | 6 | oveq2d 7417 |
. 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 2724 |
. . . 4
⊢ (𝑆 ↑s
(𝐾 ↑m 𝐼)) = (𝑆 ↑s (𝐾 ↑m 𝐼)) |
15 | | eqid 2724 |
. . . 4
⊢
(mulGrp‘(𝑆
↑s (𝐾 ↑m 𝐼))) = (mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) |
16 | | eqid 2724 |
. . . 4
⊢
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) =
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
17 | | eqid 2724 |
. . . 4
⊢
(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼))) =
(.r‘(𝑆
↑s (𝐾 ↑m 𝐼))) |
18 | | eqid 2724 |
. . . 4
⊢ (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥})) |
19 | | eqid 2724 |
. . . 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 41621 |
. . 3
⊢ (𝜑 → (𝑄‘𝐹) = ((𝑆 ↑s (𝐾 ↑m 𝐼)) Σg
(𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))((mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))))))))) |
25 | | sneq 4630 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑏) → {𝑥} = {(𝐹‘𝑏)}) |
26 | 25 | xpeq2d 5696 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑏) → ((𝐾 ↑m 𝐼) × {𝑥}) = ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})) |
27 | | eqid 2724 |
. . . . . . . . . . 11
⊢
(Base‘𝑈) =
(Base‘𝑈) |
28 | 9, 27, 10, 11, 23 | mplelf 21867 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐷⟶(Base‘𝑈)) |
29 | 13 | subrgbas 20473 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈)) |
30 | 22, 29 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 = (Base‘𝑈)) |
31 | 30 | feq3d 6694 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹:𝐷⟶𝑅 ↔ 𝐹:𝐷⟶(Base‘𝑈))) |
32 | 28, 31 | mpbird 257 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐷⟶𝑅) |
33 | 32 | ffvelcdmda 7076 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘𝑏) ∈ 𝑅) |
34 | | ovex 7434 |
. . . . . . . . . 10
⊢ (𝐾 ↑m 𝐼) ∈ V |
35 | | snex 5421 |
. . . . . . . . . 10
⊢ {(𝐹‘𝑏)} ∈ V |
36 | 34, 35 | xpex 7733 |
. . . . . . . . 9
⊢ ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) ∈ V |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) ∈ V) |
38 | 18, 26, 33, 37 | fvmptd3 7011 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏)) = ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})) |
39 | 11 | psrbagf 21780 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝐷 → 𝑏:𝐼⟶ℕ0) |
40 | 39 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏:𝐼⟶ℕ0) |
41 | 40 | ffnd 6708 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 Fn 𝐼) |
42 | 34 | mptex 7216 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)) ∈ V |
43 | 42, 19 | fnmpti 6683 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))) Fn 𝐼 |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))) Fn 𝐼) |
45 | 20 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝐼 ∈ 𝑉) |
46 | | inidm 4210 |
. . . . . . . . . . 11
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
47 | | eqidd 2725 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝑏‘𝑖) = (𝑏‘𝑖)) |
48 | | fveq2 6881 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑖 → (𝑎‘𝑥) = (𝑎‘𝑖)) |
49 | 48 | mpteq2dv 5240 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑖 → (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)) = (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))) |
50 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼) |
51 | | eqid 2724 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝑆
↑s (𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))) |
52 | 21 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → 𝑆 ∈ CRing) |
53 | | ovexd 7436 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝐾 ↑m 𝐼) ∈ V) |
54 | | elmapi 8839 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (𝐾 ↑m 𝐼) → 𝑎:𝐼⟶𝐾) |
55 | 54 | ffvelcdmda 7076 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼) → (𝑎‘𝑖) ∈ 𝐾) |
56 | 55 | ancoms 458 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ 𝐼 ∧ 𝑎 ∈ (𝐾 ↑m 𝐼)) → (𝑎‘𝑖) ∈ 𝐾) |
57 | 56 | adantll 711 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑎 ∈ (𝐾 ↑m 𝐼)) → (𝑎‘𝑖) ∈ 𝐾) |
58 | 57 | fmpttd 7106 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)):(𝐾 ↑m 𝐼)⟶𝐾) |
59 | 14, 12, 51, 52, 53, 58 | pwselbasr 41602 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
60 | 19, 49, 50, 59 | fvmptd3 7011 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))‘𝑖) = (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))) |
61 | 41, 44, 45, 45, 46, 47, 60 | offval 7672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))))) |
62 | 15, 51 | mgpbas 20035 |
. . . . . . . . . . . . . . 15
⊢
(Base‘(𝑆
↑s (𝐾 ↑m 𝐼))) = (Base‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) |
63 | 21 | crngringd 20141 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑆 ∈ Ring) |
64 | | ovexd 7436 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐾 ↑m 𝐼) ∈ V) |
65 | 14 | pwsring 20213 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ Ring ∧ (𝐾 ↑m 𝐼) ∈ V) → (𝑆 ↑s
(𝐾 ↑m 𝐼)) ∈ Ring) |
66 | 63, 64, 65 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑆 ↑s (𝐾 ↑m 𝐼)) ∈ Ring) |
67 | 15 | ringmgp 20134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ↑s
(𝐾 ↑m 𝐼)) ∈ Ring →
(mulGrp‘(𝑆
↑s (𝐾 ↑m 𝐼))) ∈ Mnd) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) ∈ Mnd) |
69 | 68 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) ∈ Mnd) |
70 | 40 | ffvelcdmda 7076 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝑏‘𝑖) ∈
ℕ0) |
71 | 62, 16, 69, 70, 59 | mulgnn0cld 19012 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
72 | 14, 12, 51, 52, 53, 71 | pwselbas 17434 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))):(𝐾 ↑m 𝐼)⟶𝐾) |
73 | 72 | ffnd 6708 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))) Fn (𝐾 ↑m 𝐼)) |
74 | | ovex 7434 |
. . . . . . . . . . . . . 14
⊢ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) ∈ V |
75 | | eqid 2724 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) |
76 | 74, 75 | fnmpti 6683 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) Fn (𝐾 ↑m 𝐼) |
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) Fn (𝐾 ↑m 𝐼)) |
78 | | eqid 2724 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)) = (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)) |
79 | | fveq1 6880 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑝 → (𝑎‘𝑖) = (𝑝‘𝑖)) |
80 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → 𝑝 ∈ (𝐾 ↑m 𝐼)) |
81 | | fvexd 6896 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → (𝑝‘𝑖) ∈ V) |
82 | 78, 79, 80, 81 | fvmptd3 7011 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → ((𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))‘𝑝) = (𝑝‘𝑖)) |
83 | 82 | oveq2d 7417 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → ((𝑏‘𝑖) ↑ ((𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))‘𝑝)) = ((𝑏‘𝑖) ↑ (𝑝‘𝑖))) |
84 | | evlsvvval.m |
. . . . . . . . . . . . . 14
⊢ 𝑀 = (mulGrp‘𝑆) |
85 | | evlsvvval.w |
. . . . . . . . . . . . . 14
⊢ ↑ =
(.g‘𝑀) |
86 | 63 | ad3antrrr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → 𝑆 ∈ Ring) |
87 | | ovexd 7436 |
. . . . . . . . . . . . . 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 20218 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → (((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)))‘𝑝) = ((𝑏‘𝑖) ↑ ((𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))‘𝑝))) |
91 | | fveq1 6880 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑝 → (𝑚‘𝑖) = (𝑝‘𝑖)) |
92 | 91 | oveq2d 7417 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑝 → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) = ((𝑏‘𝑖) ↑ (𝑝‘𝑖))) |
93 | | ovexd 7436 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → ((𝑏‘𝑖) ↑ (𝑝‘𝑖)) ∈ V) |
94 | 75, 92, 80, 93 | fvmptd3 7011 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → ((𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))‘𝑝) = ((𝑏‘𝑖) ↑ (𝑝‘𝑖))) |
95 | 83, 90, 94 | 3eqtr4d 2774 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) ∧ 𝑝 ∈ (𝐾 ↑m 𝐼)) → (((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)))‘𝑝) = ((𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))‘𝑝)) |
96 | 73, 77, 95 | eqfnfvd 7025 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ 𝐼) → ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) |
97 | 96 | mpteq2dva 5238 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖)(.g‘(mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))))(𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑖)))) = (𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) |
98 | 61, 97 | eqtrd 2764 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))) = (𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) |
99 | 98 | oveq2d 7417 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))))) = ((mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) Σg
(𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))) |
100 | | eqid 2724 |
. . . . . . . . 9
⊢
(1r‘(𝑆 ↑s (𝐾 ↑m 𝐼))) =
(1r‘(𝑆
↑s (𝐾 ↑m 𝐼))) |
101 | | ovexd 7436 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐾 ↑m 𝐼) ∈ V) |
102 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑆 ∈ CRing) |
103 | 84, 12 | mgpbas 20035 |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝑀) |
104 | 84 | ringmgp 20134 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ Ring → 𝑀 ∈ Mnd) |
105 | 63, 104 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ Mnd) |
106 | 105 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼)) → 𝑀 ∈ Mnd) |
107 | 70 | adantrl 713 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼)) → (𝑏‘𝑖) ∈
ℕ0) |
108 | | elmapi 8839 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (𝐾 ↑m 𝐼) → 𝑚:𝐼⟶𝐾) |
109 | 108 | ffvelcdmda 7076 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼) → (𝑚‘𝑖) ∈ 𝐾) |
110 | 109 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼)) → (𝑚‘𝑖) ∈ 𝐾) |
111 | 103, 85, 106, 107, 110 | mulgnn0cld 19012 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ (𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ 𝐼)) → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) ∈ 𝐾) |
112 | 45 | mptexd 7217 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) ∈ V) |
113 | | fvexd 6896 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (1r‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) ∈ V) |
114 | | funmpt 6576 |
. . . . . . . . . . 11
⊢ Fun
(𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) |
115 | 114 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → Fun (𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) |
116 | 11 | psrbagfsupp 21782 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝐷 → 𝑏 finSupp 0) |
117 | 116 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 finSupp 0) |
118 | | ssidd 3997 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑏 supp 0) ⊆ (𝑏 supp 0)) |
119 | | 0cnd 11204 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 0 ∈ ℂ) |
120 | 40, 118, 45, 119 | suppssr 8175 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → (𝑏‘𝑖) = 0) |
121 | 120 | oveq1d 7416 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) = (0 ↑ (𝑚‘𝑖))) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) = (0 ↑ (𝑚‘𝑖))) |
123 | | eldifi 4118 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (𝐼 ∖ (𝑏 supp 0)) → 𝑖 ∈ 𝐼) |
124 | 123, 109 | sylan2 592 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ (𝐾 ↑m 𝐼) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → (𝑚‘𝑖) ∈ 𝐾) |
125 | 124 | ancoms 458 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (𝐼 ∖ (𝑏 supp 0)) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → (𝑚‘𝑖) ∈ 𝐾) |
126 | 125 | adantll 711 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → (𝑚‘𝑖) ∈ 𝐾) |
127 | | eqid 2724 |
. . . . . . . . . . . . . . . . 17
⊢
(1r‘𝑆) = (1r‘𝑆) |
128 | 84, 127 | ringidval 20078 |
. . . . . . . . . . . . . . . 16
⊢
(1r‘𝑆) = (0g‘𝑀) |
129 | 103, 128,
85 | mulg0 18992 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚‘𝑖) ∈ 𝐾 → (0 ↑ (𝑚‘𝑖)) = (1r‘𝑆)) |
130 | 126, 129 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → (0 ↑ (𝑚‘𝑖)) = (1r‘𝑆)) |
131 | 122, 130 | eqtrd 2764 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) = (1r‘𝑆)) |
132 | 131 | mpteq2dva 5238 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (1r‘𝑆))) |
133 | | fconstmpt 5728 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ↑m 𝐼) ×
{(1r‘𝑆)})
= (𝑚 ∈ (𝐾 ↑m 𝐼) ↦
(1r‘𝑆)) |
134 | 14, 127 | pws1 20214 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Ring ∧ (𝐾 ↑m 𝐼) ∈ V) → ((𝐾 ↑m 𝐼) ×
{(1r‘𝑆)})
= (1r‘(𝑆
↑s (𝐾 ↑m 𝐼)))) |
135 | 63, 64, 134 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐾 ↑m 𝐼) × {(1r‘𝑆)}) =
(1r‘(𝑆
↑s (𝐾 ↑m 𝐼)))) |
136 | 135 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → ((𝐾 ↑m 𝐼) × {(1r‘𝑆)}) =
(1r‘(𝑆
↑s (𝐾 ↑m 𝐼)))) |
137 | 133, 136 | eqtr3id 2778 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (1r‘𝑆)) = (1r‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) |
138 | 132, 137 | eqtrd 2764 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑖 ∈ (𝐼 ∖ (𝑏 supp 0))) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) = (1r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
139 | 138, 45 | suppss2 8180 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) supp (1r‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) ⊆ (𝑏 supp 0)) |
140 | 112, 113,
115, 117, 139 | fsuppsssuppgd 41557 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) finSupp (1r‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) |
141 | 14, 12, 100, 15, 84, 101, 45, 102, 111, 140 | pwsgprod 41603 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) Σg
(𝑖 ∈ 𝐼 ↦ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))) |
142 | 99, 141 | eqtrd 2764 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))) |
143 | 38, 142 | oveq12d 7419 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))((mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))))) = (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))(𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))))) |
144 | 12 | subrgss 20464 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾) |
145 | 29, 144 | eqsstrrd 4013 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ (SubRing‘𝑆) → (Base‘𝑈) ⊆ 𝐾) |
146 | 22, 145 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝑈) ⊆ 𝐾) |
147 | 28, 146 | fssd 6725 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐷⟶𝐾) |
148 | 147 | ffvelcdmda 7076 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝐹‘𝑏) ∈ 𝐾) |
149 | | fconst6g 6770 |
. . . . . . . . 9
⊢ ((𝐹‘𝑏) ∈ 𝐾 → ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}):(𝐾 ↑m 𝐼)⟶𝐾) |
150 | 148, 149 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}):(𝐾 ↑m 𝐼)⟶𝐾) |
151 | 14, 12, 51, 102, 101, 150 | pwselbasr 41602 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
152 | 20 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → 𝐼 ∈ 𝑉) |
153 | 21 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → 𝑆 ∈ CRing) |
154 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → 𝑚 ∈ (𝐾 ↑m 𝐼)) |
155 | | simplr 766 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → 𝑏 ∈ 𝐷) |
156 | 11, 12, 84, 85, 152, 153, 154, 155 | evlsvvvallem 41622 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑚 ∈ (𝐾 ↑m 𝐼)) → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) ∈ 𝐾) |
157 | 156 | fmpttd 7106 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))):(𝐾 ↑m 𝐼)⟶𝐾) |
158 | 14, 12, 51, 102, 101, 157 | pwselbasr 41602 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
159 | | evlsvvval.x |
. . . . . . 7
⊢ · =
(.r‘𝑆) |
160 | 14, 51, 102, 101, 151, 158, 159, 17 | pwsmulrval 17436 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))(𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))) = (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) ∘f · (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))))) |
161 | 150 | ffnd 6708 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → ((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) Fn (𝐾 ↑m 𝐼)) |
162 | | ovex 7434 |
. . . . . . . . 9
⊢ (𝑀 Σg
(𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) ∈ V |
163 | | eqid 2724 |
. . . . . . . . 9
⊢ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) = (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) |
164 | 162, 163 | fnmpti 6683 |
. . . . . . . 8
⊢ (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) Fn (𝐾 ↑m 𝐼) |
165 | 164 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))))) Fn (𝐾 ↑m 𝐼)) |
166 | | inidm 4210 |
. . . . . . 7
⊢ ((𝐾 ↑m 𝐼) ∩ (𝐾 ↑m 𝐼)) = (𝐾 ↑m 𝐼) |
167 | | fvex 6894 |
. . . . . . . . 9
⊢ (𝐹‘𝑏) ∈ V |
168 | 167 | fvconst2 7197 |
. . . . . . . 8
⊢ (𝑙 ∈ (𝐾 ↑m 𝐼) → (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})‘𝑙) = (𝐹‘𝑏)) |
169 | 168 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)})‘𝑙) = (𝐹‘𝑏)) |
170 | | fveq1 6880 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑙 → (𝑚‘𝑖) = (𝑙‘𝑖)) |
171 | 170 | oveq2d 7417 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑙 → ((𝑏‘𝑖) ↑ (𝑚‘𝑖)) = ((𝑏‘𝑖) ↑ (𝑙‘𝑖))) |
172 | 171 | mpteq2dv 5240 |
. . . . . . . . 9
⊢ (𝑚 = 𝑙 → (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖))) = (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))) |
173 | 172 | oveq2d 7417 |
. . . . . . . 8
⊢ (𝑚 = 𝑙 → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))) = (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) |
174 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → 𝑙 ∈ (𝐾 ↑m 𝐼)) |
175 | 20 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → 𝐼 ∈ 𝑉) |
176 | 21 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → 𝑆 ∈ CRing) |
177 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → 𝑏 ∈ 𝐷) |
178 | 11, 12, 84, 85, 175, 176, 174, 177 | evlsvvvallem 41622 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))) ∈ 𝐾) |
179 | 163, 173,
174, 178 | fvmptd3 7011 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐷) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → ((𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))‘𝑙) = (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) |
180 | 161, 165,
101, 101, 166, 169, 179 | offval 7672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (((𝐾 ↑m 𝐼) × {(𝐹‘𝑏)}) ∘f · (𝑚 ∈ (𝐾 ↑m 𝐼) ↦ (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑚‘𝑖)))))) = (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) |
181 | 143, 160,
180 | 3eqtrd 2768 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))((mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥)))))) = (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) |
182 | 181 | mpteq2dva 5238 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (((𝑥 ∈ 𝑅 ↦ ((𝐾 ↑m 𝐼) × {𝑥}))‘(𝐹‘𝑏))(.r‘(𝑆 ↑s (𝐾 ↑m 𝐼)))((mulGrp‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) Σg
(𝑏 ∘f
(.g‘(mulGrp‘(𝑆 ↑s (𝐾 ↑m 𝐼))))(𝑥 ∈ 𝐼 ↦ (𝑎 ∈ (𝐾 ↑m 𝐼) ↦ (𝑎‘𝑥))))))) = (𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))))) |
183 | 182 | oveq2d 7417 |
. . 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 2724 |
. . . 4
⊢
(0g‘(𝑆 ↑s (𝐾 ↑m 𝐼))) =
(0g‘(𝑆
↑s (𝐾 ↑m 𝐼))) |
185 | | ovexd 7436 |
. . . . 5
⊢ (𝜑 → (ℕ0
↑m 𝐼)
∈ V) |
186 | 11, 185 | rabexd 5323 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ V) |
187 | 63 | ringcmnd 20173 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ CMnd) |
188 | 63 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → 𝑆 ∈ Ring) |
189 | 148 | adantrl 713 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → (𝐹‘𝑏) ∈ 𝐾) |
190 | | simpl 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → 𝜑) |
191 | | simprr 770 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → 𝑏 ∈ 𝐷) |
192 | | simprl 768 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → 𝑙 ∈ (𝐾 ↑m 𝐼)) |
193 | 190, 191,
192, 178 | syl21anc 835 |
. . . . 5
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))) ∈ 𝐾) |
194 | 12, 159, 188, 189, 193 | ringcld 20152 |
. . . 4
⊢ ((𝜑 ∧ (𝑙 ∈ (𝐾 ↑m 𝐼) ∧ 𝑏 ∈ 𝐷)) → ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) ∈ 𝐾) |
195 | 186 | mptexd 7217 |
. . . . 5
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) ∈ V) |
196 | | fvexd 6896 |
. . . . 5
⊢ (𝜑 →
(0g‘(𝑆
↑s (𝐾 ↑m 𝐼))) ∈ V) |
197 | | funmpt 6576 |
. . . . . 6
⊢ Fun
(𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) |
198 | 197 | a1i 11 |
. . . . 5
⊢ (𝜑 → Fun (𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))))) |
199 | | eqid 2724 |
. . . . . 6
⊢
(0g‘𝑈) = (0g‘𝑈) |
200 | 13 | ovexi 7435 |
. . . . . . 7
⊢ 𝑈 ∈ V |
201 | 200 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ V) |
202 | 9, 10, 199, 23, 201 | mplelsfi 21864 |
. . . . 5
⊢ (𝜑 → 𝐹 finSupp (0g‘𝑈)) |
203 | | ssidd 3997 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 supp (0g‘𝑈)) ⊆ (𝐹 supp (0g‘𝑈))) |
204 | | fvexd 6896 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝑈) ∈ V) |
205 | 147, 203,
186, 204 | suppssr 8175 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (𝐹‘𝑏) = (0g‘𝑈)) |
206 | | eqid 2724 |
. . . . . . . . . . . . . . 15
⊢
(0g‘𝑆) = (0g‘𝑆) |
207 | 13, 206 | subrg0 20471 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ (SubRing‘𝑆) →
(0g‘𝑆) =
(0g‘𝑈)) |
208 | 22, 207 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0g‘𝑆) = (0g‘𝑈)) |
209 | 208 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (0g‘𝑆) = (0g‘𝑈)) |
210 | 205, 209 | eqtr4d 2767 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (𝐹‘𝑏) = (0g‘𝑆)) |
211 | 210 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → (𝐹‘𝑏) = (0g‘𝑆)) |
212 | 211 | oveq1d 7416 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) = ((0g‘𝑆) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))) |
213 | 63 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → 𝑆 ∈ Ring) |
214 | | eldifi 4118 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈))) → 𝑏 ∈ 𝐷) |
215 | 214, 178 | sylanl2 678 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))) ∈ 𝐾) |
216 | 12, 159, 206, 213, 215 | ringlzd 20184 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → ((0g‘𝑆) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) = (0g‘𝑆)) |
217 | 212, 216 | eqtrd 2764 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) ∧ 𝑙 ∈ (𝐾 ↑m 𝐼)) → ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))) = (0g‘𝑆)) |
218 | 217 | mpteq2dva 5238 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))) = (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ (0g‘𝑆))) |
219 | | fconstmpt 5728 |
. . . . . . . . 9
⊢ ((𝐾 ↑m 𝐼) ×
{(0g‘𝑆)})
= (𝑙 ∈ (𝐾 ↑m 𝐼) ↦
(0g‘𝑆)) |
220 | 187 | cmnmndd 19714 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ Mnd) |
221 | 14, 206 | pws0g 18693 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Mnd ∧ (𝐾 ↑m 𝐼) ∈ V) → ((𝐾 ↑m 𝐼) ×
{(0g‘𝑆)})
= (0g‘(𝑆
↑s (𝐾 ↑m 𝐼)))) |
222 | 220, 64, 221 | syl2anc 583 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐾 ↑m 𝐼) × {(0g‘𝑆)}) =
(0g‘(𝑆
↑s (𝐾 ↑m 𝐼)))) |
223 | 219, 222 | eqtr3id 2778 |
. . . . . . . 8
⊢ (𝜑 → (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ (0g‘𝑆)) = (0g‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) |
224 | 223 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ (0g‘𝑆)) = (0g‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) |
225 | 218, 224 | eqtrd 2764 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐷 ∖ (𝐹 supp (0g‘𝑈)))) → (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))) = (0g‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) |
226 | 225, 186 | suppss2 8180 |
. . . . 5
⊢ (𝜑 → ((𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) supp (0g‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) ⊆ (𝐹 supp (0g‘𝑈))) |
227 | 195, 196,
198, 202, 226 | fsuppsssuppgd 41557 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))) finSupp (0g‘(𝑆 ↑s
(𝐾 ↑m 𝐼)))) |
228 | 14, 12, 184, 64, 186, 187, 194, 227 | pwsgsum 19892 |
. . 3
⊢ (𝜑 → ((𝑆 ↑s (𝐾 ↑m 𝐼)) Σg
(𝑏 ∈ 𝐷 ↦ (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖)))))))) = (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))))) |
229 | 24, 183, 228 | 3eqtrd 2768 |
. 2
⊢ (𝜑 → (𝑄‘𝐹) = (𝑙 ∈ (𝐾 ↑m 𝐼) ↦ (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝑙‘𝑖))))))))) |
230 | | evlsvvval.a |
. 2
⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) |
231 | | ovexd 7436 |
. 2
⊢ (𝜑 → (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖))))))) ∈ V) |
232 | 7, 229, 230, 231 | fvmptd4 41546 |
1
⊢ (𝜑 → ((𝑄‘𝐹)‘𝐴) = (𝑆 Σg (𝑏 ∈ 𝐷 ↦ ((𝐹‘𝑏) · (𝑀 Σg (𝑖 ∈ 𝐼 ↦ ((𝑏‘𝑖) ↑ (𝐴‘𝑖)))))))) |