ply1degltdimlem

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

Proof

Step	Hyp	Ref	Expression
1		ply1degltdim.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		ply1degltdim.d	⊢ 𝐷 = ( deg₁ ‘ 𝑅 )
3		ply1degltdim.s	⊢ 𝑆 = ( ^◡ 𝐷 “ ( -∞ [,) 𝑁 ) )
4		ply1degltdim.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
5		ply1degltdim.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
6		ply1degltdim.e	⊢ 𝐸 = ( 𝑃 ↾_s 𝑆 )
7		ply1degltdimlem.f	⊢ 𝐹 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) )
8		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9	4	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝑁 ∈ ℕ₀ )
10	5	drngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
11	10	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝑅 ∈ Ring )
12		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
13		eqid	⊢ ( 0_g ‘ 𝑃 ) = ( 0_g ‘ 𝑃 )
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 ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝑎 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
23		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) )
24		ovexd	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → ( 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 ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝑆 ∈ ( 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 ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) ) → ( 𝑘 ( ·_𝑠 ‘ 𝑃 ) 𝑥 ) ∈ 𝑆 )
87	15	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝑎 : ( 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 ..^ 𝑁 ) → 𝑛 ∈ ℕ₀ )
97	96	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℕ₀ )
98		eqid	⊢ ( var₁ ‘ 𝑅 ) = ( var₁ ‘ 𝑅 )
99	98 1 34	vr1cl	⊢ ( 𝑅 ∈ Ring → ( var₁ ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
100	10 99	syl	⊢ ( 𝜑 → ( var₁ ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
101	100	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( var₁ ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
102	90 91 95 97 101	mulgnn0cld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
103	51	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → -∞ ∈ ℝ^* )
104	54	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ^* )
105	2 1 34	deg1xrcl	⊢ ( ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) → ( 𝐷 ‘ ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ∈ ℝ^* )
106	102 105	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ∈ ℝ^* )
107	106	mnfled	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → -∞ ≤ ( 𝐷 ‘ ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) )
108	96	nn0red	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 ∈ ℝ )
109	108	rexrd	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 ∈ ℝ^* )
110	109	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℝ^* )
111	2 1 98 89 91	deg1pwle	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ₀ ) → ( 𝐷 ‘ ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ≤ 𝑛 )
112	10 96 111	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ≤ 𝑛 )
113		elfzolt2	⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 < 𝑁 )
114	113	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 < 𝑁 )
115	106 110 104 112 114	xrlelttrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) < 𝑁 )
116	103 104 106 107 115	elicod	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ∈ ( -∞ [,) 𝑁 ) )
117	88 102 116	elpreimad	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ ( ^◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
118	117 3	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ 𝑆 )
119	46	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 = ( Base ‘ 𝐸 ) )
120	118 119	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐸 ) )
121	120 7	fmptd	⊢ ( 𝜑 → 𝐹 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝐸 ) )
122	121	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝐹 : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝐸 ) )
123		inidm	⊢ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 )
124	86 87 122 24 24 123	off	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑆 )
125	24 33 124 6	gsumsubm	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → ( 𝑃 Σ_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 → ( 0_g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
130	127 129	syl	⊢ ( 𝜑 → ( 0_g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
131	51	a1i	⊢ ( 𝜑 → -∞ ∈ ℝ^* )
132	2 1 34	deg1xrcl	⊢ ( ( 0_g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) → ( 𝐷 ‘ ( 0_g ‘ 𝑃 ) ) ∈ ℝ^* )
133	130 132	syl	⊢ ( 𝜑 → ( 𝐷 ‘ ( 0_g ‘ 𝑃 ) ) ∈ ℝ^* )
134	133	mnfled	⊢ ( 𝜑 → -∞ ≤ ( 𝐷 ‘ ( 0_g ‘ 𝑃 ) ) )
135	2 1 13	deg1z	⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ ( 0_g ‘ 𝑃 ) ) = -∞ )
136	10 135	syl	⊢ ( 𝜑 → ( 𝐷 ‘ ( 0_g ‘ 𝑃 ) ) = -∞ )
137	53	mnfltd	⊢ ( 𝜑 → -∞ < 𝑁 )
138	136 137	eqbrtrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 0_g ‘ 𝑃 ) ) < 𝑁 )
139	131 54 133 134 138	elicod	⊢ ( 𝜑 → ( 𝐷 ‘ ( 0_g ‘ 𝑃 ) ) ∈ ( -∞ [,) 𝑁 ) )
140	128 130 139	elpreimad	⊢ ( 𝜑 → ( 0_g ‘ 𝑃 ) ∈ ( ^◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
141	140 3	eleqtrrdi	⊢ ( 𝜑 → ( 0_g ‘ 𝑃 ) ∈ 𝑆 )
142	6 34 13	ress0g	⊢ ( ( 𝑃 ∈ Mnd ∧ ( 0_g ‘ 𝑃 ) ∈ 𝑆 ∧ 𝑆 ⊆ ( Base ‘ 𝑃 ) ) → ( 0_g ‘ 𝑃 ) = ( 0_g ‘ 𝐸 ) )
143	127 141 44 142	syl3anc	⊢ ( 𝜑 → ( 0_g ‘ 𝑃 ) = ( 0_g ‘ 𝐸 ) )
144	143	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → ( 0_g ‘ 𝑃 ) = ( 0_g ‘ 𝐸 ) )
145	23 125 144	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → ( 𝑃 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝑃 ) )
146	1 8 9 11 7 12 13 22 145	ply1gsumz	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝑎 = ( ( 0 ..^ 𝑁 ) × { ( 0_g ‘ 𝑅 ) } ) )
147	17	fveq2d	⊢ ( 𝜑 → ( 0_g ‘ 𝑅 ) = ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) )
148	147	sneqd	⊢ ( 𝜑 → { ( 0_g ‘ 𝑅 ) } = { ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) } )
149	148	xpeq2d	⊢ ( 𝜑 → ( ( 0 ..^ 𝑁 ) × { ( 0_g ‘ 𝑅 ) } ) = ( ( 0 ..^ 𝑁 ) × { ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) } ) )
150	149	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → ( ( 0 ..^ 𝑁 ) × { ( 0_g ‘ 𝑅 ) } ) = ( ( 0 ..^ 𝑁 ) × { ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) } ) )
151	146 150	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) ∧ 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝑎 = ( ( 0 ..^ 𝑁 ) × { ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) } ) )
152	151	expl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ) → ( ( 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝑎 = ( ( 0 ..^ 𝑁 ) × { ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) } ) ) )
153	152	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ( ( 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝑎 = ( ( 0 ..^ 𝑁 ) × { ( 0_g ‘ ( 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	⊢ ( 𝑎 = ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) → ( 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ) )
160		oveq1	⊢ ( 𝑎 = ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) → ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) = ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) )
161	160	oveq2d	⊢ ( 𝑎 = ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) → ( 𝑃 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 𝑃 Σ_g ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) )
162	161	eqeq2d	⊢ ( 𝑎 = ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) → ( 𝑥 = ( 𝑃 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) ↔ 𝑥 = ( 𝑃 Σ_g ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) ) )
163	159 162	anbi12d	⊢ ( 𝑎 = ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) → ( ( 𝑎 finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 = ( 𝑃 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ↔ ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 = ( 𝑃 Σ_g ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ) )
164		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∈ V )
165		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0 ..^ 𝑁 ) ∈ V )
166	44	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
167		eqid	⊢ ( coe₁ ‘ 𝑥 ) = ( coe₁ ‘ 𝑥 )
168	167 34 1 8	coe1f	⊢ ( 𝑥 ∈ ( Base ‘ 𝑃 ) → ( coe₁ ‘ 𝑥 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
169	166 168	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( coe₁ ‘ 𝑥 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
170	18	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
171	170	feq3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( coe₁ ‘ 𝑥 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) ↔ ( coe₁ ‘ 𝑥 ) : ℕ₀ ⟶ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
172	169 171	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( coe₁ ‘ 𝑥 ) : ℕ₀ ⟶ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
173		fzo0ssnn0	⊢ ( 0 ..^ 𝑁 ) ⊆ ℕ₀
174	173	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0 ..^ 𝑁 ) ⊆ ℕ₀ )
175	172 174	fssresd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
176	164 165 175	elmapdd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) )
177	169	ffund	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → Fun ( coe₁ ‘ 𝑥 ) )
178		fzofi	⊢ ( 0 ..^ 𝑁 ) ∈ Fin
179	178	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0 ..^ 𝑁 ) ∈ Fin )
180		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ∈ V )
181	177 179 180	resfifsupp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) )
182		ringcmn	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
183	10 92 182	3syl	⊢ ( 𝜑 → 𝑃 ∈ CMnd )
184	183	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑃 ∈ CMnd )
185		nn0ex	⊢ ℕ₀ ∈ V
186	185	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ℕ₀ ∈ V )
187	26	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ₀ ) → 𝑃 ∈ LMod )
188	172	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ₀ ) → ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
189	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ₀ ) → 𝑅 ∈ Ring )
190	189 92 93	3syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ₀ ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
191		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ₀ ) → 𝑖 ∈ ℕ₀ )
192	189 99	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ₀ ) → ( var₁ ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
193	90 91 190 191 192	mulgnn0cld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ₀ ) → ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
194	34 38 39 40 187 188 193	lmodvscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ₀ ) → ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ∈ ( Base ‘ 𝑃 ) )
195		eqid	⊢ ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) = ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) )
196	194 195	fmptd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) : ℕ₀ ⟶ ( Base ‘ 𝑃 ) )
197		nfv	⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑥 ∈ 𝑆 )
198	197 194 195	fnmptd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) Fn ℕ₀ )
199		fveq2	⊢ ( 𝑖 = 𝑗 → ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) = ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) )
200		oveq1	⊢ ( 𝑖 = 𝑗 → ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) = ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) )
201	199 200	oveq12d	⊢ ( 𝑖 = 𝑗 → ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) = ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) )
202		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → 𝑗 ∈ ℕ₀ )
203		ovexd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ∈ V )
204	195 201 202 203	fvmptd3	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) = ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) )
205	166	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
206		icossxr	⊢ ( -∞ [,) 𝑁 ) ⊆ ℝ^*
207	206 75	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐷 ‘ 𝑥 ) ∈ ℝ^* )
208	207	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( 𝐷 ‘ 𝑥 ) ∈ ℝ^* )
209	54	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → 𝑁 ∈ ℝ^* )
210	202	nn0red	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → 𝑗 ∈ ℝ )
211	210	rexrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → 𝑗 ∈ ℝ^* )
212	79	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( 𝐷 ‘ 𝑥 ) < 𝑁 )
213		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → 𝑁 ≤ 𝑗 )
214	208 209 211 212 213	xrltletrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( 𝐷 ‘ 𝑥 ) < 𝑗 )
215	2 1 34 12 167	deg1lt	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑗 ∈ ℕ₀ ∧ ( 𝐷 ‘ 𝑥 ) < 𝑗 ) → ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) = ( 0_g ‘ 𝑅 ) )
216	205 202 214 215	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) = ( 0_g ‘ 𝑅 ) )
217	216	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) = ( ( 0_g ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) )
218	147	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( 0_g ‘ 𝑅 ) = ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) )
219	218	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( ( 0_g ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) = ( ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) )
220	26	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → 𝑃 ∈ LMod )
221	94	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
222	100	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( var₁ ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
223	90 91 221 202 222	mulgnn0cld	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
224		eqid	⊢ ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0_g ‘ ( Scalar ‘ 𝑃 ) )
225	34 38 39 224 13	lmod0vs	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) = ( 0_g ‘ 𝑃 ) )
226	220 223 225	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) = ( 0_g ‘ 𝑃 ) )
227	219 226	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( ( 0_g ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) = ( 0_g ‘ 𝑃 ) )
228	204 217 227	3eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) ∧ 𝑁 ≤ 𝑗 ) → ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) = ( 0_g ‘ 𝑃 ) )
229	4	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
230	229	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑁 ∈ ℤ )
231	198 228 230	suppssnn0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) supp ( 0_g ‘ 𝑃 ) ) ⊆ ( 0 ..^ 𝑁 ) )
232	186	mptexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ∈ V )
233	198	fnfund	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → Fun ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) )
234		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0_g ‘ 𝑃 ) ∈ V )
235		suppssfifsupp	⊢ ( ( ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ∈ V ∧ Fun ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ∧ ( 0_g ‘ 𝑃 ) ∈ V ) ∧ ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) supp ( 0_g ‘ 𝑃 ) ) ⊆ ( 0 ..^ 𝑁 ) ) ) → ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) finSupp ( 0_g ‘ 𝑃 ) )
236	232 233 234 179 231 235	syl32anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) finSupp ( 0_g ‘ 𝑃 ) )
237	34 13 184 186 196 231 236	gsumres	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑃 Σ_g ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) ) = ( 𝑃 Σ_g ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ) )
238		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( coe₁ ‘ 𝑥 ) ∈ V )
239		ovexd	⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ V )
240	154 239	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
241	240	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐹 ∈ V )
242		offres	⊢ ( ( ( coe₁ ‘ 𝑥 ) ∈ V ∧ 𝐹 ∈ V ) → ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) )
243	238 241 242	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) )
244	169	ffnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( coe₁ ‘ 𝑥 ) Fn ℕ₀ )
245	154	ffnd	⊢ ( 𝜑 → 𝐹 Fn ( 0 ..^ 𝑁 ) )
246	245	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐹 Fn ( 0 ..^ 𝑁 ) )
247		sseqin2	⊢ ( ( 0 ..^ 𝑁 ) ⊆ ℕ₀ ↔ ( ℕ₀ ∩ ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) )
248	173 247	mpbi	⊢ ( ℕ₀ ∩ ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 )
249		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ₀ ) → ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) = ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) )
250		oveq1	⊢ ( 𝑛 = 𝑗 → ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) = ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) )
251		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
252		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ V )
253	7 250 251 252	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) = ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) )
254	244 246 186 165 248 249 253	ofval	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ‘ 𝑗 ) = ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) )
255	173 251	sselid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ℕ₀ )
256		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ∈ V )
257	195 201 255 256	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) = ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑗 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑗 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) )
258	254 257	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ‘ 𝑗 ) = ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) )
259	258	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ‘ 𝑗 ) = ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) )
260	244 246 186 165 248	offn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) Fn ( 0 ..^ 𝑁 ) )
261		ssidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) )
262		fvreseq0	⊢ ( ( ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) Fn ( 0 ..^ 𝑁 ) ∧ ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) Fn ℕ₀ ) ∧ ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ 𝑁 ) ∧ ( 0 ..^ 𝑁 ) ⊆ ℕ₀ ) ) → ( ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ‘ 𝑗 ) = ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) ) )
263	260 198 261 174 262	syl22anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) ↔ ∀ 𝑗 ∈ ( 0 ..^ 𝑁 ) ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ‘ 𝑗 ) = ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ‘ 𝑗 ) ) )
264	259 263	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( coe₁ ‘ 𝑥 ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) )
265		fnresdm	⊢ ( 𝐹 Fn ( 0 ..^ 𝑁 ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) = 𝐹 )
266	245 265	syl	⊢ ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) = 𝐹 )
267	266	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) = 𝐹 )
268	267	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) = ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) )
269	243 264 268	3eqtr3rd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) = ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) )
270	269	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑃 Σ_g ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 𝑃 Σ_g ( ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ↾ ( 0 ..^ 𝑁 ) ) ) )
271	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑅 ∈ Ring )
272	1 98 34 39 89 91 167	ply1coe	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑃 ) ) → 𝑥 = ( 𝑃 Σ_g ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ) )
273	271 166 272	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 = ( 𝑃 Σ_g ( 𝑖 ∈ ℕ₀ ↦ ( ( ( coe₁ ‘ 𝑥 ) ‘ 𝑖 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ) ) ) )
274	237 270 273	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 = ( 𝑃 Σ_g ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) )
275	181 274	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) finSupp ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 = ( 𝑃 Σ_g ( ( ( coe₁ ‘ 𝑥 ) ↾ ( 0 ..^ 𝑁 ) ) ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) ) )
276	163 176 275	rspcedvdw	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ( 𝑎 finSupp ( 0_g ‘ ( 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 ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑥 = ( 𝑃 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ) )
279	278	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ ( ( LSpan ‘ 𝑃 ) ‘ ( 𝐹 “ ( 0 ..^ 𝑁 ) ) ) ↔ ∃ 𝑎 ∈ ( ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↑_m ( 0 ..^ 𝑁 ) ) ( 𝑎 finSupp ( 0_g ‘ ( 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	⊢ ( 0_g ‘ 𝐸 ) = ( 0_g ‘ 𝐸 )
307	301	fveq2i	⊢ ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0_g ‘ ( 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 ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐸 ) )
317		drngnzr	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
318	5 317	syl	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
319	318	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑅 ∈ NzRing )
320	97	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℕ₀ )
321		elfzonn0	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ℕ₀ )
322	321	adantl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ℕ₀ )
323	1 98 91 319 320 322	ply1moneq	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) = ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ↔ 𝑛 = 𝑖 ) )
324	323	biimpd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) = ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) )
325	324	anasss	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) = ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) )
326	325	ralrimivva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) = ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) )
327		oveq1	⊢ ( 𝑛 = 𝑖 → ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) = ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) )
328	7 327	f1mpt	⊢ ( 𝐹 : ( 0 ..^ 𝑁 ) –1-1→ ( Base ‘ 𝐸 ) ↔ ( ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐸 ) ∧ ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑛 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) = ( 𝑖 ( ._g ‘ ( mulGrp ‘ 𝑃 ) ) ( var₁ ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) ) )
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 ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝐸 Σ_g ( 𝑎 ∘_f ( ·_𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 0_g ‘ 𝐸 ) ) → 𝑎 = ( ( 0 ..^ 𝑁 ) × { ( 0_g ‘ ( Scalar ‘ 𝑃 ) ) } ) ) ∧ ( ( LSpan ‘ 𝐸 ) ‘ ran 𝐹 ) = ( Base ‘ 𝐸 ) ) ) )
331	153 293 330	mpbir2and	⊢ ( 𝜑 → ran 𝐹 ∈ ( LBasis ‘ 𝐸 ) )

Metamath Proof Explorer

Theorem ply1degltdimlem

Proof