Step | Hyp | Ref
| Expression |
1 | | mhphf.h |
. . 3
⊢ 𝐻 = (𝐼 mHomP 𝑈) |
2 | | eqid 2736 |
. . 3
⊢
(Base‘𝑈) =
(Base‘𝑈) |
3 | | eqid 2736 |
. . 3
⊢
(0g‘𝑈) = (0g‘𝑈) |
4 | | eqid 2736 |
. . 3
⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly 𝑈) |
5 | | eqid 2736 |
. . 3
⊢
(+g‘(𝐼 mPoly 𝑈)) = (+g‘(𝐼 mPoly 𝑈)) |
6 | | eqid 2736 |
. . 3
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
7 | | eqid 2736 |
. . 3
⊢ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} = {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} |
8 | | mhphf.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
9 | | mhphf.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) |
10 | | mhphf.u |
. . . . . 6
⊢ 𝑈 = (𝑆 ↾s 𝑅) |
11 | 10 | subrgring 20225 |
. . . . 5
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑈 ∈ Ring) |
12 | 9, 11 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ Ring) |
13 | 12 | ringgrpd 19973 |
. . 3
⊢ (𝜑 → 𝑈 ∈ Grp) |
14 | | mhphf.n |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
15 | | mhphf.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ (𝐻‘𝑁)) |
16 | | eqid 2736 |
. . . . . 6
⊢
(algSc‘(𝐼
mPoly 𝑈)) =
(algSc‘(𝐼 mPoly 𝑈)) |
17 | | eqid 2736 |
. . . . . 6
⊢
(0g‘(𝐼 mPoly 𝑈)) = (0g‘(𝐼 mPoly 𝑈)) |
18 | | mhphf.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ CRing) |
19 | 10 | subrgcrng 20226 |
. . . . . . 7
⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑈 ∈ CRing) |
20 | 18, 9, 19 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ CRing) |
21 | 4, 16, 3, 17, 8, 20 | mplascl0 40730 |
. . . . 5
⊢ (𝜑 → ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) = (0g‘(𝐼 mPoly 𝑈))) |
22 | 4, 6, 3, 17, 8, 13 | mpl0 21412 |
. . . . 5
⊢ (𝜑 →
(0g‘(𝐼
mPoly 𝑈)) = ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(0g‘𝑈)})) |
23 | 21, 22 | eqtr2d 2777 |
. . . 4
⊢ (𝜑 → ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(0g‘𝑈)})
= ((algSc‘(𝐼 mPoly
𝑈))‘(0g‘𝑈))) |
24 | | mhphf.m |
. . . . . . . . . 10
⊢ · =
(.r‘𝑆) |
25 | 10, 24 | ressmulr 17188 |
. . . . . . . . 9
⊢ (𝑅 ∈ (SubRing‘𝑆) → · =
(.r‘𝑈)) |
26 | 9, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → · =
(.r‘𝑈)) |
27 | 26 | oveqd 7374 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 ↑ 𝐿) ·
(0g‘𝑈)) =
((𝑁 ↑ 𝐿)(.r‘𝑈)(0g‘𝑈))) |
28 | | eqid 2736 |
. . . . . . . . . . . 12
⊢
(mulGrp‘𝑆) =
(mulGrp‘𝑆) |
29 | 28 | subrgsubm 20235 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ∈ (SubMnd‘(mulGrp‘𝑆))) |
30 | 9, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ (SubMnd‘(mulGrp‘𝑆))) |
31 | | mhphf.l |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ 𝑅) |
32 | | mhphf.e |
. . . . . . . . . . 11
⊢ ↑ =
(.g‘(mulGrp‘𝑆)) |
33 | 32 | submmulgcl 18919 |
. . . . . . . . . 10
⊢ ((𝑅 ∈
(SubMnd‘(mulGrp‘𝑆)) ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ 𝑅) → (𝑁 ↑ 𝐿) ∈ 𝑅) |
34 | 30, 14, 31, 33 | syl3anc 1371 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ 𝑅) |
35 | 10 | subrgbas 20231 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 = (Base‘𝑈)) |
36 | 9, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 = (Base‘𝑈)) |
37 | 34, 36 | eleqtrd 2840 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ (Base‘𝑈)) |
38 | | eqid 2736 |
. . . . . . . . 9
⊢
(.r‘𝑈) = (.r‘𝑈) |
39 | 2, 38, 3 | ringrz 20012 |
. . . . . . . 8
⊢ ((𝑈 ∈ Ring ∧ (𝑁 ↑ 𝐿) ∈ (Base‘𝑈)) → ((𝑁 ↑ 𝐿)(.r‘𝑈)(0g‘𝑈)) = (0g‘𝑈)) |
40 | 12, 37, 39 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 ↑ 𝐿)(.r‘𝑈)(0g‘𝑈)) = (0g‘𝑈)) |
41 | 27, 40 | eqtrd 2776 |
. . . . . 6
⊢ (𝜑 → ((𝑁 ↑ 𝐿) ·
(0g‘𝑈)) =
(0g‘𝑈)) |
42 | | mhphf.q |
. . . . . . . . 9
⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅) |
43 | | mhphf.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑆) |
44 | | eqid 2736 |
. . . . . . . . 9
⊢
(Base‘(𝐼 mPoly
𝑈)) = (Base‘(𝐼 mPoly 𝑈)) |
45 | 2, 3 | ring0cl 19990 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ Ring →
(0g‘𝑈)
∈ (Base‘𝑈)) |
46 | 12, 45 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑈) ∈ (Base‘𝑈)) |
47 | 46, 36 | eleqtrrd 2841 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝑈) ∈ 𝑅) |
48 | | mhphf.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑m 𝐼)) |
49 | 42, 4, 10, 43, 44, 16, 8, 18, 9, 47, 48 | evlsscaval 40734 |
. . . . . . . 8
⊢ (𝜑 → (((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴) = (0g‘𝑈))) |
50 | 49 | simprd 496 |
. . . . . . 7
⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴) = (0g‘𝑈)) |
51 | 50 | oveq2d 7373 |
. . . . . 6
⊢ (𝜑 → ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴)) = ((𝑁 ↑ 𝐿) ·
(0g‘𝑈))) |
52 | 43 | fvexi 6856 |
. . . . . . . . . 10
⊢ 𝐾 ∈ V |
53 | 52 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ V) |
54 | 18 | crngringd 19977 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Ring) |
55 | 43, 24 | ringcl 19981 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Ring ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾) |
56 | 54, 55 | syl3an1 1163 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾) → (𝑗 · 𝑘) ∈ 𝐾) |
57 | 56 | 3expb 1120 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾)) → (𝑗 · 𝑘) ∈ 𝐾) |
58 | 43 | subrgss 20223 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐾) |
59 | 9, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ⊆ 𝐾) |
60 | 59, 31 | sseldd 3945 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈ 𝐾) |
61 | | fconst6g 6731 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ 𝐾 → (𝐼 × {𝐿}):𝐼⟶𝐾) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼 × {𝐿}):𝐼⟶𝐾) |
63 | | elmapi 8787 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (𝐾 ↑m 𝐼) → 𝐴:𝐼⟶𝐾) |
64 | 48, 63 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴:𝐼⟶𝐾) |
65 | | inidm 4178 |
. . . . . . . . . 10
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
66 | 57, 62, 64, 8, 8, 65 | off 7635 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼⟶𝐾) |
67 | 53, 8, 66 | elmapdd 40664 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼)) |
68 | 42, 4, 10, 43, 44, 16, 8, 18, 9, 47, 67 | evlsscaval 40734 |
. . . . . . 7
⊢ (𝜑 → (((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (0g‘𝑈))) |
69 | 68 | simprd 496 |
. . . . . 6
⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (0g‘𝑈)) |
70 | 41, 51, 69 | 3eqtr4rd 2787 |
. . . . 5
⊢ (𝜑 → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴))) |
71 | | fvex 6855 |
. . . . . 6
⊢
((algSc‘(𝐼
mPoly 𝑈))‘(0g‘𝑈)) ∈ V |
72 | | fveq2 6842 |
. . . . . . . 8
⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → (𝑄‘𝑓) = (𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))) |
73 | 72 | fveq1d 6844 |
. . . . . . 7
⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴))) |
74 | 72 | fveq1d 6844 |
. . . . . . . 8
⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴)) |
75 | 74 | oveq2d 7373 |
. . . . . . 7
⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴))) |
76 | 73, 75 | eqeq12d 2752 |
. . . . . 6
⊢ (𝑓 = ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴)))) |
77 | 71, 76 | elab 3630 |
. . . . 5
⊢
(((algSc‘(𝐼
mPoly 𝑈))‘(0g‘𝑈)) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)))‘𝐴))) |
78 | 70, 77 | sylibr 233 |
. . . 4
⊢ (𝜑 → ((algSc‘(𝐼 mPoly 𝑈))‘(0g‘𝑈)) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) |
79 | 23, 78 | eqeltrd 2838 |
. . 3
⊢ (𝜑 → ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ×
{(0g‘𝑈)})
∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) |
80 | 4 | mplassa 21427 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑈 ∈ CRing) → (𝐼 mPoly 𝑈) ∈ AssAlg) |
81 | 8, 20, 80 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 mPoly 𝑈) ∈ AssAlg) |
82 | 81 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝐼 mPoly 𝑈) ∈ AssAlg) |
83 | 4, 8, 12 | mplsca 21417 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 = (Scalar‘(𝐼 mPoly 𝑈))) |
84 | 83 | fveq2d 6846 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑈) =
(Base‘(Scalar‘(𝐼 mPoly 𝑈)))) |
85 | 84 | eleq2d 2823 |
. . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ (Base‘𝑈) ↔ 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))))) |
86 | 85 | biimpa 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈)))) |
87 | 86 | adantrl 714 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈)))) |
88 | | fvexd 6857 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝑈) ∈ V) |
89 | | ovex 7390 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ↑m 𝐼) ∈ V |
90 | 89 | rabex 5289 |
. . . . . . . . . . . 12
⊢ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V |
91 | 90 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V) |
92 | | eqid 2736 |
. . . . . . . . . . . . . . . 16
⊢
(1r‘𝑈) = (1r‘𝑈) |
93 | 2, 92 | ringidcl 19989 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ Ring →
(1r‘𝑈)
∈ (Base‘𝑈)) |
94 | 12, 93 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1r‘𝑈) ∈ (Base‘𝑈)) |
95 | 94, 46 | ifcld 4532 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ (Base‘𝑈)) |
96 | 95 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ (Base‘𝑈)) |
97 | 96 | fmpttd 7063 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))):{ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}⟶(Base‘𝑈)) |
98 | 88, 91, 97 | elmapdd 40664 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ ((Base‘𝑈) ↑m {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin})) |
99 | | eqid 2736 |
. . . . . . . . . . 11
⊢ (𝐼 mPwSer 𝑈) = (𝐼 mPwSer 𝑈) |
100 | | eqid 2736 |
. . . . . . . . . . 11
⊢
(Base‘(𝐼
mPwSer 𝑈)) =
(Base‘(𝐼 mPwSer 𝑈)) |
101 | 99, 2, 6, 100, 8 | psrbas 21346 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑈)) = ((Base‘𝑈) ↑m {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin})) |
102 | 98, 101 | eleqtrrd 2841 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPwSer 𝑈))) |
103 | 90 | mptex 7173 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ V |
104 | 103 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ V) |
105 | | fvexd 6857 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑈) ∈ V) |
106 | | funmpt 6539 |
. . . . . . . . . . 11
⊢ Fun
(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) |
107 | 106 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → Fun (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) |
108 | | snfi 8988 |
. . . . . . . . . . . 12
⊢ {𝑎} ∈ Fin |
109 | 108 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑎} ∈ Fin) |
110 | | eldifsnneq 4751 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ {𝑎}) → ¬ 𝑤 = 𝑎) |
111 | 110 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ {𝑎})) → ¬ 𝑤 = 𝑎) |
112 | 111 | iffalsed 4497 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∖ {𝑎})) → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) = (0g‘𝑈)) |
113 | 112, 91 | suppss2 8131 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) supp (0g‘𝑈)) ⊆ {𝑎}) |
114 | 109, 113 | ssfid 9211 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) supp (0g‘𝑈)) ∈ Fin) |
115 | 104, 105,
107, 114 | isfsuppd 40665 |
. . . . . . . . 9
⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) finSupp (0g‘𝑈)) |
116 | 4, 99, 100, 3, 44 | mplelbas 21399 |
. . . . . . . . 9
⊢ ((𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ↔ ((𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPwSer 𝑈)) ∧ (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) finSupp (0g‘𝑈))) |
117 | 102, 115,
116 | sylanbrc 583 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈))) |
118 | 117 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈))) |
119 | | eqid 2736 |
. . . . . . . 8
⊢
(Scalar‘(𝐼
mPoly 𝑈)) =
(Scalar‘(𝐼 mPoly
𝑈)) |
120 | | eqid 2736 |
. . . . . . . 8
⊢
(Base‘(Scalar‘(𝐼 mPoly 𝑈))) = (Base‘(Scalar‘(𝐼 mPoly 𝑈))) |
121 | | eqid 2736 |
. . . . . . . 8
⊢
(.r‘(𝐼 mPoly 𝑈)) = (.r‘(𝐼 mPoly 𝑈)) |
122 | | eqid 2736 |
. . . . . . . 8
⊢ (
·𝑠 ‘(𝐼 mPoly 𝑈)) = ( ·𝑠
‘(𝐼 mPoly 𝑈)) |
123 | 16, 119, 120, 44, 121, 122 | asclmul1 21289 |
. . . . . . 7
⊢ (((𝐼 mPoly 𝑈) ∈ AssAlg ∧ 𝑏 ∈ (Base‘(Scalar‘(𝐼 mPoly 𝑈))) ∧ (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (𝑏( ·𝑠
‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))) |
124 | 82, 87, 118, 123 | syl3anc 1371 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (𝑏( ·𝑠
‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))) |
125 | | simprr 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ (Base‘𝑈)) |
126 | 4, 122, 2, 44, 38, 6, 125, 118 | mplvsca 21419 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑏( ·𝑠
‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏}) ∘f
(.r‘𝑈)(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))) |
127 | 124, 126 | eqtrd 2776 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏}) ∘f
(.r‘𝑈)(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))) |
128 | | vex 3449 |
. . . . . . 7
⊢ 𝑏 ∈ V |
129 | | fnconstg 6730 |
. . . . . . 7
⊢ (𝑏 ∈ V → ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏}) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
130 | 128, 129 | mp1i 13 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏}) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
131 | | fvex 6855 |
. . . . . . . . 9
⊢
(1r‘𝑈) ∈ V |
132 | | fvex 6855 |
. . . . . . . . 9
⊢
(0g‘𝑈) ∈ V |
133 | 131, 132 | ifex 4536 |
. . . . . . . 8
⊢ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ V |
134 | | eqid 2736 |
. . . . . . . 8
⊢ (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) = (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) |
135 | 133, 134 | fnmpti 6644 |
. . . . . . 7
⊢ (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
136 | 135 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) Fn {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
137 | 90 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∈
V) |
138 | | inidm 4178 |
. . . . . 6
⊢ ({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∩ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
139 | 128 | fvconst2 7153 |
. . . . . . 7
⊢ (𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → (({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏})‘𝑠) = 𝑏) |
140 | 139 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏})‘𝑠) = 𝑏) |
141 | | equequ1 2028 |
. . . . . . . . 9
⊢ (𝑤 = 𝑠 → (𝑤 = 𝑎 ↔ 𝑠 = 𝑎)) |
142 | 141 | ifbid 4509 |
. . . . . . . 8
⊢ (𝑤 = 𝑠 → if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)) = if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈))) |
143 | 131, 132 | ifex 4536 |
. . . . . . . 8
⊢ if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈)) ∈ V |
144 | 142, 134,
143 | fvmpt 6948 |
. . . . . . 7
⊢ (𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → ((𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))‘𝑠) = if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈))) |
145 | 144 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → ((𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))‘𝑠) = if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈))) |
146 | 130, 136,
137, 137, 138, 140, 145 | offval 7626 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (({ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} × {𝑏}) ∘f
(.r‘𝑈)(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏(.r‘𝑈)if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈))))) |
147 | | ovif2 7455 |
. . . . . . 7
⊢ (𝑏(.r‘𝑈)if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈))) = if(𝑠 = 𝑎, (𝑏(.r‘𝑈)(1r‘𝑈)), (𝑏(.r‘𝑈)(0g‘𝑈))) |
148 | 12 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑈 ∈ Ring) |
149 | | simplrr 776 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑏 ∈ (Base‘𝑈)) |
150 | 2, 38, 92, 148, 149 | ringridmd 40692 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑏(.r‘𝑈)(1r‘𝑈)) = 𝑏) |
151 | 2, 38, 3 | ringrz 20012 |
. . . . . . . . 9
⊢ ((𝑈 ∈ Ring ∧ 𝑏 ∈ (Base‘𝑈)) → (𝑏(.r‘𝑈)(0g‘𝑈)) = (0g‘𝑈)) |
152 | 148, 149,
151 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑏(.r‘𝑈)(0g‘𝑈)) = (0g‘𝑈)) |
153 | 150, 152 | ifeq12d 4507 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → if(𝑠 = 𝑎, (𝑏(.r‘𝑈)(1r‘𝑈)), (𝑏(.r‘𝑈)(0g‘𝑈))) = if(𝑠 = 𝑎, 𝑏, (0g‘𝑈))) |
154 | 147, 153 | eqtrid 2788 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑏(.r‘𝑈)if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈))) = if(𝑠 = 𝑎, 𝑏, (0g‘𝑈))) |
155 | 154 | mpteq2dva 5205 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ (𝑏(.r‘𝑈)if(𝑠 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g‘𝑈)))) |
156 | 127, 146,
155 | 3eqtrd 2780 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) = (𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g‘𝑈)))) |
157 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐼 ∈ 𝑉) |
158 | 18 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑆 ∈ CRing) |
159 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑅 ∈ (SubRing‘𝑆)) |
160 | 67 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼)) |
161 | 12 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑈 ∈ Ring) |
162 | 4, 44, 2, 16, 157, 161 | mplasclf 21473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (algSc‘(𝐼 mPoly 𝑈)):(Base‘𝑈)⟶(Base‘(𝐼 mPoly 𝑈))) |
163 | 162, 125 | ffvelcdmd 7036 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈))) |
164 | | eqidd 2737 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴))) |
165 | 163, 164 | jca 512 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)))) |
166 | | elrabi 3639 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} → 𝑎 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
167 | 166 | ad2antrl 726 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
168 | 42, 4, 10, 44, 43, 28, 32, 3, 92, 6, 134, 157, 158, 159, 160, 167 | evlsbagval 40736 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))))) |
169 | 42, 4, 10, 43, 44, 157, 158, 159, 160, 165, 168, 121, 24 | evlsmulval 40739 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))))) |
170 | 169 | simprd 496 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))))) |
171 | 28, 43 | mgpbas 19902 |
. . . . . . . . . . . 12
⊢ 𝐾 =
(Base‘(mulGrp‘𝑆)) |
172 | 28 | ringmgp 19970 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Ring →
(mulGrp‘𝑆) ∈
Mnd) |
173 | 54, 172 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (mulGrp‘𝑆) ∈ Mnd) |
174 | 171, 32, 173, 14, 60 | mulgnn0cld 18897 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ↑ 𝐿) ∈ 𝐾) |
175 | 174 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑁 ↑ 𝐿) ∈ 𝐾) |
176 | 36, 59 | eqsstrrd 3983 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Base‘𝑈) ⊆ 𝐾) |
177 | 176 | sselda 3944 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ 𝐾) |
178 | 177 | adantrl 714 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ 𝐾) |
179 | 43, 24 | crngcom 19982 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ CRing ∧ (𝑁 ↑ 𝐿) ∈ 𝐾 ∧ 𝑏 ∈ 𝐾) → ((𝑁 ↑ 𝐿) · 𝑏) = (𝑏 · (𝑁 ↑ 𝐿))) |
180 | 158, 175,
178, 179 | syl3anc 1371 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 ↑ 𝐿) · 𝑏) = (𝑏 · (𝑁 ↑ 𝐿))) |
181 | 180 | oveq1d 7372 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑁 ↑ 𝐿) · 𝑏) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑏 · (𝑁 ↑ 𝐿)) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) |
182 | 158 | crngringd 19977 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑆 ∈ Ring) |
183 | | eqid 2736 |
. . . . . . . . . . 11
⊢
(1r‘𝑆) = (1r‘𝑆) |
184 | 28, 183 | ringidval 19915 |
. . . . . . . . . 10
⊢
(1r‘𝑆) = (0g‘(mulGrp‘𝑆)) |
185 | 28 | crngmgp 19972 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ CRing →
(mulGrp‘𝑆) ∈
CMnd) |
186 | 18, 185 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (mulGrp‘𝑆) ∈ CMnd) |
187 | 186 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (mulGrp‘𝑆) ∈ CMnd) |
188 | 173 | ad2antrr 724 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (mulGrp‘𝑆) ∈ Mnd) |
189 | | elrabi 3639 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑎 ∈ (ℕ0
↑m 𝐼)) |
190 | | elmapi 8787 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (ℕ0
↑m 𝐼)
→ 𝑎:𝐼⟶ℕ0) |
191 | 166, 189,
190 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} → 𝑎:𝐼⟶ℕ0) |
192 | 191 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝑎:𝐼⟶ℕ0) |
193 | 192 | adantrr 715 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎:𝐼⟶ℕ0) |
194 | 193 | ffvelcdmda 7035 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (𝑎‘𝑣) ∈
ℕ0) |
195 | 64 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝐴:𝐼⟶𝐾) |
196 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝑣 ∈ 𝐼) |
197 | 195, 196 | ffvelcdmd 7036 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) ∈ 𝐾) |
198 | 171, 32, 188, 194, 197 | mulgnn0cld 18897 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (𝐴‘𝑣)) ∈ 𝐾) |
199 | 198 | fmpttd 7063 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))):𝐼⟶𝐾) |
200 | 6 | psrbagfsupp 21322 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} → 𝑎 finSupp 0) |
201 | 200 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → 𝑎 finSupp 0) |
202 | 201 | fsuppimpd 9312 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin}) → (𝑎 supp 0) ∈
Fin) |
203 | 166, 202 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑎 supp 0) ∈ Fin) |
204 | 203 | adantrr 715 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) ∈ Fin) |
205 | 193 | feqmptd 6910 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑎 = (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) |
206 | 205 | oveq1d 7372 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) = ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0)) |
207 | | ssidd 3967 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑎 supp 0) ⊆ (𝑎 supp 0)) |
208 | 206, 207 | eqsstrrd 3983 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0) ⊆ (𝑎 supp 0)) |
209 | 171, 184,
32 | mulg0 18879 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐾 → (0 ↑ 𝑘) = (1r‘𝑆)) |
210 | 209 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑘 ∈ 𝐾) → (0 ↑ 𝑘) = (1r‘𝑆)) |
211 | | c0ex 11149 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
212 | 211 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 0 ∈ V) |
213 | 208, 210,
194, 197, 212 | suppssov1 8129 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ⊆ (𝑎 supp 0)) |
214 | 204, 213 | ssfid 9211 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ∈ Fin) |
215 | 171, 184,
187, 157, 199, 214 | gsumcl2 19691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))) ∈ 𝐾) |
216 | 43, 24, 182, 175, 178, 215 | ringassd 40690 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑁 ↑ 𝐿) · 𝑏) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) · (𝑏 ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))) |
217 | 43, 24, 182, 178, 175, 215 | ringassd 40690 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑏 · (𝑁 ↑ 𝐿)) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = (𝑏 · ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))) |
218 | 181, 216,
217 | 3eqtr3d 2784 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 ↑ 𝐿) · (𝑏 ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) = (𝑏 · ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))) |
219 | 48 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐴 ∈ (𝐾 ↑m 𝐼)) |
220 | 36 | eleq2d 2823 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑏 ∈ 𝑅 ↔ 𝑏 ∈ (Base‘𝑈))) |
221 | 220 | biimpar 478 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ (Base‘𝑈)) → 𝑏 ∈ 𝑅) |
222 | 221 | adantrl 714 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝑏 ∈ 𝑅) |
223 | 42, 4, 10, 43, 44, 16, 157, 158, 159, 222, 219 | evlsscaval 40734 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘𝐴) = 𝑏)) |
224 | 42, 4, 10, 44, 43, 28, 32, 3, 92, 6, 134, 157, 158, 159, 219, 167 | evlsbagval 40736 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈))))‘𝐴) = ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) |
225 | 42, 4, 10, 43, 44, 157, 158, 159, 219, 223, 224, 121, 24 | evlsmulval 40739 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴) = (𝑏 ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))) |
226 | 225 | simprd 496 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴) = (𝑏 ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) |
227 | 226 | oveq2d 7373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴)) = ((𝑁 ↑ 𝐿) · (𝑏 ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))) |
228 | 42, 4, 10, 43, 44, 16, 157, 158, 159, 222, 160 | evlsscaval 40734 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = 𝑏)) |
229 | 228 | simprd 496 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = 𝑏) |
230 | | fconst6g 6731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐿 ∈ 𝑅 → (𝐼 × {𝐿}):𝐼⟶𝑅) |
231 | 31, 230 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐼 × {𝐿}):𝐼⟶𝑅) |
232 | 231 | ffnd 6669 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐼 × {𝐿}) Fn 𝐼) |
233 | 232 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝐼 × {𝐿}) Fn 𝐼) |
234 | 64 | ffnd 6669 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 Fn 𝐼) |
235 | 234 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → 𝐴 Fn 𝐼) |
236 | 31 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝐿 ∈ 𝑅) |
237 | | fvconst2g 7151 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ 𝑅 ∧ 𝑣 ∈ 𝐼) → ((𝐼 × {𝐿})‘𝑣) = 𝐿) |
238 | 236, 196,
237 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝐼 × {𝐿})‘𝑣) = 𝐿) |
239 | | eqidd 2737 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) = (𝐴‘𝑣)) |
240 | 233, 235,
157, 157, 65, 238, 239 | ofval 7628 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣) = (𝐿 · (𝐴‘𝑣))) |
241 | 240 | oveq2d 7373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)) = ((𝑎‘𝑣) ↑ (𝐿 · (𝐴‘𝑣)))) |
242 | 186 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → (mulGrp‘𝑆) ∈ CMnd) |
243 | 60 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → 𝐿 ∈ 𝐾) |
244 | 28, 24 | mgpplusg 19900 |
. . . . . . . . . . . . . 14
⊢ · =
(+g‘(mulGrp‘𝑆)) |
245 | 171, 32, 244 | mulgnn0di 19604 |
. . . . . . . . . . . . 13
⊢
(((mulGrp‘𝑆)
∈ CMnd ∧ ((𝑎‘𝑣) ∈ ℕ0 ∧ 𝐿 ∈ 𝐾 ∧ (𝐴‘𝑣) ∈ 𝐾)) → ((𝑎‘𝑣) ↑ (𝐿 · (𝐴‘𝑣))) = (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))) |
246 | 242, 194,
243, 197, 245 | syl13anc 1372 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (𝐿 · (𝐴‘𝑣))) = (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))) |
247 | 241, 246 | eqtrd 2776 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)) = (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))) |
248 | 247 | mpteq2dva 5205 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))) = (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) |
249 | 248 | oveq2d 7373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))) = ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) |
250 | 186 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (mulGrp‘𝑆) ∈ CMnd) |
251 | 8 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝐼 ∈ 𝑉) |
252 | 173 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → (mulGrp‘𝑆) ∈ Mnd) |
253 | 192 | ffvelcdmda 7035 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → (𝑎‘𝑣) ∈
ℕ0) |
254 | 60 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → 𝐿 ∈ 𝐾) |
255 | 171, 32, 252, 253, 254 | mulgnn0cld 18897 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ 𝐿) ∈ 𝐾) |
256 | 64 | ffvelcdmda 7035 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) ∈ 𝐾) |
257 | 256 | adantlr 713 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → (𝐴‘𝑣) ∈ 𝐾) |
258 | 171, 32, 252, 253, 257 | mulgnn0cld 18897 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑣 ∈ 𝐼) → ((𝑎‘𝑣) ↑ (𝐴‘𝑣)) ∈ 𝐾) |
259 | | eqidd 2737 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) = (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) |
260 | | eqidd 2737 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) = (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))) |
261 | 251 | mptexd 7174 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) ∈ V) |
262 | | fvexd 6857 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (1r‘𝑆) ∈ V) |
263 | | funmpt 6539 |
. . . . . . . . . . . . . 14
⊢ Fun
(𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) |
264 | 263 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → Fun (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) |
265 | 192 | feqmptd 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 𝑎 = (𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣))) |
266 | 265 | oveq1d 7372 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑎 supp 0) = ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0)) |
267 | | ssidd 3967 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑎 supp 0) ⊆ (𝑎 supp 0)) |
268 | 266, 267 | eqsstrrd 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ (𝑎‘𝑣)) supp 0) ⊆ (𝑎 supp 0)) |
269 | 209 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) ∧ 𝑘 ∈ 𝐾) → (0 ↑ 𝑘) = (1r‘𝑆)) |
270 | 211 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → 0 ∈ V) |
271 | 268, 269,
253, 254, 270 | suppssov1 8129 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) supp (1r‘𝑆)) ⊆ (𝑎 supp 0)) |
272 | 203, 271 | ssfid 9211 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) supp (1r‘𝑆)) ∈ Fin) |
273 | 261, 262,
264, 272 | isfsuppd 40665 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿)) finSupp (1r‘𝑆)) |
274 | 251 | mptexd 7174 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) ∈ V) |
275 | | funmpt 6539 |
. . . . . . . . . . . . . 14
⊢ Fun
(𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) |
276 | 275 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → Fun (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))) |
277 | 268, 269,
253, 257, 270 | suppssov1 8129 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ⊆ (𝑎 supp 0)) |
278 | 203, 277 | ssfid 9211 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) supp (1r‘𝑆)) ∈ Fin) |
279 | 274, 262,
276, 278 | isfsuppd 40665 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))) finSupp (1r‘𝑆)) |
280 | 171, 184,
244, 250, 251, 255, 258, 259, 260, 273, 279 | gsummptfsadd 19701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = (((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) |
281 | 6, 7, 171, 32, 8, 173, 60, 14 | mhphflem 40756 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) = (𝑁 ↑ 𝐿)) |
282 | 281 | oveq1d 7372 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → (((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ 𝐿))) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) |
283 | 280, 282 | eqtrd 2776 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁}) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) |
284 | 283 | adantrr 715 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ (((𝑎‘𝑣) ↑ 𝐿) · ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))) = ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) |
285 | 249, 284 | eqtrd 2776 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((mulGrp‘𝑆) Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣)))) = ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣)))))) |
286 | 229, 285 | oveq12d 7375 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))) = (𝑏 · ((𝑁 ↑ 𝐿) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (𝐴‘𝑣))))))) |
287 | 218, 227,
286 | 3eqtr4rd 2787 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((𝑄‘((algSc‘(𝐼 mPoly 𝑈))‘𝑏))‘((𝐼 × {𝐿}) ∘f · 𝐴)) ·
((mulGrp‘𝑆)
Σg (𝑣 ∈ 𝐼 ↦ ((𝑎‘𝑣) ↑ (((𝐼 × {𝐿}) ∘f · 𝐴)‘𝑣))))) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴))) |
288 | 170, 287 | eqtrd 2776 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴))) |
289 | | ovex 7390 |
. . . . . 6
⊢
(((algSc‘(𝐼
mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ V |
290 | | fveq2 6842 |
. . . . . . . 8
⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → (𝑄‘𝑓) = (𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))) |
291 | 290 | fveq1d 6844 |
. . . . . . 7
⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴))) |
292 | 290 | fveq1d 6844 |
. . . . . . . 8
⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴)) |
293 | 292 | oveq2d 7373 |
. . . . . . 7
⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴))) |
294 | 291, 293 | eqeq12d 2752 |
. . . . . 6
⊢ (𝑓 = (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴)))) |
295 | 289, 294 | elab 3630 |
. . . . 5
⊢
((((algSc‘(𝐼
mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))))‘𝐴))) |
296 | 288, 295 | sylibr 233 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (((algSc‘(𝐼 mPoly 𝑈))‘𝑏)(.r‘(𝐼 mPoly 𝑈))(𝑤 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑤 = 𝑎, (1r‘𝑈), (0g‘𝑈)))) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) |
297 | 156, 296 | eqeltrrd 2839 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑁} ∧ 𝑏 ∈ (Base‘𝑈))) → (𝑠 ∈ {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑠 = 𝑎, 𝑏, (0g‘𝑈))) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) |
298 | | elin 3926 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻‘𝑁) ∧ 𝑥 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})) |
299 | | vex 3449 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
300 | | fveq2 6842 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑥 → (𝑄‘𝑓) = (𝑄‘𝑥)) |
301 | 300 | fveq1d 6844 |
. . . . . . . . 9
⊢ (𝑓 = 𝑥 → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴))) |
302 | 300 | fveq1d 6844 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑥 → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘𝑥)‘𝐴)) |
303 | 302 | oveq2d 7373 |
. . . . . . . . 9
⊢ (𝑓 = 𝑥 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) |
304 | 301, 303 | eqeq12d 2752 |
. . . . . . . 8
⊢ (𝑓 = 𝑥 → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) |
305 | 299, 304 | elab 3630 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) |
306 | 305 | anbi2i 623 |
. . . . . 6
⊢ ((𝑥 ∈ (𝐻‘𝑁) ∧ 𝑥 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) |
307 | 298, 306 | bitri 274 |
. . . . 5
⊢ (𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) |
308 | | elin 3926 |
. . . . . 6
⊢ (𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻‘𝑁) ∧ 𝑦 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})) |
309 | | vex 3449 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
310 | | fveq2 6842 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑦 → (𝑄‘𝑓) = (𝑄‘𝑦)) |
311 | 310 | fveq1d 6844 |
. . . . . . . . 9
⊢ (𝑓 = 𝑦 → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴))) |
312 | 310 | fveq1d 6844 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑦 → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘𝑦)‘𝐴)) |
313 | 312 | oveq2d 7373 |
. . . . . . . . 9
⊢ (𝑓 = 𝑦 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))) |
314 | 311, 313 | eqeq12d 2752 |
. . . . . . . 8
⊢ (𝑓 = 𝑦 → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) |
315 | 309, 314 | elab 3630 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))) |
316 | 315 | anbi2i 623 |
. . . . . 6
⊢ ((𝑦 ∈ (𝐻‘𝑁) ∧ 𝑦 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) |
317 | 308, 316 | bitri 274 |
. . . . 5
⊢ (𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ↔ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) |
318 | 307, 317 | anbi12i 627 |
. . . 4
⊢ ((𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))})) ↔ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) |
319 | 54 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑆 ∈ Ring) |
320 | 174 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑁 ↑ 𝐿) ∈ 𝐾) |
321 | | eqid 2736 |
. . . . . . . . 9
⊢ (𝑆 ↑s
(Base‘(𝑆
↑s 𝐼))) = (𝑆 ↑s
(Base‘(𝑆
↑s 𝐼))) |
322 | | eqid 2736 |
. . . . . . . . 9
⊢
(Base‘(𝑆
↑s (Base‘(𝑆 ↑s 𝐼)))) = (Base‘(𝑆 ↑s
(Base‘(𝑆
↑s 𝐼)))) |
323 | 18 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑆 ∈ CRing) |
324 | | fvexd 6857 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (Base‘(𝑆 ↑s 𝐼)) ∈ V) |
325 | | eqid 2736 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ↑s
(𝐾 ↑m 𝐼)) = (𝑆 ↑s (𝐾 ↑m 𝐼)) |
326 | 42, 4, 10, 325, 43 | evlsrhm 21498 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆 ↑s (𝐾 ↑m 𝐼)))) |
327 | 8, 18, 9, 326 | syl3anc 1371 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆 ↑s (𝐾 ↑m 𝐼)))) |
328 | | eqid 2736 |
. . . . . . . . . . . . . 14
⊢
(Base‘(𝑆
↑s (𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))) |
329 | 44, 328 | rhmf 20158 |
. . . . . . . . . . . . 13
⊢ (𝑄 ∈ ((𝐼 mPoly 𝑈) RingHom (𝑆 ↑s (𝐾 ↑m 𝐼))) → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
330 | 327, 329 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
331 | 330 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑄:(Base‘(𝐼 mPoly 𝑈))⟶(Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
332 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝐼 ∈ 𝑉) |
333 | 12 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑈 ∈ Ring) |
334 | 14 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑁 ∈
ℕ0) |
335 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑥 ∈ (𝐻‘𝑁)) |
336 | 1, 4, 44, 332, 333, 334, 335 | mhpmpl 21534 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐻‘𝑁)) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈))) |
337 | 336 | adantrr 715 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈))) |
338 | 337 | adantrr 715 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑥 ∈ (Base‘(𝐼 mPoly 𝑈))) |
339 | 331, 338 | ffvelcdmd 7036 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑥) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
340 | | eqid 2736 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ↑s 𝐼) = (𝑆 ↑s 𝐼) |
341 | 340, 43 | pwsbas 17369 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ CRing ∧ 𝐼 ∈ 𝑉) → (𝐾 ↑m 𝐼) = (Base‘(𝑆 ↑s 𝐼))) |
342 | 18, 8, 341 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 ↑m 𝐼) = (Base‘(𝑆 ↑s 𝐼))) |
343 | 342 | oveq2d 7373 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ↑s (𝐾 ↑m 𝐼)) = (𝑆 ↑s
(Base‘(𝑆
↑s 𝐼)))) |
344 | 343 | fveq2d 6846 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘(𝑆 ↑s
(𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s
(Base‘(𝑆
↑s 𝐼))))) |
345 | 344 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼))) = (Base‘(𝑆 ↑s
(Base‘(𝑆
↑s 𝐼))))) |
346 | 339, 345 | eleqtrd 2840 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑥) ∈ (Base‘(𝑆 ↑s
(Base‘(𝑆
↑s 𝐼))))) |
347 | 321, 43, 322, 323, 324, 346 | pwselbas 17371 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑥):(Base‘(𝑆 ↑s 𝐼))⟶𝐾) |
348 | 48, 342 | eleqtrd 2840 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (Base‘(𝑆 ↑s 𝐼))) |
349 | 348 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐴 ∈ (Base‘(𝑆 ↑s 𝐼))) |
350 | 347, 349 | ffvelcdmd 7036 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘𝑥)‘𝐴) ∈ 𝐾) |
351 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝐼 ∈ 𝑉) |
352 | 12 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑈 ∈ Ring) |
353 | 14 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑁 ∈
ℕ0) |
354 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑦 ∈ (𝐻‘𝑁)) |
355 | 1, 4, 44, 351, 352, 353, 354 | mhpmpl 21534 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (𝐻‘𝑁)) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈))) |
356 | 355 | adantrr 715 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈))) |
357 | 356 | adantrl 714 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑦 ∈ (Base‘(𝐼 mPoly 𝑈))) |
358 | 331, 357 | ffvelcdmd 7036 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑦) ∈ (Base‘(𝑆 ↑s (𝐾 ↑m 𝐼)))) |
359 | 358, 345 | eleqtrd 2840 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑦) ∈ (Base‘(𝑆 ↑s
(Base‘(𝑆
↑s 𝐼))))) |
360 | 321, 43, 322, 323, 324, 359 | pwselbas 17371 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑄‘𝑦):(Base‘(𝑆 ↑s 𝐼))⟶𝐾) |
361 | 360, 349 | ffvelcdmd 7036 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘𝑦)‘𝐴) ∈ 𝐾) |
362 | | eqid 2736 |
. . . . . . . 8
⊢
(+g‘𝑆) = (+g‘𝑆) |
363 | 43, 362, 24 | ringdi 19987 |
. . . . . . 7
⊢ ((𝑆 ∈ Ring ∧ ((𝑁 ↑ 𝐿) ∈ 𝐾 ∧ ((𝑄‘𝑥)‘𝐴) ∈ 𝐾 ∧ ((𝑄‘𝑦)‘𝐴) ∈ 𝐾)) → ((𝑁 ↑ 𝐿) · (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) |
364 | 319, 320,
350, 361, 363 | syl13anc 1372 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑁 ↑ 𝐿) · (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) |
365 | 8 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐼 ∈ 𝑉) |
366 | 9 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝑅 ∈ (SubRing‘𝑆)) |
367 | 48 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐴 ∈ (𝐾 ↑m 𝐼)) |
368 | | eqidd 2737 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) → ((𝑄‘𝑥)‘𝐴) = ((𝑄‘𝑥)‘𝐴)) |
369 | 336, 368 | anim12dan 619 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘𝐴) = ((𝑄‘𝑥)‘𝐴))) |
370 | 369 | adantrr 715 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘𝐴) = ((𝑄‘𝑥)‘𝐴))) |
371 | | eqidd 2737 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))) → ((𝑄‘𝑦)‘𝐴) = ((𝑄‘𝑦)‘𝐴)) |
372 | 355, 371 | anim12dan 619 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘𝐴) = ((𝑄‘𝑦)‘𝐴))) |
373 | 372 | adantrl 714 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘𝐴) = ((𝑄‘𝑦)‘𝐴))) |
374 | 42, 4, 10, 43, 44, 365, 323, 366, 367, 370, 373, 5, 362 | evlsaddval 40738 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴) = (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴)))) |
375 | 374 | simprd 496 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴) = (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴))) |
376 | 375 | oveq2d 7373 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)) = ((𝑁 ↑ 𝐿) · (((𝑄‘𝑥)‘𝐴)(+g‘𝑆)((𝑄‘𝑦)‘𝐴)))) |
377 | 52 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐾 ∈ V) |
378 | 57 | adantlr 713 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) ∧ (𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾)) → (𝑗 · 𝑘) ∈ 𝐾) |
379 | 62 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝐼 × {𝐿}):𝐼⟶𝐾) |
380 | 64 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → 𝐴:𝐼⟶𝐾) |
381 | 378, 379,
380, 365, 365, 65 | off 7635 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝐼 × {𝐿}) ∘f · 𝐴):𝐼⟶𝐾) |
382 | 377, 365,
381 | elmapdd 40664 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝐼 × {𝐿}) ∘f · 𝐴) ∈ (𝐾 ↑m 𝐼)) |
383 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) → ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) |
384 | 336, 383 | anim12dan 619 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) |
385 | 384 | adantrr 715 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑥 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴)))) |
386 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))) → ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))) |
387 | 355, 386 | anim12dan 619 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) |
388 | 387 | adantrl 714 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑦 ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) |
389 | 42, 4, 10, 43, 44, 365, 323, 366, 382, 385, 388, 5, 362 | evlsaddval 40738 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ (Base‘(𝐼 mPoly 𝑈)) ∧ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) |
390 | 389 | simprd 496 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = (((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))(+g‘𝑆)((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴)))) |
391 | 364, 376,
390 | 3eqtr4rd 2787 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))) |
392 | | ovex 7390 |
. . . . . 6
⊢ (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ V |
393 | | fveq2 6842 |
. . . . . . . 8
⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → (𝑄‘𝑓) = (𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))) |
394 | 393 | fveq1d 6844 |
. . . . . . 7
⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴))) |
395 | 393 | fveq1d 6844 |
. . . . . . . 8
⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)) |
396 | 395 | oveq2d 7373 |
. . . . . . 7
⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))) |
397 | 394, 396 | eqeq12d 2752 |
. . . . . 6
⊢ (𝑓 = (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴)))) |
398 | 392, 397 | elab 3630 |
. . . . 5
⊢ ((𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘(𝑥(+g‘(𝐼 mPoly 𝑈))𝑦))‘𝐴))) |
399 | 391, 398 | sylibr 233 |
. . . 4
⊢ ((𝜑 ∧ ((𝑥 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑥)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑥)‘𝐴))) ∧ (𝑦 ∈ (𝐻‘𝑁) ∧ ((𝑄‘𝑦)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑦)‘𝐴))))) → (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) |
400 | 318, 399 | sylan2b 594 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) ∧ 𝑦 ∈ ((𝐻‘𝑁) ∩ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}))) → (𝑥(+g‘(𝐼 mPoly 𝑈))𝑦) ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) |
401 | 1, 2, 3, 4, 5, 6, 7, 8, 13, 14, 15, 79, 297, 400 | mhpind 40755 |
. 2
⊢ (𝜑 → 𝑋 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))}) |
402 | | fveq2 6842 |
. . . . . 6
⊢ (𝑓 = 𝑋 → (𝑄‘𝑓) = (𝑄‘𝑋)) |
403 | 402 | fveq1d 6844 |
. . . . 5
⊢ (𝑓 = 𝑋 → ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴))) |
404 | 402 | fveq1d 6844 |
. . . . . 6
⊢ (𝑓 = 𝑋 → ((𝑄‘𝑓)‘𝐴) = ((𝑄‘𝑋)‘𝐴)) |
405 | 404 | oveq2d 7373 |
. . . . 5
⊢ (𝑓 = 𝑋 → ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) |
406 | 403, 405 | eqeq12d 2752 |
. . . 4
⊢ (𝑓 = 𝑋 → (((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴)) ↔ ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))) |
407 | 406 | elabg 3628 |
. . 3
⊢ (𝑋 ∈ (𝐻‘𝑁) → (𝑋 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))) |
408 | 15, 407 | syl 17 |
. 2
⊢ (𝜑 → (𝑋 ∈ {𝑓 ∣ ((𝑄‘𝑓)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑓)‘𝐴))} ↔ ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴)))) |
409 | 401, 408 | mpbid 231 |
1
⊢ (𝜑 → ((𝑄‘𝑋)‘((𝐼 × {𝐿}) ∘f · 𝐴)) = ((𝑁 ↑ 𝐿) · ((𝑄‘𝑋)‘𝐴))) |