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