ply1degltdimlem

	Ref	Expression
Hypotheses	ply1degltdim.p	$⊢ P = {Poly}_{1} (R)$
	ply1degltdim.d	$⊢ D = \deg_{1} (R)$
	ply1degltdim.s	$⊢ S = D^{-1} [[−∞, N)]$
	ply1degltdim.n	$⊢ φ \to N \in ℕ_{0}$
	ply1degltdim.r	$⊢ φ \to R \in DivRing$
	ply1degltdim.e	$⊢ E = P ↾_{𝑠} S$
	ply1degltdimlem.f	$⊢ F = (n \in (0 ..^N) ⟼ n \cdot_{{mulGrp}_{P}} {var}_{1} (R))$
Assertion	ply1degltdimlem	$⊢ φ \to ran F \in LBasis (E)$

Proof

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

Metamath Proof Explorer

Theorem ply1degltdimlem

Proof