Step | Hyp | Ref
| Expression |
1 | | mplbas2.s |
. . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | mplbas2.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
3 | | mplbas2.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
4 | 1, 2, 3 | psrassa 19235 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ AssAlg) |
5 | | mplbas2.p |
. . . . . 6
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
6 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑃) =
(Base‘𝑃) |
7 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
8 | 5, 1, 6, 7 | mplbasss 19253 |
. . . . 5
⊢
(Base‘𝑃)
⊆ (Base‘𝑆) |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → (Base‘𝑃) ⊆ (Base‘𝑆)) |
10 | | mplbas2.v |
. . . . . . . 8
⊢ 𝑉 = (𝐼 mVar 𝑅) |
11 | | crngring 18381 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
12 | 3, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
13 | 1, 10, 7, 2, 12 | mvrf 19245 |
. . . . . . 7
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑆)) |
14 | 13 | ffnd 5959 |
. . . . . 6
⊢ (𝜑 → 𝑉 Fn 𝐼) |
15 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
16 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
17 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
18 | 5, 10, 6, 15, 16, 17 | mvrcl 19270 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ (Base‘𝑃)) |
19 | 18 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃)) |
20 | | ffnfv 6295 |
. . . . . 6
⊢ (𝑉:𝐼⟶(Base‘𝑃) ↔ (𝑉 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃))) |
21 | 14, 19, 20 | sylanbrc 695 |
. . . . 5
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑃)) |
22 | | frn 5966 |
. . . . 5
⊢ (𝑉:𝐼⟶(Base‘𝑃) → ran 𝑉 ⊆ (Base‘𝑃)) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑃)) |
24 | | mplbas2.a |
. . . . 5
⊢ 𝐴 = (AlgSpan‘𝑆) |
25 | 24, 7 | aspss 19153 |
. . . 4
⊢ ((𝑆 ∈ AssAlg ∧
(Base‘𝑃) ⊆
(Base‘𝑆) ∧ ran
𝑉 ⊆ (Base‘𝑃)) → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃))) |
26 | 4, 9, 23, 25 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃))) |
27 | 1, 5, 6, 2, 12 | mplsubrg 19261 |
. . . 4
⊢ (𝜑 → (Base‘𝑃) ∈ (SubRing‘𝑆)) |
28 | 1, 5, 6, 2, 12 | mpllss 19259 |
. . . 4
⊢ (𝜑 → (Base‘𝑃) ∈ (LSubSp‘𝑆)) |
29 | | eqid 2610 |
. . . . 5
⊢
(LSubSp‘𝑆) =
(LSubSp‘𝑆) |
30 | 24, 7, 29 | aspid 19151 |
. . . 4
⊢ ((𝑆 ∈ AssAlg ∧
(Base‘𝑃) ∈
(SubRing‘𝑆) ∧
(Base‘𝑃) ∈
(LSubSp‘𝑆)) →
(𝐴‘(Base‘𝑃)) = (Base‘𝑃)) |
31 | 4, 27, 28, 30 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐴‘(Base‘𝑃)) = (Base‘𝑃)) |
32 | 26, 31 | sseqtrd 3604 |
. 2
⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)) |
33 | | eqid 2610 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
34 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
35 | | eqid 2610 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
36 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝐼 ∈ 𝑊) |
37 | | eqid 2610 |
. . . . . 6
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
38 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 ∈ Ring) |
39 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (Base‘𝑃)) |
40 | 5, 33, 34, 35, 36, 6, 37, 38, 39 | mplcoe1 19286 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))))) |
41 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝑃) = (0g‘𝑃) |
42 | 5 | mplring 19273 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) |
43 | 2, 12, 42 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ Ring) |
44 | | ringabl 18403 |
. . . . . . . 8
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Abel) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ Abel) |
46 | 45 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑃 ∈ Abel) |
47 | | ovex 6577 |
. . . . . . . 8
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
48 | 47 | rabex 4740 |
. . . . . . 7
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V |
49 | 48 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
50 | 23, 8 | syl6ss 3580 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑆)) |
51 | 24, 7 | aspsubrg 19152 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆)) |
52 | 4, 50, 51 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆)) |
53 | 5, 1, 6 | mplval2 19252 |
. . . . . . . . . . 11
⊢ 𝑃 = (𝑆 ↾s (Base‘𝑃)) |
54 | 53 | subsubrg 18629 |
. . . . . . . . . 10
⊢
((Base‘𝑃)
∈ (SubRing‘𝑆)
→ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)))) |
55 | 27, 54 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)))) |
56 | 52, 32, 55 | mpbir2and 959 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃)) |
57 | | subrgsubg 18609 |
. . . . . . . 8
⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃)) |
58 | 56, 57 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃)) |
59 | 58 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃)) |
60 | 5 | mpllmod 19272 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod) |
61 | 2, 12, 60 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ LMod) |
62 | 61 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑃 ∈ LMod) |
63 | 24, 7, 29 | asplss 19150 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆)) |
64 | 4, 50, 63 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆)) |
65 | 1, 2, 12 | psrlmod 19222 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ LMod) |
66 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(LSubSp‘𝑃) =
(LSubSp‘𝑃) |
67 | 53, 29, 66 | lsslss 18782 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ LMod ∧
(Base‘𝑃) ∈
(LSubSp‘𝑆)) →
((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)))) |
68 | 65, 28, 67 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)))) |
69 | 64, 32, 68 | mpbir2and 959 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) |
70 | 69 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) |
71 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
72 | 5, 71, 6, 33, 39 | mplelf 19254 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
73 | 72 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘𝑅)) |
74 | 5, 36, 38 | mplsca 19266 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 = (Scalar‘𝑃)) |
75 | 74 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 = (Scalar‘𝑃)) |
76 | 75 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
77 | 73, 76 | eleqtrd 2690 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃))) |
78 | 2 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝐼 ∈ 𝑊) |
79 | | eqid 2610 |
. . . . . . . . . 10
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
80 | | eqid 2610 |
. . . . . . . . . 10
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
81 | 3 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ CRing) |
82 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
83 | 5, 33, 34, 35, 78, 79, 80, 10, 81, 82 | mplcoe2 19290 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) = ((mulGrp‘𝑃) Σg (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))))) |
84 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(1r‘𝑃) = (1r‘𝑃) |
85 | 79, 84 | ringidval 18326 |
. . . . . . . . . 10
⊢
(1r‘𝑃) = (0g‘(mulGrp‘𝑃)) |
86 | 5 | mplcrng 19274 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ CRing) |
87 | 2, 3, 86 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ CRing) |
88 | 79 | crngmgp 18378 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ CRing →
(mulGrp‘𝑃) ∈
CMnd) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (mulGrp‘𝑃) ∈ CMnd) |
90 | 89 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(mulGrp‘𝑃) ∈
CMnd) |
91 | 56 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃)) |
92 | 79 | subrgsubm 18616 |
. . . . . . . . . . 11
⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃))) |
93 | 91, 92 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃))) |
94 | | simplll 794 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → 𝜑) |
95 | 33 | psrbag 19185 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ 𝑊 → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈
Fin))) |
96 | 36, 95 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈
Fin))) |
97 | 96 | biimpa 500 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈
Fin)) |
98 | 97 | simpld 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑘:𝐼⟶ℕ0) |
99 | 98 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑘‘𝑧) ∈
ℕ0) |
100 | 24, 7 | aspssid 19154 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → ran 𝑉 ⊆ (𝐴‘ran 𝑉)) |
101 | 4, 50, 100 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑉 ⊆ (𝐴‘ran 𝑉)) |
102 | 101 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ran 𝑉 ⊆ (𝐴‘ran 𝑉)) |
103 | 14 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑉 Fn 𝐼) |
104 | | fnfvelrn 6264 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 Fn 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉) |
105 | 103, 104 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉) |
106 | 102, 105 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉)) |
107 | 79, 6 | mgpbas 18318 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
108 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑃) = (.r‘𝑃) |
109 | 79, 108 | mgpplusg 18316 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑃) = (+g‘(mulGrp‘𝑃)) |
110 | 108 | subrgmcl 18615 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉)) |
111 | 56, 110 | syl3an1 1351 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉)) |
112 | 84 | subrg1cl 18611 |
. . . . . . . . . . . . . 14
⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (1r‘𝑃) ∈ (𝐴‘ran 𝑉)) |
113 | 56, 112 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1r‘𝑃) ∈ (𝐴‘ran 𝑉)) |
114 | 107, 80, 109, 89, 32, 111, 85, 113 | mulgnn0subcl 17377 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘‘𝑧) ∈ ℕ0 ∧ (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉)) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉)) |
115 | 94, 99, 106, 114 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉)) |
116 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) = (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) |
117 | 115, 116 | fmptd 6292 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))):𝐼⟶(𝐴‘ran 𝑉)) |
118 | | mptexg 6389 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ 𝑊 → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V) |
119 | 2, 118 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V) |
120 | 119 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V) |
121 | | funmpt 5840 |
. . . . . . . . . . . 12
⊢ Fun
(𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) |
122 | 121 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → Fun
(𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))) |
123 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(1r‘𝑃) ∈ V |
124 | 123 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(1r‘𝑃)
∈ V) |
125 | 97 | simprd 478 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (◡𝑘 “ ℕ) ∈
Fin) |
126 | | elrabi 3328 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} → 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) |
127 | | elmapi 7765 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (ℕ0
↑𝑚 𝐼) → 𝑘:𝐼⟶ℕ0) |
128 | 127 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) → 𝑘:𝐼⟶ℕ0) |
129 | 2 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) → 𝐼 ∈ 𝑊) |
130 | | frnnn0supp 11226 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘:𝐼⟶ℕ0) → (𝑘 supp 0) = (◡𝑘 “ ℕ)) |
131 | 129, 128,
130 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) → (𝑘 supp 0) = (◡𝑘 “ ℕ)) |
132 | | eqimss 3620 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 supp 0) = (◡𝑘 “ ℕ) → (𝑘 supp 0) ⊆ (◡𝑘 “ ℕ)) |
133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) → (𝑘 supp 0) ⊆ (◡𝑘 “ ℕ)) |
134 | | c0ex 9913 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) → 0 ∈ V) |
136 | 128, 133,
129, 135 | suppssr 7213 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0) |
137 | 126, 136 | sylanl2 681 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0) |
138 | 137 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) =
(0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) |
139 | 2 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝐼 ∈ 𝑊) |
140 | 12 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝑅 ∈ Ring) |
141 | | eldifi 3694 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ)) → 𝑧 ∈ 𝐼) |
142 | 141 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝑧 ∈ 𝐼) |
143 | 5, 10, 6, 139, 140, 142 | mvrcl 19270 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑉‘𝑧) ∈ (Base‘𝑃)) |
144 | 107, 85, 80 | mulg0 17369 |
. . . . . . . . . . . . . 14
⊢ ((𝑉‘𝑧) ∈ (Base‘𝑃) →
(0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃)) |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) →
(0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃)) |
146 | 138, 145 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃)) |
147 | 146, 78 | suppss2 7216 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1r‘𝑃)) ⊆ (◡𝑘 “ ℕ)) |
148 | | suppssfifsupp 8173 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V ∧ Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∧ (1r‘𝑃) ∈ V) ∧ ((◡𝑘 “ ℕ) ∈ Fin ∧ ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1r‘𝑃)) ⊆ (◡𝑘 “ ℕ))) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1r‘𝑃)) |
149 | 120, 122,
124, 125, 147, 148 | syl32anc 1326 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1r‘𝑃)) |
150 | 85, 90, 78, 93, 117, 149 | gsumsubmcl 18142 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
((mulGrp‘𝑃)
Σg (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))) ∈ (𝐴‘ran 𝑉)) |
151 | 83, 150 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (𝐴‘ran 𝑉)) |
152 | | eqid 2610 |
. . . . . . . . 9
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
153 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
154 | 152, 37, 153, 66 | lssvscl 18776 |
. . . . . . . 8
⊢ (((𝑃 ∈ LMod ∧ (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) ∧ ((𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (𝐴‘ran 𝑉))) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) ∈ (𝐴‘ran 𝑉)) |
155 | 62, 70, 77, 151, 154 | syl22anc 1319 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) ∈ (𝐴‘ran 𝑉)) |
156 | | eqid 2610 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) |
157 | 155, 156 | fmptd 6292 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))):{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶(𝐴‘ran 𝑉)) |
158 | 47 | mptrabex 6392 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V |
159 | | funmpt 5840 |
. . . . . . . . 9
⊢ Fun
(𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) |
160 | | fvex 6113 |
. . . . . . . . 9
⊢
(0g‘𝑃) ∈ V |
161 | 158, 159,
160 | 3pm3.2i 1232 |
. . . . . . . 8
⊢ ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V) |
162 | 161 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V)) |
163 | 5, 1, 7, 34, 6 | mplelbas 19251 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (Base‘𝑃) ↔ (𝑥 ∈ (Base‘𝑆) ∧ 𝑥 finSupp (0g‘𝑅))) |
164 | 163 | simprbi 479 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Base‘𝑃) → 𝑥 finSupp (0g‘𝑅)) |
165 | 164 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 finSupp (0g‘𝑅)) |
166 | 165 | fsuppimpd 8165 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g‘𝑅)) ∈ Fin) |
167 | | ssid 3587 |
. . . . . . . . . . . . 13
⊢ (𝑥 supp (0g‘𝑅)) ⊆ (𝑥 supp (0g‘𝑅)) |
168 | 167 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g‘𝑅)) ⊆ (𝑥 supp (0g‘𝑅))) |
169 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) ∈ V |
170 | 169 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0g‘𝑅) ∈ V) |
171 | 72, 168, 49, 170 | suppssr 7213 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (𝑥‘𝑘) = (0g‘𝑅)) |
172 | 74 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
173 | 172 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) →
(0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
174 | 171, 173 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (𝑥‘𝑘) = (0g‘(Scalar‘𝑃))) |
175 | 174 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) =
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) |
176 | | eldifi 3694 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅))) → 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
177 | 12 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ Ring) |
178 | 5, 6, 34, 35, 33, 78, 177, 82 | mplmon 19284 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘𝑃)) |
179 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) |
180 | 6, 152, 37, 179, 41 | lmod0vs 18719 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ LMod ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘𝑃)) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
181 | 62, 178, 180 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
182 | 176, 181 | sylan2 490 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
183 | 175, 182 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
184 | 183, 49 | suppss2 7216 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) supp (0g‘𝑃)) ⊆ (𝑥 supp (0g‘𝑅))) |
185 | | suppssfifsupp 8173 |
. . . . . . 7
⊢ ((((𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V) ∧ ((𝑥 supp (0g‘𝑅)) ∈ Fin ∧ ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) supp (0g‘𝑃)) ⊆ (𝑥 supp (0g‘𝑅)))) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) finSupp (0g‘𝑃)) |
186 | 162, 166,
184, 185 | syl12anc 1316 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) finSupp (0g‘𝑃)) |
187 | 41, 46, 49, 59, 157, 186 | gsumsubgcl 18143 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))) ∈ (𝐴‘ran 𝑉)) |
188 | 40, 187 | eqeltrd 2688 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (𝐴‘ran 𝑉)) |
189 | 188 | ex 449 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑃) → 𝑥 ∈ (𝐴‘ran 𝑉))) |
190 | 189 | ssrdv 3574 |
. 2
⊢ (𝜑 → (Base‘𝑃) ⊆ (𝐴‘ran 𝑉)) |
191 | 32, 190 | eqssd 3585 |
1
⊢ (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃)) |