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 | 5 | difexd 5257 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 ∖ 𝐽) ∈ V) |
7 | | selvval2lem4.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ⊆ 𝐼) |
8 | 5, 7 | ssexd 5252 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ V) |
9 | | selvval2lem4.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ CRing) |
10 | 1, 2, 3, 4, 6, 8, 9 | selvval2lem2 40220 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (𝑅 RingHom 𝑇)) |
11 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
12 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘𝑇) =
(Base‘𝑇) |
13 | 11, 12 | rhmf 19966 |
. . . . . . 7
⊢ (𝐷 ∈ (𝑅 RingHom 𝑇) → 𝐷:(Base‘𝑅)⟶(Base‘𝑇)) |
14 | | ffrn 6611 |
. . . . . . 7
⊢ (𝐷:(Base‘𝑅)⟶(Base‘𝑇) → 𝐷:(Base‘𝑅)⟶ran 𝐷) |
15 | 10, 13, 14 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝐷:(Base‘𝑅)⟶ran 𝐷) |
16 | 1, 2, 3, 4, 6, 8, 9 | selvval2lem3 40221 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐷 ∈ (SubRing‘𝑇)) |
17 | 12 | subrgss 20021 |
. . . . . . . 8
⊢ (ran
𝐷 ∈
(SubRing‘𝑇) →
ran 𝐷 ⊆
(Base‘𝑇)) |
18 | | selvval2lem4.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑇 ↾s ran 𝐷) |
19 | 18, 12 | ressbas2 16945 |
. . . . . . . 8
⊢ (ran
𝐷 ⊆ (Base‘𝑇) → ran 𝐷 = (Base‘𝑆)) |
20 | 16, 17, 19 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ran 𝐷 = (Base‘𝑆)) |
21 | 20 | feq3d 6584 |
. . . . . 6
⊢ (𝜑 → (𝐷:(Base‘𝑅)⟶ran 𝐷 ↔ 𝐷:(Base‘𝑅)⟶(Base‘𝑆))) |
22 | 15, 21 | mpbid 231 |
. . . . 5
⊢ (𝜑 → 𝐷:(Base‘𝑅)⟶(Base‘𝑆)) |
23 | | selvval2lem4.p |
. . . . . 6
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
24 | | selvval2lem4.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑃) |
25 | | eqid 2740 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
26 | | selvval2lem4.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
27 | 23, 11, 24, 25, 26 | mplelf 21200 |
. . . . 5
⊢ (𝜑 → 𝐹:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
28 | 22, 27 | fcod 6623 |
. . . 4
⊢ (𝜑 → (𝐷 ∘ 𝐹):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑆)) |
29 | | fvexd 6784 |
. . . . 5
⊢ (𝜑 → (Base‘𝑆) ∈ V) |
30 | | ovex 7302 |
. . . . . . 7
⊢
(ℕ0 ↑m 𝐼) ∈ V |
31 | 30 | rabex 5260 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V |
32 | 31 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
33 | 29, 32 | elmapd 8610 |
. . . 4
⊢ (𝜑 → ((𝐷 ∘ 𝐹) ∈ ((Base‘𝑆) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ↔ (𝐷 ∘ 𝐹):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑆))) |
34 | 28, 33 | mpbird 256 |
. . 3
⊢ (𝜑 → (𝐷 ∘ 𝐹) ∈ ((Base‘𝑆) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin})) |
35 | | eqid 2740 |
. . . 4
⊢ (𝐼 mPwSer 𝑆) = (𝐼 mPwSer 𝑆) |
36 | | eqid 2740 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
37 | | eqid 2740 |
. . . 4
⊢
(Base‘(𝐼
mPwSer 𝑆)) =
(Base‘(𝐼 mPwSer 𝑆)) |
38 | 35, 36, 25, 37, 5 | psrbas 21143 |
. . 3
⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑆)) = ((Base‘𝑆) ↑m {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin})) |
39 | 34, 38 | eleqtrrd 2844 |
. 2
⊢ (𝜑 → (𝐷 ∘ 𝐹) ∈ (Base‘(𝐼 mPwSer 𝑆))) |
40 | | fvexd 6784 |
. . 3
⊢ (𝜑 → (0g‘𝑆) ∈ V) |
41 | | crngring 19791 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
42 | | eqid 2740 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
43 | 11, 42 | ring0cl 19804 |
. . . 4
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
44 | 9, 41, 43 | 3syl 18 |
. . 3
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅)) |
45 | | ssidd 3949 |
. . 3
⊢ (𝜑 → (Base‘𝑅) ⊆ (Base‘𝑅)) |
46 | | fvexd 6784 |
. . 3
⊢ (𝜑 → (Base‘𝑅) ∈ V) |
47 | 23, 24, 42, 26, 9 | mplelsfi 21197 |
. . 3
⊢ (𝜑 → 𝐹 finSupp (0g‘𝑅)) |
48 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐷 = (𝐶 ∘ (algSc‘𝑈))) |
49 | 48 | fveq1d 6771 |
. . . 4
⊢ (𝜑 → (𝐷‘(0g‘𝑅)) = ((𝐶 ∘ (algSc‘𝑈))‘(0g‘𝑅))) |
50 | | eqid 2740 |
. . . . . 6
⊢
(Base‘𝑈) =
(Base‘𝑈) |
51 | | eqid 2740 |
. . . . . 6
⊢
(algSc‘𝑈) =
(algSc‘𝑈) |
52 | 9, 41 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) |
53 | 1, 50, 11, 51, 6, 52 | mplasclf 21269 |
. . . . 5
⊢ (𝜑 → (algSc‘𝑈):(Base‘𝑅)⟶(Base‘𝑈)) |
54 | 53, 44 | fvco3d 6863 |
. . . 4
⊢ (𝜑 → ((𝐶 ∘ (algSc‘𝑈))‘(0g‘𝑅)) = (𝐶‘((algSc‘𝑈)‘(0g‘𝑅)))) |
55 | 1, 6, 9 | mplsca 21213 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 = (Scalar‘𝑈)) |
56 | 55 | fveq2d 6773 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) =
(0g‘(Scalar‘𝑈))) |
57 | 56 | fveq2d 6773 |
. . . . . . 7
⊢ (𝜑 → ((algSc‘𝑈)‘(0g‘𝑅)) = ((algSc‘𝑈)‘(0g‘(Scalar‘𝑈)))) |
58 | | eqid 2740 |
. . . . . . . 8
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
59 | 1 | mplassa 21223 |
. . . . . . . . . 10
⊢ (((𝐼 ∖ 𝐽) ∈ V ∧ 𝑅 ∈ CRing) → 𝑈 ∈ AssAlg) |
60 | 6, 9, 59 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ AssAlg) |
61 | | assalmod 21063 |
. . . . . . . . 9
⊢ (𝑈 ∈ AssAlg → 𝑈 ∈ LMod) |
62 | 60, 61 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LMod) |
63 | | assaring 21064 |
. . . . . . . . 9
⊢ (𝑈 ∈ AssAlg → 𝑈 ∈ Ring) |
64 | 60, 63 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ Ring) |
65 | 51, 58, 62, 64 | ascl0 21084 |
. . . . . . 7
⊢ (𝜑 → ((algSc‘𝑈)‘(0g‘(Scalar‘𝑈))) = (0g‘𝑈)) |
66 | 57, 65 | eqtrd 2780 |
. . . . . 6
⊢ (𝜑 → ((algSc‘𝑈)‘(0g‘𝑅)) = (0g‘𝑈)) |
67 | 66 | fveq2d 6773 |
. . . . 5
⊢ (𝜑 → (𝐶‘((algSc‘𝑈)‘(0g‘𝑅))) = (𝐶‘(0g‘𝑈))) |
68 | 2, 8, 60 | mplsca 21213 |
. . . . . . 7
⊢ (𝜑 → 𝑈 = (Scalar‘𝑇)) |
69 | 68 | fveq2d 6773 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑈) =
(0g‘(Scalar‘𝑇))) |
70 | 69 | fveq2d 6773 |
. . . . 5
⊢ (𝜑 → (𝐶‘(0g‘𝑈)) = (𝐶‘(0g‘(Scalar‘𝑇)))) |
71 | | eqid 2740 |
. . . . . . 7
⊢
(Scalar‘𝑇) =
(Scalar‘𝑇) |
72 | 1, 2, 6, 8, 9 | selvval2lem1 40219 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ AssAlg) |
73 | | assalmod 21063 |
. . . . . . . 8
⊢ (𝑇 ∈ AssAlg → 𝑇 ∈ LMod) |
74 | 72, 73 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ LMod) |
75 | | assaring 21064 |
. . . . . . . 8
⊢ (𝑇 ∈ AssAlg → 𝑇 ∈ Ring) |
76 | 72, 75 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ Ring) |
77 | 3, 71, 74, 76 | ascl0 21084 |
. . . . . 6
⊢ (𝜑 → (𝐶‘(0g‘(Scalar‘𝑇))) = (0g‘𝑇)) |
78 | | subrgsubg 20026 |
. . . . . . 7
⊢ (ran
𝐷 ∈
(SubRing‘𝑇) →
ran 𝐷 ∈
(SubGrp‘𝑇)) |
79 | | eqid 2740 |
. . . . . . . 8
⊢
(0g‘𝑇) = (0g‘𝑇) |
80 | 18, 79 | subg0 18757 |
. . . . . . 7
⊢ (ran
𝐷 ∈
(SubGrp‘𝑇) →
(0g‘𝑇) =
(0g‘𝑆)) |
81 | 16, 78, 80 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑇) = (0g‘𝑆)) |
82 | 77, 81 | eqtrd 2780 |
. . . . 5
⊢ (𝜑 → (𝐶‘(0g‘(Scalar‘𝑇))) = (0g‘𝑆)) |
83 | 67, 70, 82 | 3eqtrd 2784 |
. . . 4
⊢ (𝜑 → (𝐶‘((algSc‘𝑈)‘(0g‘𝑅))) = (0g‘𝑆)) |
84 | 49, 54, 83 | 3eqtrd 2784 |
. . 3
⊢ (𝜑 → (𝐷‘(0g‘𝑅)) = (0g‘𝑆)) |
85 | 40, 44, 27, 15, 45, 32, 46, 47, 84 | fsuppcor 9139 |
. 2
⊢ (𝜑 → (𝐷 ∘ 𝐹) finSupp (0g‘𝑆)) |
86 | | selvval2lem4.w |
. . 3
⊢ 𝑊 = (𝐼 mPoly 𝑆) |
87 | | eqid 2740 |
. . 3
⊢
(0g‘𝑆) = (0g‘𝑆) |
88 | | selvval2lem4.x |
. . 3
⊢ 𝑋 = (Base‘𝑊) |
89 | 86, 35, 37, 87, 88 | mplelbas 21195 |
. 2
⊢ ((𝐷 ∘ 𝐹) ∈ 𝑋 ↔ ((𝐷 ∘ 𝐹) ∈ (Base‘(𝐼 mPwSer 𝑆)) ∧ (𝐷 ∘ 𝐹) finSupp (0g‘𝑆))) |
90 | 39, 85, 89 | sylanbrc 583 |
1
⊢ (𝜑 → (𝐷 ∘ 𝐹) ∈ 𝑋) |