Metamath Proof Explorer

Theorem mplbas2

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)

Ref Expression
Hypotheses mplbas2.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplbas2.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
mplbas2.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
mplbas2.a ⊢ 𝐴 = ( AlgSpan ‘ 𝑆 )
mplbas2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mplbas2.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion mplbas2 ( 𝜑 → ( 𝐴 ‘ ran 𝑉 ) = ( Base ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 mplbas2.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplbas2.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
3 mplbas2.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
4 mplbas2.a ⊢ 𝐴 = ( AlgSpan ‘ 𝑆 )
5 mplbas2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 mplbas2.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
7 2 5 6 psrassa ⊢ ( 𝜑 → 𝑆 ∈ AssAlg )
8 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
9 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10 1 2 8 9 mplbasss ⊢ ( Base ‘ 𝑃 ) ⊆ ( Base ‘ 𝑆 )
11 10 a1i ⊢ ( 𝜑 → ( Base ‘ 𝑃 ) ⊆ ( Base ‘ 𝑆 ) )
12 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
13 6 12 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
14 2 3 9 5 13 mvrf ⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ ( Base ‘ 𝑆 ) )
15 14 ffnd ⊢ ( 𝜑 → 𝑉 Fn 𝐼 )
16 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
17 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ Ring )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
19 1 3 8 16 17 18 mvrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑉 ‘ 𝑥 ) ∈ ( Base ‘ 𝑃 ) )
20 19 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝑉 ‘ 𝑥 ) ∈ ( Base ‘ 𝑃 ) )
21 ffnfv ⊢ ( 𝑉 : 𝐼 ⟶ ( Base ‘ 𝑃 ) ↔ ( 𝑉 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑉 ‘ 𝑥 ) ∈ ( Base ‘ 𝑃 ) ) )
22 15 20 21 sylanbrc ⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ ( Base ‘ 𝑃 ) )
23 22 frnd ⊢ ( 𝜑 → ran 𝑉 ⊆ ( Base ‘ 𝑃 ) )
24 4 9 aspss ⊢ ( ( 𝑆 ∈ AssAlg ∧ ( Base ‘ 𝑃 ) ⊆ ( Base ‘ 𝑆 ) ∧ ran 𝑉 ⊆ ( Base ‘ 𝑃 ) ) → ( 𝐴 ‘ ran 𝑉 ) ⊆ ( 𝐴 ‘ ( Base ‘ 𝑃 ) ) )
25 7 11 23 24 syl3anc ⊢ ( 𝜑 → ( 𝐴 ‘ ran 𝑉 ) ⊆ ( 𝐴 ‘ ( Base ‘ 𝑃 ) ) )
26 2 1 8 5 13 mplsubrg ⊢ ( 𝜑 → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ 𝑆 ) )
27 2 1 8 5 13 mpllss ⊢ ( 𝜑 → ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ 𝑆 ) )
28 eqid ⊢ ( LSubSp ‘ 𝑆 ) = ( LSubSp ‘ 𝑆 )
29 4 9 28 aspid ⊢ ( ( 𝑆 ∈ AssAlg ∧ ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ 𝑆 ) ∧ ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ 𝑆 ) ) → ( 𝐴 ‘ ( Base ‘ 𝑃 ) ) = ( Base ‘ 𝑃 ) )
30 7 26 27 29 syl3anc ⊢ ( 𝜑 → ( 𝐴 ‘ ( Base ‘ 𝑃 ) ) = ( Base ‘ 𝑃 ) )
31 25 30 sseqtrd ⊢ ( 𝜑 → ( 𝐴 ‘ ran 𝑉 ) ⊆ ( Base ‘ 𝑃 ) )
32 eqid ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
33 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
34 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
35 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝐼 ∈ 𝑊 )
36 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
37 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝑅 ∈ Ring )
38 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
39 1 32 33 34 35 8 36 37 38 mplcoe1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝑥 = ( 𝑃 Σg ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) ) )
40 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
41 1 mplring ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
42 5 13 41 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ Ring )
43 ringabl ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Abel )
44 42 43 syl ⊢ ( 𝜑 → 𝑃 ∈ Abel )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝑃 ∈ Abel )
46 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
47 46 rabex ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
48 47 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
49 14 frnd ⊢ ( 𝜑 → ran 𝑉 ⊆ ( Base ‘ 𝑆 ) )
50 4 9 aspsubrg ⊢ ( ( 𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑆 ) )
51 7 49 50 syl2anc ⊢ ( 𝜑 → ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑆 ) )
52 1 2 8 mplval2 ⊢ 𝑃 = ( 𝑆 ↾s ( Base ‘ 𝑃 ) )
53 52 subsubrg ⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ 𝑆 ) → ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑃 ) ↔ ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑆 ) ∧ ( 𝐴 ‘ ran 𝑉 ) ⊆ ( Base ‘ 𝑃 ) ) ) )
54 26 53 syl ⊢ ( 𝜑 → ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑃 ) ↔ ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑆 ) ∧ ( 𝐴 ‘ ran 𝑉 ) ⊆ ( Base ‘ 𝑃 ) ) ) )
55 51 31 54 mpbir2and ⊢ ( 𝜑 → ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑃 ) )
56 subrgsubg ⊢ ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑃 ) → ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubGrp ‘ 𝑃 ) )
57 55 56 syl ⊢ ( 𝜑 → ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubGrp ‘ 𝑃 ) )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubGrp ‘ 𝑃 ) )
59 1 mpllmod ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
60 5 13 59 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ LMod )
61 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑃 ∈ LMod )
62 4 9 28 asplss ⊢ ( ( 𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝐴 ‘ ran 𝑉 ) ∈ ( LSubSp ‘ 𝑆 ) )
63 7 49 62 syl2anc ⊢ ( 𝜑 → ( 𝐴 ‘ ran 𝑉 ) ∈ ( LSubSp ‘ 𝑆 ) )
64 2 5 13 psrlmod ⊢ ( 𝜑 → 𝑆 ∈ LMod )
65 eqid ⊢ ( LSubSp ‘ 𝑃 ) = ( LSubSp ‘ 𝑃 )
66 52 28 65 lsslss ⊢ ( ( 𝑆 ∈ LMod ∧ ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ 𝑆 ) ) → ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( LSubSp ‘ 𝑃 ) ↔ ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( LSubSp ‘ 𝑆 ) ∧ ( 𝐴 ‘ ran 𝑉 ) ⊆ ( Base ‘ 𝑃 ) ) ) )
67 64 27 66 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( LSubSp ‘ 𝑃 ) ↔ ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( LSubSp ‘ 𝑆 ) ∧ ( 𝐴 ‘ ran 𝑉 ) ⊆ ( Base ‘ 𝑃 ) ) ) )
68 63 31 67 mpbir2and ⊢ ( 𝜑 → ( 𝐴 ‘ ran 𝑉 ) ∈ ( LSubSp ‘ 𝑃 ) )
69 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝐴 ‘ ran 𝑉 ) ∈ ( LSubSp ‘ 𝑃 ) )
70 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
71 1 70 8 32 38 mplelf ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝑥 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
72 71 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑥 ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
73 1 35 37 mplsca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
74 73 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
75 74 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
76 72 75 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑥 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
77 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝐼 ∈ 𝑊 )
78 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
79 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
80 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑅 ∈ CRing )
81 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
82 1 32 33 34 77 78 79 3 80 81 mplcoe2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( ( mulGrp ‘ 𝑃 ) Σg ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) ) )
83 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
84 78 83 ringidval ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ ( mulGrp ‘ 𝑃 ) )
85 1 mplcrng ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ CRing )
86 5 6 85 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ CRing )
87 78 crngmgp ⊢ ( 𝑃 ∈ CRing → ( mulGrp ‘ 𝑃 ) ∈ CMnd )
88 86 87 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ CMnd )
89 88 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( mulGrp ‘ 𝑃 ) ∈ CMnd )
90 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑃 ) )
91 78 subrgsubm ⊢ ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑃 ) → ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑃 ) ) )
92 90 91 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑃 ) ) )
93 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ 𝐼 ) → 𝜑 )
94 32 psrbag ⊢ ( 𝐼 ∈ 𝑊 → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↔ ( 𝑘 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑘 “ ℕ ) ∈ Fin ) ) )
95 35 94 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↔ ( 𝑘 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑘 “ ℕ ) ∈ Fin ) ) )
96 95 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑘 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑘 “ ℕ ) ∈ Fin ) )
97 96 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
98 97 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 )
99 4 9 aspssid ⊢ ( ( 𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ ( Base ‘ 𝑆 ) ) → ran 𝑉 ⊆ ( 𝐴 ‘ ran 𝑉 ) )
100 7 49 99 syl2anc ⊢ ( 𝜑 → ran 𝑉 ⊆ ( 𝐴 ‘ ran 𝑉 ) )
101 100 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ 𝐼 ) → ran 𝑉 ⊆ ( 𝐴 ‘ ran 𝑉 ) )
102 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑉 Fn 𝐼 )
103 fnfvelrn ⊢ ( ( 𝑉 Fn 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( 𝑉 ‘ 𝑧 ) ∈ ran 𝑉 )
104 102 103 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑉 ‘ 𝑧 ) ∈ ran 𝑉 )
105 101 104 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑉 ‘ 𝑧 ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
106 78 8 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
107 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
108 78 107 mgpplusg ⊢ ( .r ‘ 𝑃 ) = ( +g ‘ ( mulGrp ‘ 𝑃 ) )
109 107 subrgmcl ⊢ ( ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑃 ) ∧ 𝑢 ∈ ( 𝐴 ‘ ran 𝑉 ) ∧ 𝑣 ∈ ( 𝐴 ‘ ran 𝑉 ) ) → ( 𝑢 ( .r ‘ 𝑃 ) 𝑣 ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
110 55 109 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ‘ ran 𝑉 ) ∧ 𝑣 ∈ ( 𝐴 ‘ ran 𝑉 ) ) → ( 𝑢 ( .r ‘ 𝑃 ) 𝑣 ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
111 83 subrg1cl ⊢ ( ( 𝐴 ‘ ran 𝑉 ) ∈ ( SubRing ‘ 𝑃 ) → ( 1r ‘ 𝑃 ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
112 55 111 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
113 106 79 108 88 31 110 84 112 mulgnn0subcl ⊢ ( ( 𝜑 ∧ ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑉 ‘ 𝑧 ) ∈ ( 𝐴 ‘ ran 𝑉 ) ) → ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
114 93 98 105 113 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
115 114 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) : 𝐼 ⟶ ( 𝐴 ‘ ran 𝑉 ) )
116 5 mptexd ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) ∈ V )
117 116 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) ∈ V )
118 funmpt ⊢ Fun ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) )
119 118 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → Fun ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) )
120 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 1r ‘ 𝑃 ) ∈ V )
121 96 simprd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( ◡ 𝑘 “ ℕ ) ∈ Fin )
122 elrabi ⊢ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } → 𝑘 ∈ ( ℕ0 ↑m 𝐼 ) )
123 elmapi ⊢ ( 𝑘 ∈ ( ℕ0 ↑m 𝐼 ) → 𝑘 : 𝐼 ⟶ ℕ0 )
124 123 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ↑m 𝐼 ) ) → 𝑘 : 𝐼 ⟶ ℕ0 )
125 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ↑m 𝐼 ) ) → 𝐼 ∈ 𝑊 )
126 frnnn0supp ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑘 : 𝐼 ⟶ ℕ0 ) → ( 𝑘 supp 0 ) = ( ◡ 𝑘 “ ℕ ) )
127 125 124 126 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ↑m 𝐼 ) ) → ( 𝑘 supp 0 ) = ( ◡ 𝑘 “ ℕ ) )
128 eqimss ⊢ ( ( 𝑘 supp 0 ) = ( ◡ 𝑘 “ ℕ ) → ( 𝑘 supp 0 ) ⊆ ( ◡ 𝑘 “ ℕ ) )
129 127 128 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ↑m 𝐼 ) ) → ( 𝑘 supp 0 ) ⊆ ( ◡ 𝑘 “ ℕ ) )
130 c0ex ⊢ 0 ∈ V
131 130 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ↑m 𝐼 ) ) → 0 ∈ V )
132 124 129 125 131 suppssr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( ℕ0 ↑m 𝐼 ) ) ∧ 𝑧 ∈ ( 𝐼 ∖ ( ◡ 𝑘 “ ℕ ) ) ) → ( 𝑘 ‘ 𝑧 ) = 0 )
133 122 132 sylanl2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ ( 𝐼 ∖ ( ◡ 𝑘 “ ℕ ) ) ) → ( 𝑘 ‘ 𝑧 ) = 0 )
134 133 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ ( 𝐼 ∖ ( ◡ 𝑘 “ ℕ ) ) ) → ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) = ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) )
135 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ ( 𝐼 ∖ ( ◡ 𝑘 “ ℕ ) ) ) → 𝐼 ∈ 𝑊 )
136 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ ( 𝐼 ∖ ( ◡ 𝑘 “ ℕ ) ) ) → 𝑅 ∈ Ring )
137 eldifi ⊢ ( 𝑧 ∈ ( 𝐼 ∖ ( ◡ 𝑘 “ ℕ ) ) → 𝑧 ∈ 𝐼 )
138 137 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ ( 𝐼 ∖ ( ◡ 𝑘 “ ℕ ) ) ) → 𝑧 ∈ 𝐼 )
139 1 3 8 135 136 138 mvrcl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ ( 𝐼 ∖ ( ◡ 𝑘 “ ℕ ) ) ) → ( 𝑉 ‘ 𝑧 ) ∈ ( Base ‘ 𝑃 ) )
140 106 84 79 mulg0 ⊢ ( ( 𝑉 ‘ 𝑧 ) ∈ ( Base ‘ 𝑃 ) → ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) = ( 1r ‘ 𝑃 ) )
141 139 140 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ ( 𝐼 ∖ ( ◡ 𝑘 “ ℕ ) ) ) → ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) = ( 1r ‘ 𝑃 ) )
142 134 141 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑧 ∈ ( 𝐼 ∖ ( ◡ 𝑘 “ ℕ ) ) ) → ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) = ( 1r ‘ 𝑃 ) )
143 142 77 suppss2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) supp ( 1r ‘ 𝑃 ) ) ⊆ ( ◡ 𝑘 “ ℕ ) )
144 suppssfifsupp ⊢ ( ( ( ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) ∈ V ∧ Fun ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) ∧ ( 1r ‘ 𝑃 ) ∈ V ) ∧ ( ( ◡ 𝑘 “ ℕ ) ∈ Fin ∧ ( ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) supp ( 1r ‘ 𝑃 ) ) ⊆ ( ◡ 𝑘 “ ℕ ) ) ) → ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) finSupp ( 1r ‘ 𝑃 ) )
145 117 119 120 121 143 144 syl32anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) finSupp ( 1r ‘ 𝑃 ) )
146 84 89 77 92 115 145 gsumsubmcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( ( mulGrp ‘ 𝑃 ) Σg ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( 𝑉 ‘ 𝑧 ) ) ) ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
147 82 146 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
148 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
149 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
150 148 36 149 65 lssvscl ⊢ ( ( ( 𝑃 ∈ LMod ∧ ( 𝐴 ‘ ran 𝑉 ) ∈ ( LSubSp ‘ 𝑃 ) ) ∧ ( ( 𝑥 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( 𝐴 ‘ ran 𝑉 ) ) ) → ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
151 61 69 76 147 150 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
152 151 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( 𝐴 ‘ ran 𝑉 ) )
153 46 mptrabex ⊢ ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) ∈ V
154 funmpt ⊢ Fun ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
155 fvex ⊢ ( 0g ‘ 𝑃 ) ∈ V
156 153 154 155 3pm3.2i ⊢ ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V )
157 156 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V ) )
158 1 2 9 33 8 mplelbas ⊢ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑥 finSupp ( 0g ‘ 𝑅 ) ) )
159 158 simprbi ⊢ ( 𝑥 ∈ ( Base ‘ 𝑃 ) → 𝑥 finSupp ( 0g ‘ 𝑅 ) )
160 159 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝑥 finSupp ( 0g ‘ 𝑅 ) )
161 160 fsuppimpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑥 supp ( 0g ‘ 𝑅 ) ) ∈ Fin )
162 ssidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑥 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝑥 supp ( 0g ‘ 𝑅 ) ) )
163 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
164 71 162 48 163 suppssr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ ( 𝑥 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑥 ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
165 73 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
166 165 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ ( 𝑥 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
167 164 166 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ ( 𝑥 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑥 ‘ 𝑘 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
168 167 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ ( 𝑥 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
169 eldifi ⊢ ( 𝑘 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ ( 𝑥 supp ( 0g ‘ 𝑅 ) ) ) → 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
170 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → 𝑅 ∈ Ring )
171 1 8 33 34 32 77 170 81 mplmon ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( Base ‘ 𝑃 ) )
172 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
173 8 148 36 172 40 lmod0vs ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 0g ‘ 𝑃 ) )
174 61 171 173 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 0g ‘ 𝑃 ) )
175 169 174 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ ( 𝑥 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 0g ‘ 𝑃 ) )
176 168 175 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) ∧ 𝑘 ∈ ( { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∖ ( 𝑥 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 0g ‘ 𝑃 ) )
177 176 48 suppss2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) supp ( 0g ‘ 𝑃 ) ) ⊆ ( 𝑥 supp ( 0g ‘ 𝑅 ) ) )
178 suppssfifsupp ⊢ ( ( ( ( 𝑘 ∈ { 𝑓 ∈ ( ℕ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 ‘ 𝑃 ) )
179 157 161 177 178 syl12anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) finSupp ( 0g ‘ 𝑃 ) )
180 40 45 48 58 152 179 gsumsubgcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑃 Σg ( 𝑘 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( ( 𝑥 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑦 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑦 = 𝑘 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) ) ∈ ( 𝐴 ‘ ran 𝑉 ) )
181 39 180 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝑥 ∈ ( 𝐴 ‘ ran 𝑉 ) )
182 31 181 eqelssd ⊢ ( 𝜑 → ( 𝐴 ‘ ran 𝑉 ) = ( Base ‘ 𝑃 ) )