This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1degltdimlem

Description: Lemma for ply1degltdim . (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses ply1degltdim.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1degltdim.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
ply1degltdim.s ⊢ 𝑆 = ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) )
ply1degltdim.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
ply1degltdim.r ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
ply1degltdim.e ⊢ 𝐸 = ( 𝑃 ↾s 𝑆 )
ply1degltdimlem.f ⊢ 𝐹 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
Assertion ply1degltdimlem ( 𝜑 → ran 𝐹 ∈ ( LBasis ‘ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 ply1degltdim.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1degltdim.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3 ply1degltdim.s ⊢ 𝑆 = ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) )
4 ply1degltdim.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 ply1degltdim.r ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
6 ply1degltdim.e ⊢ 𝐸 = ( 𝑃 ↾s 𝑆 )
7 ply1degltdimlem.f ⊢ 𝐹 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝑁 ∈ ℕ0 )
10 5 drngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
11 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝑅 ∈ Ring )
12 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
13 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
14 elmapi ⊢ ( 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) → 𝑎 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) → 𝑎 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
16 1 ply1sca ⊢ ( 𝑅 ∈ DivRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
17 5 16 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
18 17 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
20 19 feq3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) → ( 𝑎 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝑅 ) ↔ 𝑎 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
21 15 20 mpbird ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) → 𝑎 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
22 21 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝑎 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
23 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) )
24 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → ( 0 ..^ 𝑁 ) ∈ V )
25 1 5 ply1lvec ⊢ ( 𝜑 → 𝑃 ∈ LVec )
26 25 lveclmodd ⊢ ( 𝜑 → 𝑃 ∈ LMod )
27 1 2 3 4 10 ply1degltlss ⊢ ( 𝜑 → 𝑆 ∈ ( LSubSp ‘ 𝑃 ) )
28 eqid ⊢ ( LSubSp ‘ 𝑃 ) = ( LSubSp ‘ 𝑃 )
29 28 lsssubg ⊢ ( ( 𝑃 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑃 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝑃 ) )
30 26 27 29 syl2anc ⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝑃 ) )
31 subgsubm ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑃 ) → 𝑆 ∈ ( SubMnd ‘ 𝑃 ) )
32 30 31 syl ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝑃 ) )
33 32 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝑆 ∈ ( SubMnd ‘ 𝑃 ) )
34 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
35 2 1 34 deg1xrf ⊢ 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ*
36 ffn ⊢ ( 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ* → 𝐷 Fn ( Base ‘ 𝑃 ) )
37 35 36 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝐷 Fn ( Base ‘ 𝑃 ) )
38 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
39 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
40 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
41 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑃 ∈ LMod )
42 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
43 34 28 lssss ⊢ ( 𝑆 ∈ ( LSubSp ‘ 𝑃 ) → 𝑆 ⊆ ( Base ‘ 𝑃 ) )
44 27 43 syl ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑃 ) )
45 6 34 ressbas2 ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑃 ) → 𝑆 = ( Base ‘ 𝐸 ) )
46 44 45 syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐸 ) )
47 46 44 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ 𝐸 ) ⊆ ( Base ‘ 𝑃 ) )
48 47 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
49 48 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
50 34 38 39 40 41 42 49 lmodvscld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ∈ ( Base ‘ 𝑃 ) )
51 mnfxr ⊢ -∞ ∈ ℝ*
52 51 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → -∞ ∈ ℝ* )
53 4 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
54 53 rexrd ⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
55 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑁 ∈ ℝ* )
56 35 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ* )
57 56 50 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( 𝐷 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) ∈ ℝ* )
58 57 mnfled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → -∞ ≤ ( 𝐷 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) )
59 56 49 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( 𝐷 ‘ 𝑥 ) ∈ ℝ* )
60 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑅 ∈ Ring )
61 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
62 42 61 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑘 ∈ ( Base ‘ 𝑅 ) )
63 1 2 60 34 8 39 62 49 deg1vscale ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( 𝐷 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) ≤ ( 𝐷 ‘ 𝑥 ) )
64 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝜑 )
65 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
66 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑆 = ( Base ‘ 𝐸 ) )
67 65 66 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑥 ∈ 𝑆 )
68 51 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → -∞ ∈ ℝ* )
69 54 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑁 ∈ ℝ* )
70 35 36 mp1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐷 Fn ( Base ‘ 𝑃 ) )
71 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
72 71 3 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
73 elpreima ⊢ ( 𝐷 Fn ( Base ‘ 𝑃 ) → ( 𝑥 ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐷 ‘ 𝑥 ) ∈ ( -∞ [,) 𝑁 ) ) ) )
74 73 simplbda ⊢ ( ( 𝐷 Fn ( Base ‘ 𝑃 ) ∧ 𝑥 ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) ) → ( 𝐷 ‘ 𝑥 ) ∈ ( -∞ [,) 𝑁 ) )
75 70 72 74 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐷 ‘ 𝑥 ) ∈ ( -∞ [,) 𝑁 ) )
76 elico1 ⊢ ( ( -∞ ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝑥 ) ∈ ( -∞ [,) 𝑁 ) ↔ ( ( 𝐷 ‘ 𝑥 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝑥 ) ∧ ( 𝐷 ‘ 𝑥 ) < 𝑁 ) ) )
77 76 biimpa ⊢ ( ( ( -∞ ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) ∧ ( 𝐷 ‘ 𝑥 ) ∈ ( -∞ [,) 𝑁 ) ) → ( ( 𝐷 ‘ 𝑥 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝑥 ) ∧ ( 𝐷 ‘ 𝑥 ) < 𝑁 ) )
78 77 simp3d ⊢ ( ( ( -∞ ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) ∧ ( 𝐷 ‘ 𝑥 ) ∈ ( -∞ [,) 𝑁 ) ) → ( 𝐷 ‘ 𝑥 ) < 𝑁 )
79 68 69 75 78 syl21anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐷 ‘ 𝑥 ) < 𝑁 )
80 64 67 79 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( 𝐷 ‘ 𝑥 ) < 𝑁 )
81 57 59 55 63 80 xrlelttrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( 𝐷 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) < 𝑁 )
82 52 55 57 58 81 elicod ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( 𝐷 ‘ ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ) ∈ ( -∞ [,) 𝑁 ) )
83 37 50 82 elpreimad ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
84 83 3 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ∈ 𝑆 )
85 84 anasss ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ∈ 𝑆 )
86 85 ad5ant15 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑃 ) 𝑥 ) ∈ 𝑆 )
87 15 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝑎 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
88 35 36 mp1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝐷 Fn ( Base ‘ 𝑃 ) )
89 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
90 89 34 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
91 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
92 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
93 89 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
94 10 92 93 3syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
95 94 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
96 elfzonn0 ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 ∈ ℕ0 )
97 96 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℕ0 )
98 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
99 98 1 34 vr1cl ⊢ ( 𝑅 ∈ Ring → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
100 10 99 syl ⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
101 100 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
102 90 91 95 97 101 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
103 51 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → -∞ ∈ ℝ* )
104 54 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ* )
105 2 1 34 deg1xrcl ⊢ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ℝ* )
106 102 105 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ℝ* )
107 106 mnfled ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → -∞ ≤ ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
108 96 nn0red ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 ∈ ℝ )
109 108 rexrd ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 ∈ ℝ* )
110 109 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℝ* )
111 2 1 98 89 91 deg1pwle ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ≤ 𝑛 )
112 10 96 111 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ≤ 𝑛 )
113 elfzolt2 ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 < 𝑁 )
114 113 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 < 𝑁 )
115 106 110 104 112 114 xrlelttrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) < 𝑁 )
116 103 104 106 107 115 elicod ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ( -∞ [,) 𝑁 ) )
117 88 102 116 elpreimad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
118 117 3 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ 𝑆 )
119 46 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 = ( Base ‘ 𝐸 ) )
120 118 119 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐸 ) )
121 120 7 fmptd ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝐸 ) )
122 121 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝐹 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝐸 ) )
123 inidm ⊢ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 )
124 86 87 122 24 24 123 off ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )
125 24 33 124 6 gsumsubm ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → ( 𝑃 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) )
126 ringmnd ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Mnd )
127 10 92 126 3syl ⊢ ( 𝜑 → 𝑃 ∈ Mnd )
128 35 36 mp1i ⊢ ( 𝜑 → 𝐷 Fn ( Base ‘ 𝑃 ) )
129 34 13 mndidcl ⊢ ( 𝑃 ∈ Mnd → ( 0g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
130 127 129 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
131 51 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
132 2 1 34 deg1xrcl ⊢ ( ( 0g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) ∈ ℝ* )
133 130 132 syl ⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) ∈ ℝ* )
134 133 mnfled ⊢ ( 𝜑 → -∞ ≤ ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) )
135 2 1 13 deg1z ⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
136 10 135 syl ⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
137 53 mnfltd ⊢ ( 𝜑 → -∞ < 𝑁 )
138 136 137 eqbrtrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) < 𝑁 )
139 131 54 133 134 138 elicod ⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) ∈ ( -∞ [,) 𝑁 ) )
140 128 130 139 elpreimad ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
141 140 3 eleqtrrdi ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝑆 )
142 6 34 13 ress0g ⊢ ( ( 𝑃 ∈ Mnd ∧ ( 0g ‘ 𝑃 ) ∈ 𝑆 ∧ 𝑆 ⊆ ( Base ‘ 𝑃 ) ) → ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝐸 ) )
143 127 141 44 142 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝐸 ) )
144 143 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝐸 ) )
145 23 125 144 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → ( 𝑃 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝑃 ) )
146 1 8 9 11 7 12 13 22 145 ply1gsumz ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝑎 = ( ( 0 ..^ 𝑁 ) × { ( 0g ‘ 𝑅 ) } ) )
147 17 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
148 147 sneqd ⊢ ( 𝜑 → { ( 0g ‘ 𝑅 ) } = { ( 0g ‘ ( Scalar ‘ 𝑃 ) ) } )
149 148 xpeq2d ⊢ ( 𝜑 → ( ( 0 ..^ 𝑁 ) × { ( 0g ‘ 𝑅 ) } ) = ( ( 0 ..^ 𝑁 ) × { ( 0g ‘ ( Scalar ‘ 𝑃 ) ) } ) )
150 149 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → ( ( 0 ..^ 𝑁 ) × { ( 0g ‘ 𝑅 ) } ) = ( ( 0 ..^ 𝑁 ) × { ( 0g ‘ ( Scalar ‘ 𝑃 ) ) } ) )
151 146 150 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝑎 = ( ( 0 ..^ 𝑁 ) × { ( 0g ‘ ( Scalar ‘ 𝑃 ) ) } ) )
152 151 expl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ) → ( ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝑎 = ( ( 0 ..^ 𝑁 ) × { ( 0g ‘ ( Scalar ‘ 𝑃 ) ) } ) ) )
153 152 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ( ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝑎 = ( ( 0 ..^ 𝑁 ) × { ( 0g ‘ ( Scalar ‘ 𝑃 ) ) } ) ) )
154 118 7 fmptd ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )
155 154 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝑆 )
156 eqid ⊢ ( LSpan ‘ 𝑃 ) = ( LSpan ‘ 𝑃 )
157 28 156 lspssp ⊢ ( ( 𝑃 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑃 ) ∧ ran 𝐹 ⊆ 𝑆 ) → ( ( LSpan ‘ 𝑃 ) ‘ ran 𝐹 ) ⊆ 𝑆 )
158 26 27 155 157 syl3anc ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑃 ) ‘ ran 𝐹 ) ⊆ 𝑆 )
159 breq1 ⊢ ( 𝑎 = ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) → ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ) )
160 oveq1 ⊢ ( 𝑎 = ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) → ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) = ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) )
161 160 oveq2d ⊢ ( 𝑎 = ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) → ( 𝑃 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 𝑃 Σg ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) )
162 161 eqeq2d ⊢ ( 𝑎 = ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) → ( 𝑥 = ( 𝑃 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ↔ 𝑥 = ( 𝑃 Σg ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) )
163 159 162 anbi12d ⊢ ( 𝑎 = ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) → ( ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 = ( 𝑃 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ↔ ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 = ( 𝑃 Σg ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ) )
164 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∈ V )
165 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0 ..^ 𝑁 ) ∈ V )
166 44 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
167 eqid ⊢ ( coe1 ‘ 𝑥 ) = ( coe1 ‘ 𝑥 )
168 167 34 1 8 coe1f ⊢ ( 𝑥 ∈ ( Base ‘ 𝑃 ) → ( coe1 ‘ 𝑥 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
169 166 168 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( coe1 ‘ 𝑥 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
170 18 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
171 170 feq3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( coe1 ‘ 𝑥 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) ↔ ( coe1 ‘ 𝑥 ) : ℕ0 ⟶ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
172 169 171 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( coe1 ‘ 𝑥 ) : ℕ0 ⟶ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
173 fzo0ssnn0 ⊢ ( 0 ..^ 𝑁 ) ⊆ ℕ0
174 173 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0 ..^ 𝑁 ) ⊆ ℕ0 )
175 172 174 fssresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
176 164 165 175 elmapdd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) )
177 169 ffund ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → Fun ( coe1 ‘ 𝑥 ) )
178 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
179 178 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0 ..^ 𝑁 ) ∈ Fin )
180 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∈ V )
181 177 179 180 resfifsupp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
182 ringcmn ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
183 10 92 182 3syl ⊢ ( 𝜑 → 𝑃 ∈ CMnd )
184 183 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑃 ∈ CMnd )
185 nn0ex ⊢ ℕ0 ∈ V
186 185 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ℕ0 ∈ V )
187 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → 𝑃 ∈ LMod )
188 172 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
189 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → 𝑅 ∈ Ring )
190 189 92 93 3syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
191 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
192 189 99 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
193 90 91 190 191 192 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
194 34 38 39 40 187 188 193 lmodvscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ( Base ‘ 𝑃 ) )
195 eqid ⊢ ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
196 194 195 fmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) : ℕ0 ⟶ ( Base ‘ 𝑃 ) )
197 nfv ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑥 ∈ 𝑆 )
198 197 194 195 fnmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) Fn ℕ0 )
199 fveq2 ⊢ ( 𝑖 = 𝑗 → ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) = ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) )
200 oveq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
201 199 200 oveq12d ⊢ ( 𝑖 = 𝑗 → ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
202 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → 𝑗 ∈ ℕ0 )
203 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ V )
204 195 201 202 203 fvmptd3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) = ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
205 166 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
206 icossxr ⊢ ( -∞ [,) 𝑁 ) ⊆ ℝ*
207 206 75 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐷 ‘ 𝑥 ) ∈ ℝ* )
208 207 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( 𝐷 ‘ 𝑥 ) ∈ ℝ* )
209 54 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → 𝑁 ∈ ℝ* )
210 202 nn0red ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → 𝑗 ∈ ℝ )
211 210 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → 𝑗 ∈ ℝ* )
212 79 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( 𝐷 ‘ 𝑥 ) < 𝑁 )
213 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → 𝑁 ≤ 𝑗 )
214 208 209 211 212 213 xrltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( 𝐷 ‘ 𝑥 ) < 𝑗 )
215 2 1 34 12 167 deg1lt ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑗 ∈ ℕ0 ∧ ( 𝐷 ‘ 𝑥 ) < 𝑗 ) → ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) = ( 0g ‘ 𝑅 ) )
216 205 202 214 215 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) = ( 0g ‘ 𝑅 ) )
217 216 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
218 147 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
219 218 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
220 26 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → 𝑃 ∈ LMod )
221 94 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
222 100 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
223 90 91 221 202 222 mulgnn0cld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
224 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
225 34 38 39 224 13 lmod0vs ⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) )
226 220 223 225 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) )
227 219 226 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( ( 0g ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑃 ) )
228 204 217 227 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑗 ) → ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) = ( 0g ‘ 𝑃 ) )
229 4 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
230 229 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑁 ∈ ℤ )
231 198 228 230 suppssnn0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) supp ( 0g ‘ 𝑃 ) ) ⊆ ( 0 ..^ 𝑁 ) )
232 186 mptexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ V )
233 198 fnfund ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → Fun ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
234 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0g ‘ 𝑃 ) ∈ V )
235 suppssfifsupp ⊢ ( ( ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∈ V ∧ Fun ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V ) ∧ ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) supp ( 0g ‘ 𝑃 ) ) ⊆ ( 0 ..^ 𝑁 ) ) ) → ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) finSupp ( 0g ‘ 𝑃 ) )
236 232 233 234 179 231 235 syl32anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) finSupp ( 0g ‘ 𝑃 ) )
237 34 13 184 186 196 231 236 gsumres ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑃 Σg ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) ) = ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) )
238 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( coe1 ‘ 𝑥 ) ∈ V )
239 ovexd ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ V )
240 154 239 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
241 240 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐹 ∈ V )
242 offres ⊢ ( ( ( coe1 ‘ 𝑥 ) ∈ V ∧ 𝐹 ∈ V ) → ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) )
243 238 241 242 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) )
244 169 ffnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( coe1 ‘ 𝑥 ) Fn ℕ0 )
245 154 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( 0 ..^ 𝑁 ) )
246 245 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐹 Fn ( 0 ..^ 𝑁 ) )
247 sseqin2 ⊢ ( ( 0 ..^ 𝑁 ) ⊆ ℕ0 ↔ ( ℕ0 ∩ ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) )
248 173 247 mpbi ⊢ ( ℕ0 ∩ ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 )
249 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) )
250 oveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
251 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
252 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ V )
253 7 250 251 252 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) = ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
254 244 246 186 165 248 249 253 ofval ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ‘ 𝑗 ) = ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
255 173 251 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ℕ0 )
256 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ V )
257 195 201 255 256 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) = ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑗 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
258 254 257 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ‘ 𝑗 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) )
259 258 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ‘ 𝑗 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) )
260 244 246 186 165 248 offn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) Fn ( 0 ..^ 𝑁 ) )
261 ssidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
262 fvreseq0 ⊢ ( ( ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) Fn ( 0 ..^ 𝑁 ) ∧ ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) Fn ℕ0 ) ∧ ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) ∧ ( 0 ..^ 𝑁 ) ⊆ ℕ0 ) ) → ( ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ‘ 𝑗 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) ) )
263 260 198 261 174 262 syl22anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ‘ 𝑗 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) ) )
264 259 263 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( coe1 ‘ 𝑥 ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) )
265 fnresdm ⊢ ( 𝐹 Fn ( 0 ..^ 𝑁 ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) = 𝐹 )
266 245 265 syl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) = 𝐹 )
267 266 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) = 𝐹 )
268 267 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) = ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) )
269 243 264 268 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) = ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) )
270 269 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑃 Σg ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 𝑃 Σg ( ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) ) )
271 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑅 ∈ Ring )
272 1 98 34 39 89 91 167 ply1coe ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝑥 = ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) )
273 271 166 272 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 = ( 𝑃 Σg ( 𝑖 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑥 ) ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) )
274 237 270 273 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 = ( 𝑃 Σg ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) )
275 181 274 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 = ( 𝑃 Σg ( ( ( coe1 ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) )
276 163 176 275 rspcedvdw ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 = ( 𝑃 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) )
277 102 7 fmptd ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝑃 ) )
278 156 34 40 38 224 39 277 26 239 ellspd ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( LSpan ‘ 𝑃 ) ‘ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ↔ ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 = ( 𝑃 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ) )
279 278 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ( ( LSpan ‘ 𝑃 ) ‘ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ↔ ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 = ( 𝑃 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ) )
280 276 279 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( ( LSpan ‘ 𝑃 ) ‘ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
281 imadmrn ⊢ ( 𝐹 “ dom 𝐹 ) = ran 𝐹
282 154 fdmd ⊢ ( 𝜑 → dom 𝐹 = ( 0 ..^ 𝑁 ) )
283 282 imaeq2d ⊢ ( 𝜑 → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
284 281 283 eqtr3id ⊢ ( 𝜑 → ran 𝐹 = ( 𝐹 “ ( 0 ..^ 𝑁 ) ) )
285 284 fveq2d ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑃 ) ‘ ran 𝐹 ) = ( ( LSpan ‘ 𝑃 ) ‘ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
286 285 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( LSpan ‘ 𝑃 ) ‘ ran 𝐹 ) = ( ( LSpan ‘ 𝑃 ) ‘ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) )
287 280 286 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( ( LSpan ‘ 𝑃 ) ‘ ran 𝐹 ) )
288 158 287 eqelssd ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑃 ) ‘ ran 𝐹 ) = 𝑆 )
289 eqid ⊢ ( LSpan ‘ 𝐸 ) = ( LSpan ‘ 𝐸 )
290 6 156 289 28 lsslsp ⊢ ( ( 𝑃 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑃 ) ∧ ran 𝐹 ⊆ 𝑆 ) → ( ( LSpan ‘ 𝐸 ) ‘ ran 𝐹 ) = ( ( LSpan ‘ 𝑃 ) ‘ ran 𝐹 ) )
291 290 eqcomd ⊢ ( ( 𝑃 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑃 ) ∧ ran 𝐹 ⊆ 𝑆 ) → ( ( LSpan ‘ 𝑃 ) ‘ ran 𝐹 ) = ( ( LSpan ‘ 𝐸 ) ‘ ran 𝐹 ) )
292 26 27 155 291 syl3anc ⊢ ( 𝜑 → ( ( LSpan ‘ 𝑃 ) ‘ ran 𝐹 ) = ( ( LSpan ‘ 𝐸 ) ‘ ran 𝐹 ) )
293 288 292 46 3eqtr3d ⊢ ( 𝜑 → ( ( LSpan ‘ 𝐸 ) ‘ ran 𝐹 ) = ( Base ‘ 𝐸 ) )
294 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
295 2 fvexi ⊢ 𝐷 ∈ V
296 cnvexg ⊢ ( 𝐷 ∈ V → ◡ 𝐷 ∈ V )
297 imaexg ⊢ ( ◡ 𝐷 ∈ V → ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) ∈ V )
298 295 296 297 mp2b ⊢ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) ∈ V
299 3 298 eqeltri ⊢ 𝑆 ∈ V
300 6 38 resssca ⊢ ( 𝑆 ∈ V → ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝐸 ) )
301 299 300 ax-mp ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝐸 )
302 301 fveq2i ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝐸 ) )
303 eqid ⊢ ( Scalar ‘ 𝐸 ) = ( Scalar ‘ 𝐸 )
304 6 39 ressvsca ⊢ ( 𝑆 ∈ V → ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝐸 ) )
305 299 304 ax-mp ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝐸 )
306 eqid ⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
307 301 fveq2i ⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝐸 ) )
308 eqid ⊢ ( LBasis ‘ 𝐸 ) = ( LBasis ‘ 𝐸 )
309 6 28 lsslvec ⊢ ( ( 𝑃 ∈ LVec ∧ 𝑆 ∈ ( LSubSp ‘ 𝑃 ) ) → 𝐸 ∈ LVec )
310 25 27 309 syl2anc ⊢ ( 𝜑 → 𝐸 ∈ LVec )
311 310 lveclmodd ⊢ ( 𝜑 → 𝐸 ∈ LMod )
312 17 5 eqeltrrd ⊢ ( 𝜑 → ( Scalar ‘ 𝑃 ) ∈ DivRing )
313 drngnzr ⊢ ( ( Scalar ‘ 𝑃 ) ∈ DivRing → ( Scalar ‘ 𝑃 ) ∈ NzRing )
314 312 313 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝑃 ) ∈ NzRing )
315 301 314 eqeltrrid ⊢ ( 𝜑 → ( Scalar ‘ 𝐸 ) ∈ NzRing )
316 120 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐸 ) )
317 drngnzr ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
318 5 317 syl ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
319 318 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑅 ∈ NzRing )
320 97 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℕ0 )
321 elfzonn0 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ℕ0 )
322 321 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ℕ0 )
323 1 98 91 319 320 322 ply1moneq ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ↔ 𝑛 = 𝑖 ) )
324 323 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) )
325 324 anasss ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) )
326 325 ralrimivva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) )
327 oveq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
328 7 327 f1mpt ⊢ ( 𝐹 : ( 0 ..^ 𝑁 ) –1-1→ ( Base ‘ 𝐸 ) ↔ ( ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐸 ) ∧ ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) ) )
329 316 326 328 sylanbrc ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ 𝑁 ) –1-1→ ( Base ‘ 𝐸 ) )
330 294 302 303 305 306 307 308 289 311 315 239 329 islbs5 ⊢ ( 𝜑 → ( ran 𝐹 ∈ ( LBasis ‘ 𝐸 ) ↔ ( ∀ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑m ( 0 ..^ 𝑁 ) ) ( ( 𝑎 finSupp ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝐸 Σg ( 𝑎 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0g ‘ 𝐸 ) ) → 𝑎 = ( ( 0 ..^ 𝑁 ) × { ( 0g ‘ ( Scalar ‘ 𝑃 ) ) } ) ) ∧ ( ( LSpan ‘ 𝐸 ) ‘ ran 𝐹 ) = ( Base ‘ 𝐸 ) ) ) )
331 153 293 330 mpbir2and ⊢ ( 𝜑 → ran 𝐹 ∈ ( LBasis ‘ 𝐸 ) )