MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mplbas2 Structured version   Visualization version   GIF version

Theorem mplbas2 22077
Description: An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 10-Jan-2015.)
Hypotheses
Ref Expression
mplbas2.p 𝑃 = (𝐼 mPoly 𝑅)
mplbas2.s 𝑆 = (𝐼 mPwSer 𝑅)
mplbas2.v 𝑉 = (𝐼 mVar 𝑅)
mplbas2.a 𝐴 = (AlgSpan‘𝑆)
mplbas2.i (𝜑𝐼𝑊)
mplbas2.r (𝜑𝑅 ∈ CRing)
Assertion
Ref Expression
mplbas2 (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃))

Proof of Theorem mplbas2
Dummy variables 𝑢 𝑘 𝑣 𝑥 𝑧 𝑦 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplbas2.s . . . . 5 𝑆 = (𝐼 mPwSer 𝑅)
2 mplbas2.i . . . . 5 (𝜑𝐼𝑊)
3 mplbas2.r . . . . 5 (𝜑𝑅 ∈ CRing)
41, 2, 3psrassa 22010 . . . 4 (𝜑𝑆 ∈ AssAlg)
5 mplbas2.p . . . . . 6 𝑃 = (𝐼 mPoly 𝑅)
6 eqid 2734 . . . . . 6 (Base‘𝑃) = (Base‘𝑃)
7 eqid 2734 . . . . . 6 (Base‘𝑆) = (Base‘𝑆)
85, 1, 6, 7mplbasss 22034 . . . . 5 (Base‘𝑃) ⊆ (Base‘𝑆)
98a1i 11 . . . 4 (𝜑 → (Base‘𝑃) ⊆ (Base‘𝑆))
10 mplbas2.v . . . . . . . 8 𝑉 = (𝐼 mVar 𝑅)
11 crngring 20262 . . . . . . . . 9 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
123, 11syl 17 . . . . . . . 8 (𝜑𝑅 ∈ Ring)
131, 10, 7, 2, 12mvrf 22022 . . . . . . 7 (𝜑𝑉:𝐼⟶(Base‘𝑆))
1413ffnd 6737 . . . . . 6 (𝜑𝑉 Fn 𝐼)
152adantr 480 . . . . . . . 8 ((𝜑𝑥𝐼) → 𝐼𝑊)
1612adantr 480 . . . . . . . 8 ((𝜑𝑥𝐼) → 𝑅 ∈ Ring)
17 simpr 484 . . . . . . . 8 ((𝜑𝑥𝐼) → 𝑥𝐼)
185, 10, 6, 15, 16, 17mvrcl 22029 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑉𝑥) ∈ (Base‘𝑃))
1918ralrimiva 3143 . . . . . 6 (𝜑 → ∀𝑥𝐼 (𝑉𝑥) ∈ (Base‘𝑃))
20 ffnfv 7138 . . . . . 6 (𝑉:𝐼⟶(Base‘𝑃) ↔ (𝑉 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑉𝑥) ∈ (Base‘𝑃)))
2114, 19, 20sylanbrc 583 . . . . 5 (𝜑𝑉:𝐼⟶(Base‘𝑃))
2221frnd 6744 . . . 4 (𝜑 → ran 𝑉 ⊆ (Base‘𝑃))
23 mplbas2.a . . . . 5 𝐴 = (AlgSpan‘𝑆)
2423, 7aspss 21914 . . . 4 ((𝑆 ∈ AssAlg ∧ (Base‘𝑃) ⊆ (Base‘𝑆) ∧ ran 𝑉 ⊆ (Base‘𝑃)) → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃)))
254, 9, 22, 24syl3anc 1370 . . 3 (𝜑 → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃)))
261, 5, 6, 2, 12mplsubrg 22042 . . . 4 (𝜑 → (Base‘𝑃) ∈ (SubRing‘𝑆))
271, 5, 6, 2, 12mpllss 22040 . . . 4 (𝜑 → (Base‘𝑃) ∈ (LSubSp‘𝑆))
28 eqid 2734 . . . . 5 (LSubSp‘𝑆) = (LSubSp‘𝑆)
2923, 7, 28aspid 21912 . . . 4 ((𝑆 ∈ AssAlg ∧ (Base‘𝑃) ∈ (SubRing‘𝑆) ∧ (Base‘𝑃) ∈ (LSubSp‘𝑆)) → (𝐴‘(Base‘𝑃)) = (Base‘𝑃))
304, 26, 27, 29syl3anc 1370 . . 3 (𝜑 → (𝐴‘(Base‘𝑃)) = (Base‘𝑃))
3125, 30sseqtrd 4035 . 2 (𝜑 → (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))
32 eqid 2734 . . . 4 {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
33 eqid 2734 . . . 4 (0g𝑅) = (0g𝑅)
34 eqid 2734 . . . 4 (1r𝑅) = (1r𝑅)
352adantr 480 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝐼𝑊)
36 eqid 2734 . . . 4 ( ·𝑠𝑃) = ( ·𝑠𝑃)
3712adantr 480 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑅 ∈ Ring)
38 simpr 484 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (Base‘𝑃))
395, 32, 33, 34, 35, 6, 36, 37, 38mplcoe1 22072 . . 3 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))))))
40 eqid 2734 . . . 4 (0g𝑃) = (0g𝑃)
415, 2, 12mplringd 22060 . . . . . 6 (𝜑𝑃 ∈ Ring)
42 ringabl 20294 . . . . . 6 (𝑃 ∈ Ring → 𝑃 ∈ Abel)
4341, 42syl 17 . . . . 5 (𝜑𝑃 ∈ Abel)
4443adantr 480 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑃 ∈ Abel)
45 ovex 7463 . . . . . 6 (ℕ0m 𝐼) ∈ V
4645rabex 5344 . . . . 5 {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∈ V
4746a1i 11 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑃)) → {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∈ V)
4813frnd 6744 . . . . . . . 8 (𝜑 → ran 𝑉 ⊆ (Base‘𝑆))
4923, 7aspsubrg 21913 . . . . . . . 8 ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆))
504, 48, 49syl2anc 584 . . . . . . 7 (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆))
515, 1, 6mplval2 22033 . . . . . . . . 9 𝑃 = (𝑆s (Base‘𝑃))
5251subsubrg 20614 . . . . . . . 8 ((Base‘𝑃) ∈ (SubRing‘𝑆) → ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
5326, 52syl 17 . . . . . . 7 (𝜑 → ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
5450, 31, 53mpbir2and 713 . . . . . 6 (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃))
55 subrgsubg 20593 . . . . . 6 ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
5654, 55syl 17 . . . . 5 (𝜑 → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
5756adantr 480 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
585, 2, 12mpllmodd 22061 . . . . . . 7 (𝜑𝑃 ∈ LMod)
5958ad2antrr 726 . . . . . 6 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑃 ∈ LMod)
6023, 7, 28asplss 21911 . . . . . . . . 9 ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆))
614, 48, 60syl2anc 584 . . . . . . . 8 (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆))
621, 2, 12psrlmod 21997 . . . . . . . . 9 (𝜑𝑆 ∈ LMod)
63 eqid 2734 . . . . . . . . . 10 (LSubSp‘𝑃) = (LSubSp‘𝑃)
6451, 28, 63lsslss 20976 . . . . . . . . 9 ((𝑆 ∈ LMod ∧ (Base‘𝑃) ∈ (LSubSp‘𝑆)) → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
6562, 27, 64syl2anc 584 . . . . . . . 8 (𝜑 → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
6661, 31, 65mpbir2and 713 . . . . . . 7 (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃))
6766ad2antrr 726 . . . . . 6 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃))
68 eqid 2734 . . . . . . . . 9 (Base‘𝑅) = (Base‘𝑅)
695, 68, 6, 32, 38mplelf 22035 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑥:{𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}⟶(Base‘𝑅))
7069ffvelcdmda 7103 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑥𝑘) ∈ (Base‘𝑅))
715, 35, 37mplsca 22050 . . . . . . . . 9 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑅 = (Scalar‘𝑃))
7271adantr 480 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑅 = (Scalar‘𝑃))
7372fveq2d 6910 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
7470, 73eleqtrd 2840 . . . . . 6 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑥𝑘) ∈ (Base‘(Scalar‘𝑃)))
752ad2antrr 726 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝐼𝑊)
76 eqid 2734 . . . . . . . 8 (mulGrp‘𝑃) = (mulGrp‘𝑃)
77 eqid 2734 . . . . . . . 8 (.g‘(mulGrp‘𝑃)) = (.g‘(mulGrp‘𝑃))
783ad2antrr 726 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ CRing)
79 simpr 484 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin})
805, 32, 33, 34, 75, 76, 77, 10, 78, 79mplcoe2 22076 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))) = ((mulGrp‘𝑃) Σg (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)))))
81 eqid 2734 . . . . . . . . 9 (1r𝑃) = (1r𝑃)
8276, 81ringidval 20200 . . . . . . . 8 (1r𝑃) = (0g‘(mulGrp‘𝑃))
835mplcrng 22058 . . . . . . . . . . 11 ((𝐼𝑊𝑅 ∈ CRing) → 𝑃 ∈ CRing)
842, 3, 83syl2anc 584 . . . . . . . . . 10 (𝜑𝑃 ∈ CRing)
8576crngmgp 20258 . . . . . . . . . 10 (𝑃 ∈ CRing → (mulGrp‘𝑃) ∈ CMnd)
8684, 85syl 17 . . . . . . . . 9 (𝜑 → (mulGrp‘𝑃) ∈ CMnd)
8786ad2antrr 726 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (mulGrp‘𝑃) ∈ CMnd)
8854ad2antrr 726 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃))
8976subrgsubm 20601 . . . . . . . . 9 ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃)))
9088, 89syl 17 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃)))
91 simplll 775 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → 𝜑)
9232psrbag 21954 . . . . . . . . . . . . . 14 (𝐼𝑊 → (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (𝑘 “ ℕ) ∈ Fin)))
9335, 92syl 17 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (𝑘 “ ℕ) ∈ Fin)))
9493biimpa 476 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑘:𝐼⟶ℕ0 ∧ (𝑘 “ ℕ) ∈ Fin))
9594simpld 494 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑘:𝐼⟶ℕ0)
9695ffvelcdmda 7103 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → (𝑘𝑧) ∈ ℕ0)
9723, 7aspssid 21915 . . . . . . . . . . . . 13 ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
984, 48, 97syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
9998ad3antrrr 730 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
10014ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑉 Fn 𝐼)
101 fnfvelrn 7099 . . . . . . . . . . . 12 ((𝑉 Fn 𝐼𝑧𝐼) → (𝑉𝑧) ∈ ran 𝑉)
102100, 101sylan 580 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → (𝑉𝑧) ∈ ran 𝑉)
10399, 102sseldd 3995 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → (𝑉𝑧) ∈ (𝐴‘ran 𝑉))
10476, 6mgpbas 20157 . . . . . . . . . . 11 (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
105 eqid 2734 . . . . . . . . . . . 12 (.r𝑃) = (.r𝑃)
10676, 105mgpplusg 20155 . . . . . . . . . . 11 (.r𝑃) = (+g‘(mulGrp‘𝑃))
107105subrgmcl 20600 . . . . . . . . . . . 12 (((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r𝑃)𝑣) ∈ (𝐴‘ran 𝑉))
10854, 107syl3an1 1162 . . . . . . . . . . 11 ((𝜑𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r𝑃)𝑣) ∈ (𝐴‘ran 𝑉))
10981subrg1cl 20596 . . . . . . . . . . . 12 ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (1r𝑃) ∈ (𝐴‘ran 𝑉))
11054, 109syl 17 . . . . . . . . . . 11 (𝜑 → (1r𝑃) ∈ (𝐴‘ran 𝑉))
111104, 77, 106, 86, 31, 108, 82, 110mulgnn0subcl 19117 . . . . . . . . . 10 ((𝜑 ∧ (𝑘𝑧) ∈ ℕ0 ∧ (𝑉𝑧) ∈ (𝐴‘ran 𝑉)) → ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)) ∈ (𝐴‘ran 𝑉))
11291, 96, 103, 111syl3anc 1370 . . . . . . . . 9 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)) ∈ (𝐴‘ran 𝑉))
113112fmpttd 7134 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))):𝐼⟶(𝐴‘ran 𝑉))
1142mptexd 7243 . . . . . . . . . 10 (𝜑 → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) ∈ V)
115114ad2antrr 726 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) ∈ V)
116 funmpt 6605 . . . . . . . . . 10 Fun (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)))
117116a1i 11 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → Fun (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))))
118 fvexd 6921 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (1r𝑃) ∈ V)
11994simprd 495 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑘 “ ℕ) ∈ Fin)
120 elrabi 3689 . . . . . . . . . . . . 13 (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} → 𝑘 ∈ (ℕ0m 𝐼))
121 elmapi 8887 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℕ0m 𝐼) → 𝑘:𝐼⟶ℕ0)
122121adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0m 𝐼)) → 𝑘:𝐼⟶ℕ0)
1232ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0m 𝐼)) → 𝐼𝑊)
124 fcdmnn0supp 12580 . . . . . . . . . . . . . . . 16 ((𝐼𝑊𝑘:𝐼⟶ℕ0) → (𝑘 supp 0) = (𝑘 “ ℕ))
125123, 122, 124syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0m 𝐼)) → (𝑘 supp 0) = (𝑘 “ ℕ))
126 eqimss 4053 . . . . . . . . . . . . . . 15 ((𝑘 supp 0) = (𝑘 “ ℕ) → (𝑘 supp 0) ⊆ (𝑘 “ ℕ))
127125, 126syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0m 𝐼)) → (𝑘 supp 0) ⊆ (𝑘 “ ℕ))
128 c0ex 11252 . . . . . . . . . . . . . . 15 0 ∈ V
129128a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0m 𝐼)) → 0 ∈ V)
130122, 127, 123, 129suppssr 8218 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0m 𝐼)) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → (𝑘𝑧) = 0)
131120, 130sylanl2 681 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → (𝑘𝑧) = 0)
132131oveq1d 7445 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)) = (0(.g‘(mulGrp‘𝑃))(𝑉𝑧)))
1332ad3antrrr 730 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → 𝐼𝑊)
13412ad3antrrr 730 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → 𝑅 ∈ Ring)
135 eldifi 4140 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ)) → 𝑧𝐼)
136135adantl 481 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → 𝑧𝐼)
1375, 10, 6, 133, 134, 136mvrcl 22029 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → (𝑉𝑧) ∈ (Base‘𝑃))
138104, 82, 77mulg0 19104 . . . . . . . . . . . 12 ((𝑉𝑧) ∈ (Base‘𝑃) → (0(.g‘(mulGrp‘𝑃))(𝑉𝑧)) = (1r𝑃))
139137, 138syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → (0(.g‘(mulGrp‘𝑃))(𝑉𝑧)) = (1r𝑃))
140132, 139eqtrd 2774 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)) = (1r𝑃))
141140, 75suppss2 8223 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → ((𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) supp (1r𝑃)) ⊆ (𝑘 “ ℕ))
142 suppssfifsupp 9417 . . . . . . . . 9 ((((𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) ∈ V ∧ Fun (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) ∧ (1r𝑃) ∈ V) ∧ ((𝑘 “ ℕ) ∈ Fin ∧ ((𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) supp (1r𝑃)) ⊆ (𝑘 “ ℕ))) → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) finSupp (1r𝑃))
143115, 117, 118, 119, 141, 142syl32anc 1377 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) finSupp (1r𝑃))
14482, 87, 75, 90, 113, 143gsumsubmcl 19951 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → ((mulGrp‘𝑃) Σg (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)))) ∈ (𝐴‘ran 𝑉))
14580, 144eqeltrd 2838 . . . . . 6 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))) ∈ (𝐴‘ran 𝑉))
146 eqid 2734 . . . . . . 7 (Scalar‘𝑃) = (Scalar‘𝑃)
147 eqid 2734 . . . . . . 7 (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
148146, 36, 147, 63lssvscl 20970 . . . . . 6 (((𝑃 ∈ LMod ∧ (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) ∧ ((𝑥𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))) ∈ (𝐴‘ran 𝑉))) → ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) ∈ (𝐴‘ran 𝑉))
14959, 67, 74, 145, 148syl22anc 839 . . . . 5 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) ∈ (𝐴‘ran 𝑉))
150149fmpttd 7134 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))):{𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}⟶(𝐴‘ran 𝑉))
15145mptrabex 7244 . . . . . . 7 (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∈ V
152 funmpt 6605 . . . . . . 7 Fun (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))))
153 fvex 6919 . . . . . . 7 (0g𝑃) ∈ V
154151, 152, 1533pm3.2i 1338 . . . . . 6 ((𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∧ (0g𝑃) ∈ V)
155154a1i 11 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∧ (0g𝑃) ∈ V))
1565, 1, 7, 33, 6mplelbas 22028 . . . . . . . 8 (𝑥 ∈ (Base‘𝑃) ↔ (𝑥 ∈ (Base‘𝑆) ∧ 𝑥 finSupp (0g𝑅)))
157156simprbi 496 . . . . . . 7 (𝑥 ∈ (Base‘𝑃) → 𝑥 finSupp (0g𝑅))
158157adantl 481 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑥 finSupp (0g𝑅))
159158fsuppimpd 9406 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g𝑅)) ∈ Fin)
160 ssidd 4018 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g𝑅)) ⊆ (𝑥 supp (0g𝑅)))
161 fvexd 6921 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝑃)) → (0g𝑅) ∈ V)
16269, 160, 47, 161suppssr 8218 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → (𝑥𝑘) = (0g𝑅))
16371fveq2d 6910 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝑃)) → (0g𝑅) = (0g‘(Scalar‘𝑃)))
164163adantr 480 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → (0g𝑅) = (0g‘(Scalar‘𝑃)))
165162, 164eqtrd 2774 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → (𝑥𝑘) = (0g‘(Scalar‘𝑃)))
166165oveq1d 7445 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) = ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))))
167 eldifi 4140 . . . . . . . 8 (𝑘 ∈ ({𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅))) → 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin})
16812ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ Ring)
1695, 6, 33, 34, 32, 75, 168, 79mplmon 22070 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))) ∈ (Base‘𝑃))
170 eqid 2734 . . . . . . . . . 10 (0g‘(Scalar‘𝑃)) = (0g‘(Scalar‘𝑃))
1716, 146, 36, 170, 40lmod0vs 20909 . . . . . . . . 9 ((𝑃 ∈ LMod ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))) ∈ (Base‘𝑃)) → ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) = (0g𝑃))
17259, 169, 171syl2anc 584 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) = (0g𝑃))
173167, 172sylan2 593 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) = (0g𝑃))
174166, 173eqtrd 2774 . . . . . 6 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) = (0g𝑃))
175174, 47suppss2 8223 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) supp (0g𝑃)) ⊆ (𝑥 supp (0g𝑅)))
176 suppssfifsupp 9417 . . . . 5 ((((𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∧ (0g𝑃) ∈ V) ∧ ((𝑥 supp (0g𝑅)) ∈ Fin ∧ ((𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) supp (0g𝑃)) ⊆ (𝑥 supp (0g𝑅)))) → (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) finSupp (0g𝑃))
177155, 159, 175, 176syl12anc 837 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) finSupp (0g𝑃))
17840, 44, 47, 57, 150, 177gsumsubgcl 19952 . . 3 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0m 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))))) ∈ (𝐴‘ran 𝑉))
17939, 178eqeltrd 2838 . 2 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (𝐴‘ran 𝑉))
18031, 179eqelssd 4016 1 (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wral 3058  {crab 3432  Vcvv 3477  cdif 3959  wss 3962  ifcif 4530   class class class wbr 5147  cmpt 5230  ccnv 5687  ran crn 5689  cima 5691  Fun wfun 6556   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430   supp csupp 8183  m cmap 8864  Fincfn 8983   finSupp cfsupp 9398  0cc0 11152  cn 12263  0cn0 12523  Basecbs 17244  .rcmulr 17298  Scalarcsca 17300   ·𝑠 cvsca 17301  0gc0g 17485   Σg cgsu 17486  SubMndcsubmnd 18807  .gcmg 19097  SubGrpcsubg 19150  CMndccmn 19812  Abelcabl 19813  mulGrpcmgp 20151  1rcur 20198  Ringcrg 20250  CRingccrg 20251  SubRingcsubrg 20585  LModclmod 20874  LSubSpclss 20946  AssAlgcasa 21887  AlgSpancasp 21888   mPwSer cmps 21941   mVar cmvr 21942   mPoly cmpl 21943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-ofr 7697  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-fz 13544  df-fzo 13691  df-seq 14039  df-hash 14366  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-hom 17321  df-cco 17322  df-0g 17487  df-gsum 17488  df-prds 17493  df-pws 17495  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mhm 18808  df-submnd 18809  df-grp 18966  df-minusg 18967  df-sbg 18968  df-mulg 19098  df-subg 19153  df-ghm 19243  df-cntz 19347  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-srg 20204  df-ring 20252  df-cring 20253  df-subrng 20562  df-subrg 20586  df-lmod 20876  df-lss 20947  df-assa 21890  df-asp 21891  df-psr 21946  df-mvr 21947  df-mpl 21948
This theorem is referenced by:  mplind  22111  evlseu  22124
  Copyright terms: Public domain W3C validator