Step | Hyp | Ref
| Expression |
1 | | selvval2lem4.u |
. . . . . . . 8
⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) |
2 | | selvval2lem4.t |
. . . . . . . 8
⊢ 𝑇 = (𝐽 mPoly 𝑈) |
3 | | selvval2lem4.c |
. . . . . . . 8
⊢ 𝐶 = (algSc‘𝑇) |
4 | | selvval2lem4.d |
. . . . . . . 8
⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈)) |
5 | | selvval2lem4.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
6 | | difexg 5231 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑉 → (𝐼 ∖ 𝐽) ∈ V) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 ∖ 𝐽) ∈ V) |
8 | | selvval2lem4.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ⊆ 𝐼) |
9 | 5, 8 | ssexd 5228 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ V) |
10 | | selvval2lem4.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ CRing) |
11 | 1, 2, 3, 4, 7, 9, 10 | selvval2lem2 39182 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇)) |
12 | | eqid 2821 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
13 | | eqid 2821 |
. . . . . . . 8
⊢
(Base‘𝑇) =
(Base‘𝑇) |
14 | 12, 13 | rhmf 19478 |
. . . . . . 7
⊢ (𝐷 ∈ (𝑅 RingHom 𝑇) → 𝐷:(Base‘𝑅)⟶(Base‘𝑇)) |
15 | | ffrn 6526 |
. . . . . . 7
⊢ (𝐷:(Base‘𝑅)⟶(Base‘𝑇) → 𝐷:(Base‘𝑅)⟶ran 𝐷) |
16 | 11, 14, 15 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝐷:(Base‘𝑅)⟶ran 𝐷) |
17 | 1, 2, 3, 4, 7, 9, 10 | selvval2lem3 39183 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐷 ∈ (SubRing‘𝑇)) |
18 | 13 | subrgss 19536 |
. . . . . . . 8
⊢ (ran
𝐷 ∈
(SubRing‘𝑇) →
ran 𝐷 ⊆
(Base‘𝑇)) |
19 | | selvval2lem4.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑇 ↾s ran 𝐷) |
20 | 19, 13 | ressbas2 16555 |
. . . . . . . 8
⊢ (ran
𝐷 ⊆ (Base‘𝑇) → ran 𝐷 = (Base‘𝑆)) |
21 | 17, 18, 20 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ran 𝐷 = (Base‘𝑆)) |
22 | 21 | feq3d 6501 |
. . . . . 6
⊢ (𝜑 → (𝐷:(Base‘𝑅)⟶ran 𝐷 ↔ 𝐷:(Base‘𝑅)⟶(Base‘𝑆))) |
23 | 16, 22 | mpbid 234 |
. . . . 5
⊢ (𝜑 → 𝐷:(Base‘𝑅)⟶(Base‘𝑆)) |
24 | | selvval2lem4.p |
. . . . . 6
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
25 | | selvval2lem4.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑃) |
26 | | eqid 2821 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
27 | | selvval2lem4.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
28 | 24, 12, 25, 26, 27 | mplelf 20213 |
. . . . 5
⊢ (𝜑 → 𝐹:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
29 | 23, 28 | fcod 6532 |
. . . 4
⊢ (𝜑 → (𝐷 ∘ 𝐹):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑆)) |
30 | | fvexd 6685 |
. . . . 5
⊢ (𝜑 → (Base‘𝑆) ∈ V) |
31 | | ovex 7189 |
. . . . . . 7
⊢
(ℕ0 ↑m 𝐼) ∈ V |
32 | 31 | rabex 5235 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V |
33 | 32 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
34 | 30, 33 | elmapd 8420 |
. . . 4
⊢ (𝜑 → ((𝐷 ∘ 𝐹) ∈ ((Base‘𝑆) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ↔ (𝐷 ∘ 𝐹):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑆))) |
35 | 29, 34 | mpbird 259 |
. . 3
⊢ (𝜑 → (𝐷 ∘ 𝐹) ∈ ((Base‘𝑆) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin})) |
36 | | eqid 2821 |
. . . 4
⊢ (𝐼 mPwSer 𝑆) = (𝐼 mPwSer 𝑆) |
37 | | eqid 2821 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
38 | | eqid 2821 |
. . . 4
⊢
(Base‘(𝐼
mPwSer 𝑆)) =
(Base‘(𝐼 mPwSer 𝑆)) |
39 | 36, 37, 26, 38, 5 | psrbas 20158 |
. . 3
⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑆)) = ((Base‘𝑆) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin})) |
40 | 35, 39 | eleqtrrd 2916 |
. 2
⊢ (𝜑 → (𝐷 ∘ 𝐹) ∈ (Base‘(𝐼 mPwSer 𝑆))) |
41 | | fvexd 6685 |
. . 3
⊢ (𝜑 → (0g‘𝑆) ∈ V) |
42 | | crngring 19308 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
43 | | eqid 2821 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
44 | 12, 43 | ring0cl 19319 |
. . . 4
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
45 | 10, 42, 44 | 3syl 18 |
. . 3
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅)) |
46 | | ssidd 3990 |
. . 3
⊢ (𝜑 → (Base‘𝑅) ⊆ (Base‘𝑅)) |
47 | | fvexd 6685 |
. . 3
⊢ (𝜑 → (Base‘𝑅) ∈ V) |
48 | 24, 25, 43, 27, 10 | mplelsfi 20271 |
. . 3
⊢ (𝜑 → 𝐹 finSupp (0g‘𝑅)) |
49 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐷 = (𝐶 ∘ (algSc‘𝑈))) |
50 | 49 | fveq1d 6672 |
. . . 4
⊢ (𝜑 → (𝐷‘(0g‘𝑅)) = ((𝐶 ∘ (algSc‘𝑈))‘(0g‘𝑅))) |
51 | | eqid 2821 |
. . . . . 6
⊢
(Base‘𝑈) =
(Base‘𝑈) |
52 | | eqid 2821 |
. . . . . 6
⊢
(algSc‘𝑈) =
(algSc‘𝑈) |
53 | 10, 42 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) |
54 | 1, 51, 12, 52, 7, 53 | mplasclf 20277 |
. . . . 5
⊢ (𝜑 → (algSc‘𝑈):(Base‘𝑅)⟶(Base‘𝑈)) |
55 | 54, 45 | fvco3d 6761 |
. . . 4
⊢ (𝜑 → ((𝐶 ∘ (algSc‘𝑈))‘(0g‘𝑅)) = (𝐶‘((algSc‘𝑈)‘(0g‘𝑅)))) |
56 | 1, 7, 10 | mplsca 20225 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 = (Scalar‘𝑈)) |
57 | 56 | fveq2d 6674 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) =
(0g‘(Scalar‘𝑈))) |
58 | 57 | fveq2d 6674 |
. . . . . . 7
⊢ (𝜑 → ((algSc‘𝑈)‘(0g‘𝑅)) = ((algSc‘𝑈)‘(0g‘(Scalar‘𝑈)))) |
59 | | eqid 2821 |
. . . . . . . 8
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
60 | 1 | mplassa 20235 |
. . . . . . . . . 10
⊢ (((𝐼 ∖ 𝐽) ∈ V ∧ 𝑅 ∈ CRing) → 𝑈 ∈ AssAlg) |
61 | 7, 10, 60 | syl2anc 586 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ AssAlg) |
62 | | assalmod 20092 |
. . . . . . . . 9
⊢ (𝑈 ∈ AssAlg → 𝑈 ∈ LMod) |
63 | 61, 62 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
64 | | assaring 20093 |
. . . . . . . . 9
⊢ (𝑈 ∈ AssAlg → 𝑈 ∈ Ring) |
65 | 61, 64 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ Ring) |
66 | 52, 59, 63, 65 | ascl0 20113 |
. . . . . . 7
⊢ (𝜑 → ((algSc‘𝑈)‘(0g‘(Scalar‘𝑈))) = (0g‘𝑈)) |
67 | 58, 66 | eqtrd 2856 |
. . . . . 6
⊢ (𝜑 → ((algSc‘𝑈)‘(0g‘𝑅)) = (0g‘𝑈)) |
68 | 67 | fveq2d 6674 |
. . . . 5
⊢ (𝜑 → (𝐶‘((algSc‘𝑈)‘(0g‘𝑅))) = (𝐶‘(0g‘𝑈))) |
69 | 2, 9, 61 | mplsca 20225 |
. . . . . . 7
⊢ (𝜑 → 𝑈 = (Scalar‘𝑇)) |
70 | 69 | fveq2d 6674 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑈) =
(0g‘(Scalar‘𝑇))) |
71 | 70 | fveq2d 6674 |
. . . . 5
⊢ (𝜑 → (𝐶‘(0g‘𝑈)) = (𝐶‘(0g‘(Scalar‘𝑇)))) |
72 | | eqid 2821 |
. . . . . . 7
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) |
73 | 1, 2, 7, 9, 10 | selvval2lem1 39181 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ AssAlg) |
74 | | assalmod 20092 |
. . . . . . . 8
⊢ (𝑇 ∈ AssAlg → 𝑇 ∈ LMod) |
75 | 73, 74 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ LMod) |
76 | | assaring 20093 |
. . . . . . . 8
⊢ (𝑇 ∈ AssAlg → 𝑇 ∈ Ring) |
77 | 73, 76 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ Ring) |
78 | 3, 72, 75, 77 | ascl0 20113 |
. . . . . 6
⊢ (𝜑 → (𝐶‘(0g‘(Scalar‘𝑇))) = (0g‘𝑇)) |
79 | | subrgsubg 19541 |
. . . . . . 7
⊢ (ran
𝐷 ∈
(SubRing‘𝑇) →
ran 𝐷 ∈
(SubGrp‘𝑇)) |
80 | | eqid 2821 |
. . . . . . . 8
⊢
(0g‘𝑇) = (0g‘𝑇) |
81 | 19, 80 | subg0 18285 |
. . . . . . 7
⊢ (ran
𝐷 ∈
(SubGrp‘𝑇) →
(0g‘𝑇) =
(0g‘𝑆)) |
82 | 17, 79, 81 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑇) = (0g‘𝑆)) |
83 | 78, 82 | eqtrd 2856 |
. . . . 5
⊢ (𝜑 → (𝐶‘(0g‘(Scalar‘𝑇))) = (0g‘𝑆)) |
84 | 68, 71, 83 | 3eqtrd 2860 |
. . . 4
⊢ (𝜑 → (𝐶‘((algSc‘𝑈)‘(0g‘𝑅))) = (0g‘𝑆)) |
85 | 50, 55, 84 | 3eqtrd 2860 |
. . 3
⊢ (𝜑 → (𝐷‘(0g‘𝑅)) = (0g‘𝑆)) |
86 | 41, 45, 28, 16, 46, 33, 47, 48, 85 | fsuppcor 8867 |
. 2
⊢ (𝜑 → (𝐷 ∘ 𝐹) finSupp (0g‘𝑆)) |
87 | | selvval2lem4.w |
. . 3
⊢ 𝑊 = (𝐼 mPoly 𝑆) |
88 | | eqid 2821 |
. . 3
⊢
(0g‘𝑆) = (0g‘𝑆) |
89 | | selvval2lem4.x |
. . 3
⊢ 𝑋 = (Base‘𝑊) |
90 | 87, 36, 38, 88, 89 | mplelbas 20210 |
. 2
⊢ ((𝐷 ∘ 𝐹) ∈ 𝑋 ↔ ((𝐷 ∘ 𝐹) ∈ (Base‘(𝐼 mPwSer 𝑆)) ∧ (𝐷 ∘ 𝐹) finSupp (0g‘𝑆))) |
91 | 40, 86, 90 | sylanbrc 585 |
1
⊢ (𝜑 → (𝐷 ∘ 𝐹) ∈ 𝑋) |