mplbas2

Description: An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Hypotheses	mplbas2.p	$⊢ P = I mPoly R$
	mplbas2.s	$⊢ S = I mPwSer R$
	mplbas2.v	$⊢ V = I mVar R$
	mplbas2.a	$⊢ A = AlgSpan (S)$
	mplbas2.i	$⊢ φ \to I \in W$
	mplbas2.r	$⊢ φ \to R \in CRing$
Assertion	mplbas2	$⊢ φ \to A (ran V) = {Base}_{P}$

Proof

Step	Hyp	Ref	Expression
1		mplbas2.p	$⊢ P = I mPoly R$
2		mplbas2.s	$⊢ S = I mPwSer R$
3		mplbas2.v	$⊢ V = I mVar R$
4		mplbas2.a	$⊢ A = AlgSpan (S)$
5		mplbas2.i	$⊢ φ \to I \in W$
6		mplbas2.r	$⊢ φ \to R \in CRing$
7	2 5 6	psrassa	$⊢ φ \to S \in AssAlg$
8		eqid	$⊢ {Base}_{P} = {Base}_{P}$
9		eqid	$⊢ {Base}_{S} = {Base}_{S}$
10	1 2 8 9	mplbasss	$⊢ {Base}_{P} \subseteq {Base}_{S}$
11	10	a1i	$⊢ φ \to {Base}_{P} \subseteq {Base}_{S}$
12		crngring	$⊢ R \in CRing \to R \in Ring$
13	6 12	syl	$⊢ φ \to R \in Ring$
14	2 3 9 5 13	mvrf	$⊢ φ \to V : I ⟶ {Base}_{S}$
15	14	ffnd	$⊢ φ \to V Fn I$
16	5	adantr	$⊢ (φ \land x \in I) \to I \in W$
17	13	adantr	$⊢ (φ \land x \in I) \to R \in Ring$
18		simpr	$⊢ (φ \land x \in I) \to x \in I$
19	1 3 8 16 17 18	mvrcl	$⊢ (φ \land x \in I) \to V (x) \in {Base}_{P}$
20	19	ralrimiva	$⊢ φ \to \forall x \in I V (x) \in {Base}_{P}$
21		ffnfv	$⊢ V : I ⟶ {Base}_{P} \leftrightarrow (V Fn I \land \forall x \in I V (x) \in {Base}_{P})$
22	15 20 21	sylanbrc	$⊢ φ \to V : I ⟶ {Base}_{P}$
23	22	frnd	$⊢ φ \to ran V \subseteq {Base}_{P}$
24	4 9	aspss	$⊢ (S \in AssAlg \land {Base}_{P} \subseteq {Base}_{S} \land ran V \subseteq {Base}_{P}) \to A (ran V) \subseteq A ({Base}_{P})$
25	7 11 23 24	syl3anc	$⊢ φ \to A (ran V) \subseteq A ({Base}_{P})$
26	2 1 8 5 13	mplsubrg	$⊢ φ \to {Base}_{P} \in SubRing (S)$
27	2 1 8 5 13	mpllss	$⊢ φ \to {Base}_{P} \in LSubSp (S)$
28		eqid	$⊢ LSubSp (S) = LSubSp (S)$
29	4 9 28	aspid	$⊢ (S \in AssAlg \land {Base}_{P} \in SubRing (S) \land {Base}_{P} \in LSubSp (S)) \to A ({Base}_{P}) = {Base}_{P}$
30	7 26 27 29	syl3anc	$⊢ φ \to A ({Base}_{P}) = {Base}_{P}$
31	25 30	sseqtrd	$⊢ φ \to A (ran V) \subseteq {Base}_{P}$
32		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
33		eqid	$⊢ 0_{R} = 0_{R}$
34		eqid	$⊢ 1_{R} = 1_{R}$
35	5	adantr	$⊢ (φ \land x \in {Base}_{P}) \to I \in W$
36		eqid	$⊢ \cdot_{P} = \cdot_{P}$
37	13	adantr	$⊢ (φ \land x \in {Base}_{P}) \to R \in Ring$
38		simpr	$⊢ (φ \land x \in {Base}_{P}) \to x \in {Base}_{P}$
39	1 32 33 34 35 8 36 37 38	mplcoe1	$⊢ (φ \land x \in {Base}_{P}) \to x = \underset{k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}{\sum_{P}} (x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})))$
40		eqid	$⊢ 0_{P} = 0_{P}$
41	1	mplring	$⊢ (I \in W \land R \in Ring) \to P \in Ring$
42	5 13 41	syl2anc	$⊢ φ \to P \in Ring$
43		ringabl	$⊢ P \in Ring \to P \in Abel$
44	42 43	syl	$⊢ φ \to P \in Abel$
45	44	adantr	$⊢ (φ \land x \in {Base}_{P}) \to P \in Abel$
46		ovex	$⊢ {ℕ_{0}}^{I} \in V$
47	46	rabex	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
48	47	a1i	$⊢ (φ \land x \in {Base}_{P}) \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
49	14	frnd	$⊢ φ \to ran V \subseteq {Base}_{S}$
50	4 9	aspsubrg	$⊢ (S \in AssAlg \land ran V \subseteq {Base}_{S}) \to A (ran V) \in SubRing (S)$
51	7 49 50	syl2anc	$⊢ φ \to A (ran V) \in SubRing (S)$
52	1 2 8	mplval2	$⊢ P = S ↾_{𝑠} {Base}_{P}$
53	52	subsubrg	$⊢ {Base}_{P} \in SubRing (S) \to (A (ran V) \in SubRing (P) \leftrightarrow (A (ran V) \in SubRing (S) \land A (ran V) \subseteq {Base}_{P}))$
54	26 53	syl	$⊢ φ \to (A (ran V) \in SubRing (P) \leftrightarrow (A (ran V) \in SubRing (S) \land A (ran V) \subseteq {Base}_{P}))$
55	51 31 54	mpbir2and	$⊢ φ \to A (ran V) \in SubRing (P)$
56		subrgsubg	$⊢ A (ran V) \in SubRing (P) \to A (ran V) \in SubGrp (P)$
57	55 56	syl	$⊢ φ \to A (ran V) \in SubGrp (P)$
58	57	adantr	$⊢ (φ \land x \in {Base}_{P}) \to A (ran V) \in SubGrp (P)$
59	1	mpllmod	$⊢ (I \in W \land R \in Ring) \to P \in LMod$
60	5 13 59	syl2anc	$⊢ φ \to P \in LMod$
61	60	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to P \in LMod$
62	4 9 28	asplss	$⊢ (S \in AssAlg \land ran V \subseteq {Base}_{S}) \to A (ran V) \in LSubSp (S)$
63	7 49 62	syl2anc	$⊢ φ \to A (ran V) \in LSubSp (S)$
64	2 5 13	psrlmod	$⊢ φ \to S \in LMod$
65		eqid	$⊢ LSubSp (P) = LSubSp (P)$
66	52 28 65	lsslss	$⊢ (S \in LMod \land {Base}_{P} \in LSubSp (S)) \to (A (ran V) \in LSubSp (P) \leftrightarrow (A (ran V) \in LSubSp (S) \land A (ran V) \subseteq {Base}_{P}))$
67	64 27 66	syl2anc	$⊢ φ \to (A (ran V) \in LSubSp (P) \leftrightarrow (A (ran V) \in LSubSp (S) \land A (ran V) \subseteq {Base}_{P}))$
68	63 31 67	mpbir2and	$⊢ φ \to A (ran V) \in LSubSp (P)$
69	68	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to A (ran V) \in LSubSp (P)$
70		eqid	$⊢ {Base}_{R} = {Base}_{R}$
71	1 70 8 32 38	mplelf	$⊢ (φ \land x \in {Base}_{P}) \to x : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
72	71	ffvelcdmda	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to x (k) \in {Base}_{R}$
73	1 35 37	mplsca	$⊢ (φ \land x \in {Base}_{P}) \to R = Scalar (P)$
74	73	adantr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to R = Scalar (P)$
75	74	fveq2d	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to {Base}_{R} = {Base}_{Scalar (P)}$
76	72 75	eleqtrd	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to x (k) \in {Base}_{Scalar (P)}$
77	5	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to I \in W$
78		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
79		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
80	6	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to R \in CRing$
81		simpr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
82	1 32 33 34 77 78 79 3 80 81	mplcoe2	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) = \underset{z \in I}{\sum_{{mulGrp}_{P}}} (k (z) \cdot_{{mulGrp}_{P}} V (z))$
83		eqid	$⊢ 1_{P} = 1_{P}$
84	78 83	ringidval	$⊢ 1_{P} = 0_{{mulGrp}_{P}}$
85	1	mplcrng	$⊢ (I \in W \land R \in CRing) \to P \in CRing$
86	5 6 85	syl2anc	$⊢ φ \to P \in CRing$
87	78	crngmgp	$⊢ P \in CRing \to {mulGrp}_{P} \in CMnd$
88	86 87	syl	$⊢ φ \to {mulGrp}_{P} \in CMnd$
89	88	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to {mulGrp}_{P} \in CMnd$
90	55	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to A (ran V) \in SubRing (P)$
91	78	subrgsubm	$⊢ A (ran V) \in SubRing (P) \to A (ran V) \in SubMnd ({mulGrp}_{P})$
92	90 91	syl	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to A (ran V) \in SubMnd ({mulGrp}_{P})$
93		simplll	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in I) \to φ$
94	32	psrbag	$⊢ I \in W \to (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \leftrightarrow (k : I ⟶ ℕ_{0} \land k^{-1} [ℕ] \in Fin))$
95	35 94	syl	$⊢ (φ \land x \in {Base}_{P}) \to (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \leftrightarrow (k : I ⟶ ℕ_{0} \land k^{-1} [ℕ] \in Fin))$
96	95	biimpa	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to (k : I ⟶ ℕ_{0} \land k^{-1} [ℕ] \in Fin)$
97	96	simpld	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to k : I ⟶ ℕ_{0}$
98	97	ffvelcdmda	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in I) \to k (z) \in ℕ_{0}$
99	4 9	aspssid	$⊢ (S \in AssAlg \land ran V \subseteq {Base}_{S}) \to ran V \subseteq A (ran V)$
100	7 49 99	syl2anc	$⊢ φ \to ran V \subseteq A (ran V)$
101	100	ad3antrrr	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in I) \to ran V \subseteq A (ran V)$
102	15	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to V Fn I$
103		fnfvelrn	$⊢ (V Fn I \land z \in I) \to V (z) \in ran V$
104	102 103	sylan	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in I) \to V (z) \in ran V$
105	101 104	sseldd	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in I) \to V (z) \in A (ran V)$
106	78 8	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
107		eqid	$⊢ \cdot_{P} = \cdot_{P}$
108	78 107	mgpplusg	$⊢ \cdot_{P} = +_{{mulGrp}_{P}}$
109	107	subrgmcl	$⊢ (A (ran V) \in SubRing (P) \land u \in A (ran V) \land v \in A (ran V)) \to u \cdot_{P} v \in A (ran V)$
110	55 109	syl3an1	$⊢ (φ \land u \in A (ran V) \land v \in A (ran V)) \to u \cdot_{P} v \in A (ran V)$
111	83	subrg1cl	$⊢ A (ran V) \in SubRing (P) \to 1_{P} \in A (ran V)$
112	55 111	syl	$⊢ φ \to 1_{P} \in A (ran V)$
113	106 79 108 88 31 110 84 112	mulgnn0subcl	$⊢ (φ \land k (z) \in ℕ_{0} \land V (z) \in A (ran V)) \to k (z) \cdot_{{mulGrp}_{P}} V (z) \in A (ran V)$
114	93 98 105 113	syl3anc	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in I) \to k (z) \cdot_{{mulGrp}_{P}} V (z) \in A (ran V)$
115	114	fmpttd	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to (z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z)) : I ⟶ A (ran V)$
116	5	mptexd	$⊢ φ \to (z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z)) \in V$
117	116	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to (z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z)) \in V$
118		funmpt	$⊢ Fun (z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z))$
119	118	a1i	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to Fun (z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z))$
120		fvexd	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to 1_{P} \in V$
121	96	simprd	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to k^{-1} [ℕ] \in Fin$
122		elrabi	$⊢ k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \to k \in ({ℕ_{0}}^{I})$
123		elmapi	$⊢ k \in ({ℕ_{0}}^{I}) \to k : I ⟶ ℕ_{0}$
124	123	adantl	$⊢ ((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \to k : I ⟶ ℕ_{0}$
125	5	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \to I \in W$
126		fcdmnn0supp	$⊢ (I \in W \land k : I ⟶ ℕ_{0}) \to k supp 0 = k^{-1} [ℕ]$
127	125 124 126	syl2anc	$⊢ ((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \to k supp 0 = k^{-1} [ℕ]$
128		eqimss	$⊢ k supp 0 = k^{-1} [ℕ] \to k supp 0 \subseteq k^{-1} [ℕ]$
129	127 128	syl	$⊢ ((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \to k supp 0 \subseteq k^{-1} [ℕ]$
130		c0ex	$⊢ 0 \in V$
131	130	a1i	$⊢ ((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \to 0 \in V$
132	124 129 125 131	suppssr	$⊢ (((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \land z \in (I ∖ k^{-1} [ℕ])) \to k (z) = 0$
133	122 132	sylanl2	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in (I ∖ k^{-1} [ℕ])) \to k (z) = 0$
134	133	oveq1d	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in (I ∖ k^{-1} [ℕ])) \to k (z) \cdot_{{mulGrp}_{P}} V (z) = 0 \cdot_{{mulGrp}_{P}} V (z)$
135	5	ad3antrrr	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in (I ∖ k^{-1} [ℕ])) \to I \in W$
136	13	ad3antrrr	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in (I ∖ k^{-1} [ℕ])) \to R \in Ring$
137		eldifi	$⊢ z \in (I ∖ k^{-1} [ℕ]) \to z \in I$
138	137	adantl	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in (I ∖ k^{-1} [ℕ])) \to z \in I$
139	1 3 8 135 136 138	mvrcl	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in (I ∖ k^{-1} [ℕ])) \to V (z) \in {Base}_{P}$
140	106 84 79	mulg0	$⊢ V (z) \in {Base}_{P} \to 0 \cdot_{{mulGrp}_{P}} V (z) = 1_{P}$
141	139 140	syl	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in (I ∖ k^{-1} [ℕ])) \to 0 \cdot_{{mulGrp}_{P}} V (z) = 1_{P}$
142	134 141	eqtrd	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in (I ∖ k^{-1} [ℕ])) \to k (z) \cdot_{{mulGrp}_{P}} V (z) = 1_{P}$
143	142 77	suppss2	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to (z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z)) supp 1_{P} \subseteq k^{-1} [ℕ]$
144		suppssfifsupp	$⊢ (((z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z)) \in V \land Fun (z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z)) \land 1_{P} \in V) \land (k^{-1} [ℕ] \in Fin \land (z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z)) supp 1_{P} \subseteq k^{-1} [ℕ])) \to {finSupp}_{1_{P}} ((z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z)))$
145	117 119 120 121 143 144	syl32anc	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to {finSupp}_{1_{P}} ((z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z)))$
146	84 89 77 92 115 145	gsumsubmcl	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to \underset{z \in I}{\sum_{{mulGrp}_{P}}} (k (z) \cdot_{{mulGrp}_{P}} V (z)) \in A (ran V)$
147	82 146	eqeltrd	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) \in A (ran V)$
148		eqid	$⊢ Scalar (P) = Scalar (P)$
149		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
150	148 36 149 65	lssvscl	$⊢ ((P \in LMod \land A (ran V) \in LSubSp (P)) \land (x (k) \in {Base}_{Scalar (P)} \land (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) \in A (ran V))) \to x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) \in A (ran V)$
151	61 69 76 147 150	syl22anc	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) \in A (ran V)$
152	151	fmpttd	$⊢ (φ \land x \in {Base}_{P}) \to (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ A (ran V)$
153	46	mptrabex	$⊢ (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) \in V$
154		funmpt	$⊢ Fun (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})))$
155		fvex	$⊢ 0_{P} \in V$
156	153 154 155	3pm3.2i	$⊢ ((k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) \in V \land Fun (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) \land 0_{P} \in V)$
157	156	a1i	$⊢ (φ \land x \in {Base}_{P}) \to ((k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) \in V \land Fun (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) \land 0_{P} \in V)$
158	1 2 9 33 8	mplelbas	$⊢ x \in {Base}_{P} \leftrightarrow (x \in {Base}_{S} \land {finSupp}_{0_{R}} (x))$
159	158	simprbi	$⊢ x \in {Base}_{P} \to {finSupp}_{0_{R}} (x)$
160	159	adantl	$⊢ (φ \land x \in {Base}_{P}) \to {finSupp}_{0_{R}} (x)$
161	160	fsuppimpd	$⊢ (φ \land x \in {Base}_{P}) \to x supp 0_{R} \in Fin$
162		ssidd	$⊢ (φ \land x \in {Base}_{P}) \to x supp 0_{R} \subseteq x supp 0_{R}$
163		fvexd	$⊢ (φ \land x \in {Base}_{P}) \to 0_{R} \in V$
164	71 162 48 163	suppssr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ {supp}_{0_{R}} (x))) \to x (k) = 0_{R}$
165	73	fveq2d	$⊢ (φ \land x \in {Base}_{P}) \to 0_{R} = 0_{Scalar (P)}$
166	165	adantr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ {supp}_{0_{R}} (x))) \to 0_{R} = 0_{Scalar (P)}$
167	164 166	eqtrd	$⊢ ((φ \land x \in {Base}_{P}) \land k \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ {supp}_{0_{R}} (x))) \to x (k) = 0_{Scalar (P)}$
168	167	oveq1d	$⊢ ((φ \land x \in {Base}_{P}) \land k \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ {supp}_{0_{R}} (x))) \to x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) = 0_{Scalar (P)} \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))$
169		eldifi	$⊢ k \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ {supp}_{0_{R}} (x)) \to k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
170	13	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to R \in Ring$
171	1 8 33 34 32 77 170 81	mplmon	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) \in {Base}_{P}$
172		eqid	$⊢ 0_{Scalar (P)} = 0_{Scalar (P)}$
173	8 148 36 172 40	lmod0vs	$⊢ (P \in LMod \land (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) \in {Base}_{P}) \to 0_{Scalar (P)} \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) = 0_{P}$
174	61 171 173	syl2anc	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to 0_{Scalar (P)} \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) = 0_{P}$
175	169 174	sylan2	$⊢ ((φ \land x \in {Base}_{P}) \land k \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ {supp}_{0_{R}} (x))) \to 0_{Scalar (P)} \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) = 0_{P}$
176	168 175	eqtrd	$⊢ ((φ \land x \in {Base}_{P}) \land k \in (\{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ∖ {supp}_{0_{R}} (x))) \to x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R})) = 0_{P}$
177	176 48	suppss2	$⊢ (φ \land x \in {Base}_{P}) \to (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) supp 0_{P} \subseteq x supp 0_{R}$
178		suppssfifsupp	$⊢ (((k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) \in V \land Fun (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) \land 0_{P} \in V) \land (x supp 0_{R} \in Fin \land (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) supp 0_{P} \subseteq x supp 0_{R})) \to {finSupp}_{0_{P}} ((k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))))$
179	157 161 177 178	syl12anc	$⊢ (φ \land x \in {Base}_{P}) \to {finSupp}_{0_{P}} ((k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))))$
180	40 45 48 58 152 179	gsumsubgcl	$⊢ (φ \land x \in {Base}_{P}) \to \underset{k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}}{\sum_{P}} (x (k) \cdot_{P} (y \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (y = k, 1_{R}, 0_{R}))) \in A (ran V)$
181	39 180	eqeltrd	$⊢ (φ \land x \in {Base}_{P}) \to x \in A (ran V)$
182	31 181	eqelssd	$⊢ φ \to A (ran V) = {Base}_{P}$

Metamath Proof Explorer

Theorem mplbas2

Proof