Step | Hyp | Ref
| Expression |
1 | | mplbas2.s |
. . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
2 | | mplbas2.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
3 | | mplbas2.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
4 | 1, 2, 3 | psrassa 19414 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ AssAlg) |
5 | | mplbas2.p |
. . . . . 6
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
6 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑃) =
(Base‘𝑃) |
7 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
8 | 5, 1, 6, 7 | mplbasss 19432 |
. . . . 5
⊢
(Base‘𝑃)
⊆ (Base‘𝑆) |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → (Base‘𝑃) ⊆ (Base‘𝑆)) |
10 | | mplbas2.v |
. . . . . . . 8
⊢ 𝑉 = (𝐼 mVar 𝑅) |
11 | | crngring 18558 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
12 | 3, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
13 | 1, 10, 7, 2, 12 | mvrf 19424 |
. . . . . . 7
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑆)) |
14 | 13 | ffnd 6046 |
. . . . . 6
⊢ (𝜑 → 𝑉 Fn 𝐼) |
15 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
16 | 12 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
17 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
18 | 5, 10, 6, 15, 16, 17 | mvrcl 19449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ (Base‘𝑃)) |
19 | 18 | ralrimiva 2966 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃)) |
20 | | ffnfv 6388 |
. . . . . 6
⊢ (𝑉:𝐼⟶(Base‘𝑃) ↔ (𝑉 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃))) |
21 | 14, 19, 20 | sylanbrc 698 |
. . . . 5
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑃)) |
22 | | frn 6053 |
. . . . 5
⊢ (𝑉:𝐼⟶(Base‘𝑃) → ran 𝑉 ⊆ (Base‘𝑃)) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑃)) |
24 | | mplbas2.a |
. . . . 5
⊢ 𝐴 = (AlgSpan‘𝑆) |
25 | 24, 7 | aspss 19332 |
. . . 4
⊢ ((𝑆 ∈ AssAlg ∧
(Base‘𝑃) ⊆
(Base‘𝑆) ∧ ran
𝑉 ⊆ (Base‘𝑃)) → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃))) |
26 | 4, 9, 23, 25 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃))) |
27 | 1, 5, 6, 2, 12 | mplsubrg 19440 |
. . . 4
⊢ (𝜑 → (Base‘𝑃) ∈ (SubRing‘𝑆)) |
28 | 1, 5, 6, 2, 12 | mpllss 19438 |
. . . 4
⊢ (𝜑 → (Base‘𝑃) ∈ (LSubSp‘𝑆)) |
29 | | eqid 2622 |
. . . . 5
⊢
(LSubSp‘𝑆) =
(LSubSp‘𝑆) |
30 | 24, 7, 29 | aspid 19330 |
. . . 4
⊢ ((𝑆 ∈ AssAlg ∧
(Base‘𝑃) ∈
(SubRing‘𝑆) ∧
(Base‘𝑃) ∈
(LSubSp‘𝑆)) →
(𝐴‘(Base‘𝑃)) = (Base‘𝑃)) |
31 | 4, 27, 28, 30 | syl3anc 1326 |
. . 3
⊢ (𝜑 → (𝐴‘(Base‘𝑃)) = (Base‘𝑃)) |
32 | 26, 31 | sseqtrd 3641 |
. 2
⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)) |
33 | | eqid 2622 |
. . . . . 6
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
34 | | eqid 2622 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
35 | | eqid 2622 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
36 | 2 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝐼 ∈ 𝑊) |
37 | | eqid 2622 |
. . . . . 6
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
38 | 12 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 ∈ Ring) |
39 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (Base‘𝑃)) |
40 | 5, 33, 34, 35, 36, 6, 37, 38, 39 | mplcoe1 19465 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))))) |
41 | | eqid 2622 |
. . . . . 6
⊢
(0g‘𝑃) = (0g‘𝑃) |
42 | 5 | mplring 19452 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring) |
43 | 2, 12, 42 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ Ring) |
44 | | ringabl 18580 |
. . . . . . . 8
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Abel) |
45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ Abel) |
46 | 45 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑃 ∈ Abel) |
47 | | ovex 6678 |
. . . . . . . 8
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
48 | 47 | rabex 4813 |
. . . . . . 7
⊢ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V |
49 | 48 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
50 | 23, 8 | syl6ss 3615 |
. . . . . . . . . 10
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑆)) |
51 | 24, 7 | aspsubrg 19331 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆)) |
52 | 4, 50, 51 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆)) |
53 | 5, 1, 6 | mplval2 19431 |
. . . . . . . . . . 11
⊢ 𝑃 = (𝑆 ↾s (Base‘𝑃)) |
54 | 53 | subsubrg 18806 |
. . . . . . . . . 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 957 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃)) |
57 | | subrgsubg 18786 |
. . . . . . . 8
⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃)) |
58 | 56, 57 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃)) |
59 | 58 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃)) |
60 | 5 | mpllmod 19451 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod) |
61 | 2, 12, 60 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ LMod) |
62 | 61 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑃 ∈ LMod) |
63 | 24, 7, 29 | asplss 19329 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆)) |
64 | 4, 50, 63 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆)) |
65 | 1, 2, 12 | psrlmod 19401 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ LMod) |
66 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(LSubSp‘𝑃) =
(LSubSp‘𝑃) |
67 | 53, 29, 66 | lsslss 18961 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ LMod ∧
(Base‘𝑃) ∈
(LSubSp‘𝑆)) →
((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)))) |
68 | 65, 28, 67 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)))) |
69 | 64, 32, 68 | mpbir2and 957 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) |
70 | 69 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) |
71 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
72 | 5, 71, 6, 33, 39 | mplelf 19433 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥:{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
73 | 72 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘𝑅)) |
74 | 5, 36, 38 | mplsca 19445 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 = (Scalar‘𝑃)) |
75 | 74 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 = (Scalar‘𝑃)) |
76 | 75 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
77 | 73, 76 | eleqtrd 2703 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃))) |
78 | 2 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝐼 ∈ 𝑊) |
79 | | eqid 2622 |
. . . . . . . . . 10
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
80 | | eqid 2622 |
. . . . . . . . . 10
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
81 | 3 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ CRing) |
82 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
83 | 5, 33, 34, 35, 78, 79, 80, 10, 81, 82 | mplcoe2 19469 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) = ((mulGrp‘𝑃) Σg (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))))) |
84 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(1r‘𝑃) = (1r‘𝑃) |
85 | 79, 84 | ringidval 18503 |
. . . . . . . . . 10
⊢
(1r‘𝑃) = (0g‘(mulGrp‘𝑃)) |
86 | 5 | mplcrng 19453 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ CRing) |
87 | 2, 3, 86 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ CRing) |
88 | 79 | crngmgp 18555 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ CRing →
(mulGrp‘𝑃) ∈
CMnd) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (mulGrp‘𝑃) ∈ CMnd) |
90 | 89 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(mulGrp‘𝑃) ∈
CMnd) |
91 | 56 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃)) |
92 | 79 | subrgsubm 18793 |
. . . . . . . . . . 11
⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃))) |
93 | 91, 92 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃))) |
94 | | simplll 798 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → 𝜑) |
95 | 33 | psrbag 19364 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ 𝑊 → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈
Fin))) |
96 | 36, 95 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈
Fin))) |
97 | 96 | biimpa 501 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈
Fin)) |
98 | 97 | simpld 475 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑘:𝐼⟶ℕ0) |
99 | 98 | ffvelrnda 6359 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑘‘𝑧) ∈
ℕ0) |
100 | 24, 7 | aspssid 19333 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → ran 𝑉 ⊆ (𝐴‘ran 𝑉)) |
101 | 4, 50, 100 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑉 ⊆ (𝐴‘ran 𝑉)) |
102 | 101 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ran 𝑉 ⊆ (𝐴‘ran 𝑉)) |
103 | 14 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑉 Fn 𝐼) |
104 | | fnfvelrn 6356 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 Fn 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉) |
105 | 103, 104 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉) |
106 | 102, 105 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉)) |
107 | 79, 6 | mgpbas 18495 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
108 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑃) = (.r‘𝑃) |
109 | 79, 108 | mgpplusg 18493 |
. . . . . . . . . . . . 13
⊢
(.r‘𝑃) = (+g‘(mulGrp‘𝑃)) |
110 | 108 | subrgmcl 18792 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉)) |
111 | 56, 110 | syl3an1 1359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉)) |
112 | 84 | subrg1cl 18788 |
. . . . . . . . . . . . . 14
⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (1r‘𝑃) ∈ (𝐴‘ran 𝑉)) |
113 | 56, 112 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1r‘𝑃) ∈ (𝐴‘ran 𝑉)) |
114 | 107, 80, 109, 89, 32, 111, 85, 113 | mulgnn0subcl 17554 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑘‘𝑧) ∈ ℕ0 ∧ (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉)) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉)) |
115 | 94, 99, 106, 114 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉)) |
116 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) = (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) |
117 | 115, 116 | fmptd 6385 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))):𝐼⟶(𝐴‘ran 𝑉)) |
118 | | mptexg 6484 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈ 𝑊 → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V) |
119 | 2, 118 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V) |
120 | 119 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V) |
121 | | funmpt 5926 |
. . . . . . . . . . . 12
⊢ Fun
(𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) |
122 | 121 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → Fun
(𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))) |
123 | | fvexd 6203 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(1r‘𝑃)
∈ V) |
124 | 97 | simprd 479 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (◡𝑘 “ ℕ) ∈
Fin) |
125 | | elrabi 3359 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} → 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) |
126 | | elmapi 7879 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (ℕ0
↑𝑚 𝐼) → 𝑘:𝐼⟶ℕ0) |
127 | 126 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) → 𝑘:𝐼⟶ℕ0) |
128 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) → 𝐼 ∈ 𝑊) |
129 | | frnnn0supp 11349 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘:𝐼⟶ℕ0) → (𝑘 supp 0) = (◡𝑘 “ ℕ)) |
130 | 128, 127,
129 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) → (𝑘 supp 0) = (◡𝑘 “ ℕ)) |
131 | | eqimss 3657 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 supp 0) = (◡𝑘 “ ℕ) → (𝑘 supp 0) ⊆ (◡𝑘 “ ℕ)) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) → (𝑘 supp 0) ⊆ (◡𝑘 “ ℕ)) |
133 | | c0ex 10034 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) → 0 ∈ V) |
135 | 127, 132,
128, 134 | suppssr 7326 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑𝑚 𝐼)) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0) |
136 | 125, 135 | sylanl2 683 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0) |
137 | 136 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) =
(0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) |
138 | 2 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝐼 ∈ 𝑊) |
139 | 12 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝑅 ∈ Ring) |
140 | | eldifi 3732 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ)) → 𝑧 ∈ 𝐼) |
141 | 140 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝑧 ∈ 𝐼) |
142 | 5, 10, 6, 138, 139, 141 | mvrcl 19449 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑉‘𝑧) ∈ (Base‘𝑃)) |
143 | 107, 85, 80 | mulg0 17546 |
. . . . . . . . . . . . . 14
⊢ ((𝑉‘𝑧) ∈ (Base‘𝑃) →
(0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃)) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) →
(0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃)) |
145 | 137, 144 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃)) |
146 | 145, 78 | suppss2 7329 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1r‘𝑃)) ⊆ (◡𝑘 “ ℕ)) |
147 | | suppssfifsupp 8290 |
. . . . . . . . . . 11
⊢ ((((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V ∧ Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∧ (1r‘𝑃) ∈ V) ∧ ((◡𝑘 “ ℕ) ∈ Fin ∧ ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1r‘𝑃)) ⊆ (◡𝑘 “ ℕ))) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1r‘𝑃)) |
148 | 120, 122,
123, 124, 146, 147 | syl32anc 1334 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1r‘𝑃)) |
149 | 85, 90, 78, 93, 117, 148 | gsumsubmcl 18319 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
((mulGrp‘𝑃)
Σg (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))) ∈ (𝐴‘ran 𝑉)) |
150 | 83, 149 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (𝐴‘ran 𝑉)) |
151 | | eqid 2622 |
. . . . . . . . 9
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
152 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
153 | 151, 37, 152, 66 | lssvscl 18955 |
. . . . . . . 8
⊢ (((𝑃 ∈ LMod ∧ (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) ∧ ((𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (𝐴‘ran 𝑉))) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) ∈ (𝐴‘ran 𝑉)) |
154 | 62, 70, 77, 150, 153 | syl22anc 1327 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) ∈ (𝐴‘ran 𝑉)) |
155 | | eqid 2622 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) = (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) |
156 | 154, 155 | fmptd 6385 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))):{𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶(𝐴‘ran 𝑉)) |
157 | 47 | mptrabex 6488 |
. . . . . . . . 9
⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V |
158 | | funmpt 5926 |
. . . . . . . . 9
⊢ Fun
(𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) |
159 | | fvex 6201 |
. . . . . . . . 9
⊢
(0g‘𝑃) ∈ V |
160 | 157, 158,
159 | 3pm3.2i 1239 |
. . . . . . . 8
⊢ ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V) |
161 | 160 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V)) |
162 | 5, 1, 7, 34, 6 | mplelbas 19430 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (Base‘𝑃) ↔ (𝑥 ∈ (Base‘𝑆) ∧ 𝑥 finSupp (0g‘𝑅))) |
163 | 162 | simprbi 480 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Base‘𝑃) → 𝑥 finSupp (0g‘𝑅)) |
164 | 163 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 finSupp (0g‘𝑅)) |
165 | 164 | fsuppimpd 8282 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g‘𝑅)) ∈ Fin) |
166 | | ssid 3624 |
. . . . . . . . . . . . 13
⊢ (𝑥 supp (0g‘𝑅)) ⊆ (𝑥 supp (0g‘𝑅)) |
167 | 166 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g‘𝑅)) ⊆ (𝑥 supp (0g‘𝑅))) |
168 | | fvexd 6203 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0g‘𝑅) ∈ V) |
169 | 72, 167, 49, 168 | suppssr 7326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (𝑥‘𝑘) = (0g‘𝑅)) |
170 | 74 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
171 | 170 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) →
(0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
172 | 169, 171 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (𝑥‘𝑘) = (0g‘(Scalar‘𝑃))) |
173 | 172 | oveq1d 6665 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) =
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) |
174 | | eldifi 3732 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅))) → 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin}) |
175 | 12 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ Ring) |
176 | 5, 6, 34, 35, 33, 78, 175, 82 | mplmon 19463 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘𝑃)) |
177 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) |
178 | 6, 151, 37, 177, 41 | lmod0vs 18896 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ LMod ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘𝑃)) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
179 | 62, 176, 178 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
180 | 174, 179 | sylan2 491 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
181 | 173, 180 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
182 | 181, 49 | suppss2 7329 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) supp (0g‘𝑃)) ⊆ (𝑥 supp (0g‘𝑅))) |
183 | | suppssfifsupp 8290 |
. . . . . . 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‘𝑃)) |
184 | 161, 165,
182, 183 | syl12anc 1324 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) finSupp (0g‘𝑃)) |
185 | 41, 46, 49, 59, 156, 184 | gsumsubgcl 18320 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))) ∈ (𝐴‘ran 𝑉)) |
186 | 40, 185 | eqeltrd 2701 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (𝐴‘ran 𝑉)) |
187 | 186 | ex 450 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑃) → 𝑥 ∈ (𝐴‘ran 𝑉))) |
188 | 187 | ssrdv 3609 |
. 2
⊢ (𝜑 → (Base‘𝑃) ⊆ (𝐴‘ran 𝑉)) |
189 | 32, 188 | eqssd 3620 |
1
⊢ (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃)) |