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

Metamath Proof Explorer

Theorem ply1degltdimlem

Proof