| Step | Hyp | Ref
| Expression |
| 1 | | mplbas2.s |
. . . . 5
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
| 2 | | mplbas2.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
| 3 | | mplbas2.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 4 | 1, 2, 3 | psrassa 21993 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ AssAlg) |
| 5 | | mplbas2.p |
. . . . . 6
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
| 6 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 7 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 8 | 5, 1, 6, 7 | mplbasss 22017 |
. . . . 5
⊢
(Base‘𝑃)
⊆ (Base‘𝑆) |
| 9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → (Base‘𝑃) ⊆ (Base‘𝑆)) |
| 10 | | mplbas2.v |
. . . . . . . 8
⊢ 𝑉 = (𝐼 mVar 𝑅) |
| 11 | | crngring 20242 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
| 12 | 3, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 13 | 1, 10, 7, 2, 12 | mvrf 22005 |
. . . . . . 7
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑆)) |
| 14 | 13 | ffnd 6737 |
. . . . . 6
⊢ (𝜑 → 𝑉 Fn 𝐼) |
| 15 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
| 16 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
| 17 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
| 18 | 5, 10, 6, 15, 16, 17 | mvrcl 22012 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ (Base‘𝑃)) |
| 19 | 18 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃)) |
| 20 | | ffnfv 7139 |
. . . . . 6
⊢ (𝑉:𝐼⟶(Base‘𝑃) ↔ (𝑉 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃))) |
| 21 | 14, 19, 20 | sylanbrc 583 |
. . . . 5
⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑃)) |
| 22 | 21 | frnd 6744 |
. . . 4
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑃)) |
| 23 | | mplbas2.a |
. . . . 5
⊢ 𝐴 = (AlgSpan‘𝑆) |
| 24 | 23, 7 | aspss 21897 |
. . . 4
⊢ ((𝑆 ∈ AssAlg ∧
(Base‘𝑃) ⊆
(Base‘𝑆) ∧ ran
𝑉 ⊆ (Base‘𝑃)) → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃))) |
| 25 | 4, 9, 22, 24 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃))) |
| 26 | 1, 5, 6, 2, 12 | mplsubrg 22025 |
. . . 4
⊢ (𝜑 → (Base‘𝑃) ∈ (SubRing‘𝑆)) |
| 27 | 1, 5, 6, 2, 12 | mpllss 22023 |
. . . 4
⊢ (𝜑 → (Base‘𝑃) ∈ (LSubSp‘𝑆)) |
| 28 | | eqid 2737 |
. . . . 5
⊢
(LSubSp‘𝑆) =
(LSubSp‘𝑆) |
| 29 | 23, 7, 28 | aspid 21895 |
. . . 4
⊢ ((𝑆 ∈ AssAlg ∧
(Base‘𝑃) ∈
(SubRing‘𝑆) ∧
(Base‘𝑃) ∈
(LSubSp‘𝑆)) →
(𝐴‘(Base‘𝑃)) = (Base‘𝑃)) |
| 30 | 4, 26, 27, 29 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝐴‘(Base‘𝑃)) = (Base‘𝑃)) |
| 31 | 25, 30 | sseqtrd 4020 |
. 2
⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)) |
| 32 | | eqid 2737 |
. . . 4
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 33 | | eqid 2737 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 34 | | eqid 2737 |
. . . 4
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 35 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝐼 ∈ 𝑊) |
| 36 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
| 37 | 12 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 ∈ Ring) |
| 38 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (Base‘𝑃)) |
| 39 | 5, 32, 33, 34, 35, 6, 36, 37, 38 | mplcoe1 22055 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))))) |
| 40 | | eqid 2737 |
. . . 4
⊢
(0g‘𝑃) = (0g‘𝑃) |
| 41 | 5, 2, 12 | mplringd 22043 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ Ring) |
| 42 | | ringabl 20278 |
. . . . . 6
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Abel) |
| 43 | 41, 42 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ Abel) |
| 44 | 43 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑃 ∈ Abel) |
| 45 | | ovex 7464 |
. . . . . 6
⊢
(ℕ0 ↑m 𝐼) ∈ V |
| 46 | 45 | rabex 5339 |
. . . . 5
⊢ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V |
| 47 | 46 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∈
V) |
| 48 | 13 | frnd 6744 |
. . . . . . . 8
⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑆)) |
| 49 | 23, 7 | aspsubrg 21896 |
. . . . . . . 8
⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆)) |
| 50 | 4, 48, 49 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆)) |
| 51 | 5, 1, 6 | mplval2 22016 |
. . . . . . . . 9
⊢ 𝑃 = (𝑆 ↾s (Base‘𝑃)) |
| 52 | 51 | subsubrg 20598 |
. . . . . . . 8
⊢
((Base‘𝑃)
∈ (SubRing‘𝑆)
→ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)))) |
| 53 | 26, 52 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)))) |
| 54 | 50, 31, 53 | mpbir2and 713 |
. . . . . 6
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃)) |
| 55 | | subrgsubg 20577 |
. . . . . 6
⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃)) |
| 56 | 54, 55 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃)) |
| 57 | 56 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃)) |
| 58 | 5, 2, 12 | mpllmodd 22044 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ LMod) |
| 59 | 58 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑃 ∈ LMod) |
| 60 | 23, 7, 28 | asplss 21894 |
. . . . . . . . 9
⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆)) |
| 61 | 4, 48, 60 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆)) |
| 62 | 1, 2, 12 | psrlmod 21980 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ LMod) |
| 63 | | eqid 2737 |
. . . . . . . . . 10
⊢
(LSubSp‘𝑃) =
(LSubSp‘𝑃) |
| 64 | 51, 28, 63 | lsslss 20959 |
. . . . . . . . 9
⊢ ((𝑆 ∈ LMod ∧
(Base‘𝑃) ∈
(LSubSp‘𝑆)) →
((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)))) |
| 65 | 62, 27, 64 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃)))) |
| 66 | 61, 31, 65 | mpbir2and 713 |
. . . . . . 7
⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) |
| 67 | 66 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) |
| 68 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 69 | 5, 68, 6, 32, 38 | mplelf 22018 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥:{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
| 70 | 69 | ffvelcdmda 7104 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘𝑅)) |
| 71 | 5, 35, 37 | mplsca 22033 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 = (Scalar‘𝑃)) |
| 72 | 71 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 = (Scalar‘𝑃)) |
| 73 | 72 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
| 74 | 70, 73 | eleqtrd 2843 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃))) |
| 75 | 2 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝐼 ∈ 𝑊) |
| 76 | | eqid 2737 |
. . . . . . . 8
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
| 77 | | eqid 2737 |
. . . . . . . 8
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
| 78 | 3 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ CRing) |
| 79 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}) |
| 80 | 5, 32, 33, 34, 75, 76, 77, 10, 78, 79 | mplcoe2 22059 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) = ((mulGrp‘𝑃) Σg (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))))) |
| 81 | | eqid 2737 |
. . . . . . . . 9
⊢
(1r‘𝑃) = (1r‘𝑃) |
| 82 | 76, 81 | ringidval 20180 |
. . . . . . . 8
⊢
(1r‘𝑃) = (0g‘(mulGrp‘𝑃)) |
| 83 | 5 | mplcrng 22041 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ CRing) |
| 84 | 2, 3, 83 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ CRing) |
| 85 | 76 | crngmgp 20238 |
. . . . . . . . . 10
⊢ (𝑃 ∈ CRing →
(mulGrp‘𝑃) ∈
CMnd) |
| 86 | 84, 85 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (mulGrp‘𝑃) ∈ CMnd) |
| 87 | 86 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(mulGrp‘𝑃) ∈
CMnd) |
| 88 | 54 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃)) |
| 89 | 76 | subrgsubm 20585 |
. . . . . . . . 9
⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃))) |
| 90 | 88, 89 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃))) |
| 91 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → 𝜑) |
| 92 | 32 | psrbag 21937 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ 𝑊 → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈
Fin))) |
| 93 | 35, 92 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈
Fin))) |
| 94 | 93 | biimpa 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈
Fin)) |
| 95 | 94 | simpld 494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑘:𝐼⟶ℕ0) |
| 96 | 95 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑘‘𝑧) ∈
ℕ0) |
| 97 | 23, 7 | aspssid 21898 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → ran 𝑉 ⊆ (𝐴‘ran 𝑉)) |
| 98 | 4, 48, 97 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝑉 ⊆ (𝐴‘ran 𝑉)) |
| 99 | 98 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ran 𝑉 ⊆ (𝐴‘ran 𝑉)) |
| 100 | 14 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑉 Fn 𝐼) |
| 101 | | fnfvelrn 7100 |
. . . . . . . . . . . 12
⊢ ((𝑉 Fn 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉) |
| 102 | 100, 101 | sylan 580 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉) |
| 103 | 99, 102 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉)) |
| 104 | 76, 6 | mgpbas 20142 |
. . . . . . . . . . 11
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
| 105 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 106 | 76, 105 | mgpplusg 20141 |
. . . . . . . . . . 11
⊢
(.r‘𝑃) = (+g‘(mulGrp‘𝑃)) |
| 107 | 105 | subrgmcl 20584 |
. . . . . . . . . . . 12
⊢ (((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉)) |
| 108 | 54, 107 | syl3an1 1164 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉)) |
| 109 | 81 | subrg1cl 20580 |
. . . . . . . . . . . 12
⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (1r‘𝑃) ∈ (𝐴‘ran 𝑉)) |
| 110 | 54, 109 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (1r‘𝑃) ∈ (𝐴‘ran 𝑉)) |
| 111 | 104, 77, 106, 86, 31, 108, 82, 110 | mulgnn0subcl 19105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘‘𝑧) ∈ ℕ0 ∧ (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉)) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉)) |
| 112 | 91, 96, 103, 111 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉)) |
| 113 | 112 | fmpttd 7135 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))):𝐼⟶(𝐴‘ran 𝑉)) |
| 114 | 2 | mptexd 7244 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V) |
| 115 | 114 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V) |
| 116 | | funmpt 6604 |
. . . . . . . . . 10
⊢ Fun
(𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) |
| 117 | 116 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → Fun
(𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))) |
| 118 | | fvexd 6921 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) →
(1r‘𝑃)
∈ V) |
| 119 | 94 | simprd 495 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (◡𝑘 “ ℕ) ∈
Fin) |
| 120 | | elrabi 3687 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} → 𝑘 ∈ (ℕ0
↑m 𝐼)) |
| 121 | | elmapi 8889 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (ℕ0
↑m 𝐼)
→ 𝑘:𝐼⟶ℕ0) |
| 122 | 121 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑m 𝐼))
→ 𝑘:𝐼⟶ℕ0) |
| 123 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑m 𝐼))
→ 𝐼 ∈ 𝑊) |
| 124 | | fcdmnn0supp 12583 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘:𝐼⟶ℕ0) → (𝑘 supp 0) = (◡𝑘 “ ℕ)) |
| 125 | 123, 122,
124 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑m 𝐼))
→ (𝑘 supp 0) = (◡𝑘 “ ℕ)) |
| 126 | | eqimss 4042 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 supp 0) = (◡𝑘 “ ℕ) → (𝑘 supp 0) ⊆ (◡𝑘 “ ℕ)) |
| 127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑m 𝐼))
→ (𝑘 supp 0) ⊆
(◡𝑘 “ ℕ)) |
| 128 | | c0ex 11255 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
V |
| 129 | 128 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑m 𝐼))
→ 0 ∈ V) |
| 130 | 122, 127,
123, 129 | suppssr 8220 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0
↑m 𝐼))
∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0) |
| 131 | 120, 130 | sylanl2 681 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0) |
| 132 | 131 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) =
(0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) |
| 133 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝐼 ∈ 𝑊) |
| 134 | 12 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝑅 ∈ Ring) |
| 135 | | eldifi 4131 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ)) → 𝑧 ∈ 𝐼) |
| 136 | 135 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝑧 ∈ 𝐼) |
| 137 | 5, 10, 6, 133, 134, 136 | mvrcl 22012 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑉‘𝑧) ∈ (Base‘𝑃)) |
| 138 | 104, 82, 77 | mulg0 19092 |
. . . . . . . . . . . 12
⊢ ((𝑉‘𝑧) ∈ (Base‘𝑃) →
(0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃)) |
| 139 | 137, 138 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) →
(0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃)) |
| 140 | 132, 139 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃)) |
| 141 | 140, 75 | suppss2 8225 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1r‘𝑃)) ⊆ (◡𝑘 “ ℕ)) |
| 142 | | suppssfifsupp 9420 |
. . . . . . . . 9
⊢ ((((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V ∧ Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∧ (1r‘𝑃) ∈ V) ∧ ((◡𝑘 “ ℕ) ∈ Fin ∧ ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1r‘𝑃)) ⊆ (◡𝑘 “ ℕ))) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1r‘𝑃)) |
| 143 | 115, 117,
118, 119, 141, 142 | syl32anc 1380 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1r‘𝑃)) |
| 144 | 82, 87, 75, 90, 113, 143 | gsumsubmcl 19937 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) →
((mulGrp‘𝑃)
Σg (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))) ∈ (𝐴‘ran 𝑉)) |
| 145 | 80, 144 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (𝐴‘ran 𝑉)) |
| 146 | | eqid 2737 |
. . . . . . 7
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
| 147 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
| 148 | 146, 36, 147, 63 | lssvscl 20953 |
. . . . . 6
⊢ (((𝑃 ∈ LMod ∧ (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) ∧ ((𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (𝐴‘ran 𝑉))) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) ∈ (𝐴‘ran 𝑉)) |
| 149 | 59, 67, 74, 145, 148 | syl22anc 839 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) ∈ (𝐴‘ran 𝑉)) |
| 150 | 149 | fmpttd 7135 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))):{𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}⟶(𝐴‘ran 𝑉)) |
| 151 | 45 | mptrabex 7245 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V |
| 152 | | funmpt 6604 |
. . . . . . 7
⊢ Fun
(𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) |
| 153 | | fvex 6919 |
. . . . . . 7
⊢
(0g‘𝑃) ∈ V |
| 154 | 151, 152,
153 | 3pm3.2i 1340 |
. . . . . 6
⊢ ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V) |
| 155 | 154 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V)) |
| 156 | 5, 1, 7, 33, 6 | mplelbas 22011 |
. . . . . . . 8
⊢ (𝑥 ∈ (Base‘𝑃) ↔ (𝑥 ∈ (Base‘𝑆) ∧ 𝑥 finSupp (0g‘𝑅))) |
| 157 | 156 | simprbi 496 |
. . . . . . 7
⊢ (𝑥 ∈ (Base‘𝑃) → 𝑥 finSupp (0g‘𝑅)) |
| 158 | 157 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 finSupp (0g‘𝑅)) |
| 159 | 158 | fsuppimpd 9409 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g‘𝑅)) ∈ Fin) |
| 160 | | ssidd 4007 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g‘𝑅)) ⊆ (𝑥 supp (0g‘𝑅))) |
| 161 | | fvexd 6921 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0g‘𝑅) ∈ V) |
| 162 | 69, 160, 47, 161 | suppssr 8220 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (𝑥‘𝑘) = (0g‘𝑅)) |
| 163 | 71 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
| 164 | 163 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) →
(0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
| 165 | 162, 164 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (𝑥‘𝑘) = (0g‘(Scalar‘𝑃))) |
| 166 | 165 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) =
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) |
| 167 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝑘 ∈ ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅))) → 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin}) |
| 168 | 12 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ Ring) |
| 169 | 5, 6, 33, 34, 32, 75, 168, 79 | mplmon 22053 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘𝑃)) |
| 170 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) |
| 171 | 6, 146, 36, 170, 40 | lmod0vs 20893 |
. . . . . . . . 9
⊢ ((𝑃 ∈ LMod ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘𝑃)) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
| 172 | 59, 169, 171 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin}) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
| 173 | 167, 172 | sylan2 593 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
| 174 | 166, 173 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃)) |
| 175 | 174, 47 | suppss2 8225 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) supp (0g‘𝑃)) ⊆ (𝑥 supp (0g‘𝑅))) |
| 176 | | suppssfifsupp 9420 |
. . . . 5
⊢ ((((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V) ∧ ((𝑥 supp (0g‘𝑅)) ∈ Fin ∧ ((𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) supp (0g‘𝑃)) ⊆ (𝑥 supp (0g‘𝑅)))) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) finSupp (0g‘𝑃)) |
| 177 | 155, 159,
175, 176 | syl12anc 837 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) finSupp (0g‘𝑃)) |
| 178 | 40, 44, 47, 57, 150, 177 | gsumsubgcl 19938 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠
‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈ Fin} ↦
if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))) ∈ (𝐴‘ran 𝑉)) |
| 179 | 39, 178 | eqeltrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (𝐴‘ran 𝑉)) |
| 180 | 31, 179 | eqelssd 4005 |
1
⊢ (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃)) |