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

Theorem mplbas2 19672
 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 19616 . . . 4 (𝜑𝑆 ∈ AssAlg)
5 mplbas2.p . . . . . 6 𝑃 = (𝐼 mPoly 𝑅)
6 eqid 2760 . . . . . 6 (Base‘𝑃) = (Base‘𝑃)
7 eqid 2760 . . . . . 6 (Base‘𝑆) = (Base‘𝑆)
85, 1, 6, 7mplbasss 19634 . . . . 5 (Base‘𝑃) ⊆ (Base‘𝑆)
98a1i 11 . . . 4 (𝜑 → (Base‘𝑃) ⊆ (Base‘𝑆))
10 mplbas2.v . . . . . . . 8 𝑉 = (𝐼 mVar 𝑅)
11 crngring 18758 . . . . . . . . 9 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
123, 11syl 17 . . . . . . . 8 (𝜑𝑅 ∈ Ring)
131, 10, 7, 2, 12mvrf 19626 . . . . . . 7 (𝜑𝑉:𝐼⟶(Base‘𝑆))
1413ffnd 6207 . . . . . 6 (𝜑𝑉 Fn 𝐼)
152adantr 472 . . . . . . . 8 ((𝜑𝑥𝐼) → 𝐼𝑊)
1612adantr 472 . . . . . . . 8 ((𝜑𝑥𝐼) → 𝑅 ∈ Ring)
17 simpr 479 . . . . . . . 8 ((𝜑𝑥𝐼) → 𝑥𝐼)
185, 10, 6, 15, 16, 17mvrcl 19651 . . . . . . 7 ((𝜑𝑥𝐼) → (𝑉𝑥) ∈ (Base‘𝑃))
1918ralrimiva 3104 . . . . . 6 (𝜑 → ∀𝑥𝐼 (𝑉𝑥) ∈ (Base‘𝑃))
20 ffnfv 6551 . . . . . 6 (𝑉:𝐼⟶(Base‘𝑃) ↔ (𝑉 Fn 𝐼 ∧ ∀𝑥𝐼 (𝑉𝑥) ∈ (Base‘𝑃)))
2114, 19, 20sylanbrc 701 . . . . 5 (𝜑𝑉:𝐼⟶(Base‘𝑃))
22 frn 6214 . . . . 5 (𝑉:𝐼⟶(Base‘𝑃) → ran 𝑉 ⊆ (Base‘𝑃))
2321, 22syl 17 . . . 4 (𝜑 → ran 𝑉 ⊆ (Base‘𝑃))
24 mplbas2.a . . . . 5 𝐴 = (AlgSpan‘𝑆)
2524, 7aspss 19534 . . . 4 ((𝑆 ∈ AssAlg ∧ (Base‘𝑃) ⊆ (Base‘𝑆) ∧ ran 𝑉 ⊆ (Base‘𝑃)) → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃)))
264, 9, 23, 25syl3anc 1477 . . 3 (𝜑 → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃)))
271, 5, 6, 2, 12mplsubrg 19642 . . . 4 (𝜑 → (Base‘𝑃) ∈ (SubRing‘𝑆))
281, 5, 6, 2, 12mpllss 19640 . . . 4 (𝜑 → (Base‘𝑃) ∈ (LSubSp‘𝑆))
29 eqid 2760 . . . . 5 (LSubSp‘𝑆) = (LSubSp‘𝑆)
3024, 7, 29aspid 19532 . . . 4 ((𝑆 ∈ AssAlg ∧ (Base‘𝑃) ∈ (SubRing‘𝑆) ∧ (Base‘𝑃) ∈ (LSubSp‘𝑆)) → (𝐴‘(Base‘𝑃)) = (Base‘𝑃))
314, 27, 28, 30syl3anc 1477 . . 3 (𝜑 → (𝐴‘(Base‘𝑃)) = (Base‘𝑃))
3226, 31sseqtrd 3782 . 2 (𝜑 → (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))
33 eqid 2760 . . . . . 6 {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}
34 eqid 2760 . . . . . 6 (0g𝑅) = (0g𝑅)
35 eqid 2760 . . . . . 6 (1r𝑅) = (1r𝑅)
362adantr 472 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝐼𝑊)
37 eqid 2760 . . . . . 6 ( ·𝑠𝑃) = ( ·𝑠𝑃)
3812adantr 472 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑅 ∈ Ring)
39 simpr 479 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (Base‘𝑃))
405, 33, 34, 35, 36, 6, 37, 38, 39mplcoe1 19667 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))))))
41 eqid 2760 . . . . . 6 (0g𝑃) = (0g𝑃)
425mplring 19654 . . . . . . . . 9 ((𝐼𝑊𝑅 ∈ Ring) → 𝑃 ∈ Ring)
432, 12, 42syl2anc 696 . . . . . . . 8 (𝜑𝑃 ∈ Ring)
44 ringabl 18780 . . . . . . . 8 (𝑃 ∈ Ring → 𝑃 ∈ Abel)
4543, 44syl 17 . . . . . . 7 (𝜑𝑃 ∈ Abel)
4645adantr 472 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑃 ∈ Abel)
47 ovex 6841 . . . . . . . 8 (ℕ0𝑚 𝐼) ∈ V
4847rabex 4964 . . . . . . 7 {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∈ V
4948a1i 11 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑃)) → {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∈ V)
5023, 8syl6ss 3756 . . . . . . . . . 10 (𝜑 → ran 𝑉 ⊆ (Base‘𝑆))
5124, 7aspsubrg 19533 . . . . . . . . . 10 ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆))
524, 50, 51syl2anc 696 . . . . . . . . 9 (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆))
535, 1, 6mplval2 19633 . . . . . . . . . . 11 𝑃 = (𝑆s (Base‘𝑃))
5453subsubrg 19008 . . . . . . . . . 10 ((Base‘𝑃) ∈ (SubRing‘𝑆) → ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
5527, 54syl 17 . . . . . . . . 9 (𝜑 → ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
5652, 32, 55mpbir2and 995 . . . . . . . 8 (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃))
57 subrgsubg 18988 . . . . . . . 8 ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
5856, 57syl 17 . . . . . . 7 (𝜑 → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
5958adantr 472 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
605mpllmod 19653 . . . . . . . . . 10 ((𝐼𝑊𝑅 ∈ Ring) → 𝑃 ∈ LMod)
612, 12, 60syl2anc 696 . . . . . . . . 9 (𝜑𝑃 ∈ LMod)
6261ad2antrr 764 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑃 ∈ LMod)
6324, 7, 29asplss 19531 . . . . . . . . . . 11 ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆))
644, 50, 63syl2anc 696 . . . . . . . . . 10 (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆))
651, 2, 12psrlmod 19603 . . . . . . . . . . 11 (𝜑𝑆 ∈ LMod)
66 eqid 2760 . . . . . . . . . . . 12 (LSubSp‘𝑃) = (LSubSp‘𝑃)
6753, 29, 66lsslss 19163 . . . . . . . . . . 11 ((𝑆 ∈ LMod ∧ (Base‘𝑃) ∈ (LSubSp‘𝑆)) → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
6865, 28, 67syl2anc 696 . . . . . . . . . 10 (𝜑 → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
6964, 32, 68mpbir2and 995 . . . . . . . . 9 (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃))
7069ad2antrr 764 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃))
71 eqid 2760 . . . . . . . . . . 11 (Base‘𝑅) = (Base‘𝑅)
725, 71, 6, 33, 39mplelf 19635 . . . . . . . . . 10 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑥:{𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}⟶(Base‘𝑅))
7372ffvelrnda 6522 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑥𝑘) ∈ (Base‘𝑅))
745, 36, 38mplsca 19647 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑅 = (Scalar‘𝑃))
7574adantr 472 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑅 = (Scalar‘𝑃))
7675fveq2d 6356 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
7773, 76eleqtrd 2841 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑥𝑘) ∈ (Base‘(Scalar‘𝑃)))
782ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝐼𝑊)
79 eqid 2760 . . . . . . . . . 10 (mulGrp‘𝑃) = (mulGrp‘𝑃)
80 eqid 2760 . . . . . . . . . 10 (.g‘(mulGrp‘𝑃)) = (.g‘(mulGrp‘𝑃))
813ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ CRing)
82 simpr 479 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin})
835, 33, 34, 35, 78, 79, 80, 10, 81, 82mplcoe2 19671 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))) = ((mulGrp‘𝑃) Σg (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)))))
84 eqid 2760 . . . . . . . . . . 11 (1r𝑃) = (1r𝑃)
8579, 84ringidval 18703 . . . . . . . . . 10 (1r𝑃) = (0g‘(mulGrp‘𝑃))
865mplcrng 19655 . . . . . . . . . . . . 13 ((𝐼𝑊𝑅 ∈ CRing) → 𝑃 ∈ CRing)
872, 3, 86syl2anc 696 . . . . . . . . . . . 12 (𝜑𝑃 ∈ CRing)
8879crngmgp 18755 . . . . . . . . . . . 12 (𝑃 ∈ CRing → (mulGrp‘𝑃) ∈ CMnd)
8987, 88syl 17 . . . . . . . . . . 11 (𝜑 → (mulGrp‘𝑃) ∈ CMnd)
9089ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (mulGrp‘𝑃) ∈ CMnd)
9156ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃))
9279subrgsubm 18995 . . . . . . . . . . 11 ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃)))
9391, 92syl 17 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃)))
94 simplll 815 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → 𝜑)
9533psrbag 19566 . . . . . . . . . . . . . . . 16 (𝐼𝑊 → (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (𝑘 “ ℕ) ∈ Fin)))
9636, 95syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (𝑘 “ ℕ) ∈ Fin)))
9796biimpa 502 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑘:𝐼⟶ℕ0 ∧ (𝑘 “ ℕ) ∈ Fin))
9897simpld 477 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑘:𝐼⟶ℕ0)
9998ffvelrnda 6522 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → (𝑘𝑧) ∈ ℕ0)
10024, 7aspssid 19535 . . . . . . . . . . . . . . 15 ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
1014, 50, 100syl2anc 696 . . . . . . . . . . . . . 14 (𝜑 → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
102101ad3antrrr 768 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
10314ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑉 Fn 𝐼)
104 fnfvelrn 6519 . . . . . . . . . . . . . 14 ((𝑉 Fn 𝐼𝑧𝐼) → (𝑉𝑧) ∈ ran 𝑉)
105103, 104sylan 489 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → (𝑉𝑧) ∈ ran 𝑉)
106102, 105sseldd 3745 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → (𝑉𝑧) ∈ (𝐴‘ran 𝑉))
10779, 6mgpbas 18695 . . . . . . . . . . . . 13 (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
108 eqid 2760 . . . . . . . . . . . . . 14 (.r𝑃) = (.r𝑃)
10979, 108mgpplusg 18693 . . . . . . . . . . . . 13 (.r𝑃) = (+g‘(mulGrp‘𝑃))
110108subrgmcl 18994 . . . . . . . . . . . . . 14 (((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r𝑃)𝑣) ∈ (𝐴‘ran 𝑉))
11156, 110syl3an1 1167 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r𝑃)𝑣) ∈ (𝐴‘ran 𝑉))
11284subrg1cl 18990 . . . . . . . . . . . . . 14 ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (1r𝑃) ∈ (𝐴‘ran 𝑉))
11356, 112syl 17 . . . . . . . . . . . . 13 (𝜑 → (1r𝑃) ∈ (𝐴‘ran 𝑉))
114107, 80, 109, 89, 32, 111, 85, 113mulgnn0subcl 17755 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘𝑧) ∈ ℕ0 ∧ (𝑉𝑧) ∈ (𝐴‘ran 𝑉)) → ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)) ∈ (𝐴‘ran 𝑉))
11594, 99, 106, 114syl3anc 1477 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧𝐼) → ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)) ∈ (𝐴‘ran 𝑉))
116 eqid 2760 . . . . . . . . . . 11 (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) = (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)))
117115, 116fmptd 6548 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))):𝐼⟶(𝐴‘ran 𝑉))
118 mptexg 6648 . . . . . . . . . . . . 13 (𝐼𝑊 → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) ∈ V)
1192, 118syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) ∈ V)
120119ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) ∈ V)
121 funmpt 6087 . . . . . . . . . . . 12 Fun (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)))
122121a1i 11 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → Fun (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))))
123 fvexd 6364 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (1r𝑃) ∈ V)
12497simprd 482 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑘 “ ℕ) ∈ Fin)
125 elrabi 3499 . . . . . . . . . . . . . . 15 (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} → 𝑘 ∈ (ℕ0𝑚 𝐼))
126 elmapi 8045 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (ℕ0𝑚 𝐼) → 𝑘:𝐼⟶ℕ0)
127126adantl 473 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0𝑚 𝐼)) → 𝑘:𝐼⟶ℕ0)
1282ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0𝑚 𝐼)) → 𝐼𝑊)
129 frnnn0supp 11541 . . . . . . . . . . . . . . . . . 18 ((𝐼𝑊𝑘:𝐼⟶ℕ0) → (𝑘 supp 0) = (𝑘 “ ℕ))
130128, 127, 129syl2anc 696 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0𝑚 𝐼)) → (𝑘 supp 0) = (𝑘 “ ℕ))
131 eqimss 3798 . . . . . . . . . . . . . . . . 17 ((𝑘 supp 0) = (𝑘 “ ℕ) → (𝑘 supp 0) ⊆ (𝑘 “ ℕ))
132130, 131syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0𝑚 𝐼)) → (𝑘 supp 0) ⊆ (𝑘 “ ℕ))
133 c0ex 10226 . . . . . . . . . . . . . . . . 17 0 ∈ V
134133a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0𝑚 𝐼)) → 0 ∈ V)
135127, 132, 128, 134suppssr 7495 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0𝑚 𝐼)) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → (𝑘𝑧) = 0)
136125, 135sylanl2 686 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → (𝑘𝑧) = 0)
137136oveq1d 6828 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)) = (0(.g‘(mulGrp‘𝑃))(𝑉𝑧)))
1382ad3antrrr 768 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → 𝐼𝑊)
13912ad3antrrr 768 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → 𝑅 ∈ Ring)
140 eldifi 3875 . . . . . . . . . . . . . . . 16 (𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ)) → 𝑧𝐼)
141140adantl 473 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → 𝑧𝐼)
1425, 10, 6, 138, 139, 141mvrcl 19651 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → (𝑉𝑧) ∈ (Base‘𝑃))
143107, 85, 80mulg0 17747 . . . . . . . . . . . . . 14 ((𝑉𝑧) ∈ (Base‘𝑃) → (0(.g‘(mulGrp‘𝑃))(𝑉𝑧)) = (1r𝑃))
144142, 143syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → (0(.g‘(mulGrp‘𝑃))(𝑉𝑧)) = (1r𝑃))
145137, 144eqtrd 2794 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (𝑘 “ ℕ))) → ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)) = (1r𝑃))
146145, 78suppss2 7498 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → ((𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) supp (1r𝑃)) ⊆ (𝑘 “ ℕ))
147 suppssfifsupp 8455 . . . . . . . . . . 11 ((((𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) ∈ V ∧ Fun (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) ∧ (1r𝑃) ∈ V) ∧ ((𝑘 “ ℕ) ∈ Fin ∧ ((𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) supp (1r𝑃)) ⊆ (𝑘 “ ℕ))) → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) finSupp (1r𝑃))
148120, 122, 123, 124, 146, 147syl32anc 1485 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧))) finSupp (1r𝑃))
14985, 90, 78, 93, 117, 148gsumsubmcl 18519 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → ((mulGrp‘𝑃) Σg (𝑧𝐼 ↦ ((𝑘𝑧)(.g‘(mulGrp‘𝑃))(𝑉𝑧)))) ∈ (𝐴‘ran 𝑉))
15083, 149eqeltrd 2839 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))) ∈ (𝐴‘ran 𝑉))
151 eqid 2760 . . . . . . . . 9 (Scalar‘𝑃) = (Scalar‘𝑃)
152 eqid 2760 . . . . . . . . 9 (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
153151, 37, 152, 66lssvscl 19157 . . . . . . . 8 (((𝑃 ∈ LMod ∧ (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) ∧ ((𝑥𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))) ∈ (𝐴‘ran 𝑉))) → ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) ∈ (𝐴‘ran 𝑉))
15462, 70, 77, 150, 153syl22anc 1478 . . . . . . 7 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) ∈ (𝐴‘ran 𝑉))
155 eqid 2760 . . . . . . 7 (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) = (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))))
156154, 155fmptd 6548 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))):{𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}⟶(𝐴‘ran 𝑉))
15747mptrabex 6652 . . . . . . . . 9 (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∈ V
158 funmpt 6087 . . . . . . . . 9 Fun (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))))
159 fvex 6362 . . . . . . . . 9 (0g𝑃) ∈ V
160157, 158, 1593pm3.2i 1424 . . . . . . . 8 ((𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∧ (0g𝑃) ∈ V)
161160a1i 11 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) ∧ (0g𝑃) ∈ V))
1625, 1, 7, 34, 6mplelbas 19632 . . . . . . . . . 10 (𝑥 ∈ (Base‘𝑃) ↔ (𝑥 ∈ (Base‘𝑆) ∧ 𝑥 finSupp (0g𝑅)))
163162simprbi 483 . . . . . . . . 9 (𝑥 ∈ (Base‘𝑃) → 𝑥 finSupp (0g𝑅))
164163adantl 473 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑥 finSupp (0g𝑅))
165164fsuppimpd 8447 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g𝑅)) ∈ Fin)
166 ssid 3765 . . . . . . . . . . . . 13 (𝑥 supp (0g𝑅)) ⊆ (𝑥 supp (0g𝑅))
167166a1i 11 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g𝑅)) ⊆ (𝑥 supp (0g𝑅)))
168 fvexd 6364 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (Base‘𝑃)) → (0g𝑅) ∈ V)
16972, 167, 49, 168suppssr 7495 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → (𝑥𝑘) = (0g𝑅))
17074fveq2d 6356 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (Base‘𝑃)) → (0g𝑅) = (0g‘(Scalar‘𝑃)))
171170adantr 472 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → (0g𝑅) = (0g‘(Scalar‘𝑃)))
172169, 171eqtrd 2794 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → (𝑥𝑘) = (0g‘(Scalar‘𝑃)))
173172oveq1d 6828 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) = ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))))
174 eldifi 3875 . . . . . . . . . 10 (𝑘 ∈ ({𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅))) → 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin})
17512ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ Ring)
1765, 6, 34, 35, 33, 78, 175, 82mplmon 19665 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))) ∈ (Base‘𝑃))
177 eqid 2760 . . . . . . . . . . . 12 (0g‘(Scalar‘𝑃)) = (0g‘(Scalar‘𝑃))
1786, 151, 37, 177, 41lmod0vs 19098 . . . . . . . . . . 11 ((𝑃 ∈ LMod ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))) ∈ (Base‘𝑃)) → ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) = (0g𝑃))
17962, 176, 178syl2anc 696 . . . . . . . . . 10 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin}) → ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) = (0g𝑃))
180174, 179sylan2 492 . . . . . . . . 9 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → ((0g‘(Scalar‘𝑃))( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) = (0g𝑃))
181173, 180eqtrd 2794 . . . . . . . 8 (((𝜑𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g𝑅)))) → ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))) = (0g𝑃))
182181, 49suppss2 7498 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) supp (0g𝑃)) ⊆ (𝑥 supp (0g𝑅)))
183 suppssfifsupp 8455 . . . . . . 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𝑃))
184161, 165, 182, 183syl12anc 1475 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅))))) finSupp (0g𝑃))
18541, 46, 49, 59, 156, 184gsumsubgcl 18520 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝑃)) → (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥𝑘)( ·𝑠𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0𝑚 𝐼) ∣ (𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r𝑅), (0g𝑅)))))) ∈ (𝐴‘ran 𝑉))
18640, 185eqeltrd 2839 . . . 4 ((𝜑𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (𝐴‘ran 𝑉))
187186ex 449 . . 3 (𝜑 → (𝑥 ∈ (Base‘𝑃) → 𝑥 ∈ (𝐴‘ran 𝑉)))
188187ssrdv 3750 . 2 (𝜑 → (Base‘𝑃) ⊆ (𝐴‘ran 𝑉))
18932, 188eqssd 3761 1 (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139  ∀wral 3050  {crab 3054  Vcvv 3340   ∖ cdif 3712   ⊆ wss 3715  ifcif 4230   class class class wbr 4804   ↦ cmpt 4881  ◡ccnv 5265  ran crn 5267   “ cima 5269  Fun wfun 6043   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049  (class class class)co 6813   supp csupp 7463   ↑𝑚 cmap 8023  Fincfn 8121   finSupp cfsupp 8440  0cc0 10128  ℕcn 11212  ℕ0cn0 11484  Basecbs 16059  .rcmulr 16144  Scalarcsca 16146   ·𝑠 cvsca 16147  0gc0g 16302   Σg cgsu 16303  SubMndcsubmnd 17535  .gcmg 17741  SubGrpcsubg 17789  CMndccmn 18393  Abelcabl 18394  mulGrpcmgp 18689  1rcur 18701  Ringcrg 18747  CRingccrg 18748  SubRingcsubrg 18978  LModclmod 19065  LSubSpclss 19134  AssAlgcasa 19511  AlgSpancasp 19512   mPwSer cmps 19553   mVar cmvr 19554   mPoly cmpl 19555 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-ofr 7063  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-oi 8580  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-uz 11880  df-fz 12520  df-fzo 12660  df-seq 12996  df-hash 13312  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-sca 16159  df-vsca 16160  df-tset 16162  df-0g 16304  df-gsum 16305  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-subg 17792  df-ghm 17859  df-cntz 17950  df-cmn 18395  df-abl 18396  df-mgp 18690  df-ur 18702  df-srg 18706  df-ring 18749  df-cring 18750  df-subrg 18980  df-lmod 19067  df-lss 19135  df-assa 19514  df-asp 19515  df-psr 19558  df-mvr 19559  df-mpl 19560 This theorem is referenced by:  mplind  19704  evlseu  19718
 Copyright terms: Public domain W3C validator