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 5 13	mplringd	$⊢ φ \to P \in Ring$
42		ringabl	$⊢ P \in Ring \to P \in Abel$
43	41 42	syl	$⊢ φ \to P \in Abel$
44	43	adantr	$⊢ (φ \land x \in {Base}_{P}) \to P \in Abel$
45		ovex	$⊢ {ℕ_{0}}^{I} \in V$
46	45	rabex	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
47	46	a1i	$⊢ (φ \land x \in {Base}_{P}) \to \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
48	14	frnd	$⊢ φ \to ran V \subseteq {Base}_{S}$
49	4 9	aspsubrg	$⊢ (S \in AssAlg \land ran V \subseteq {Base}_{S}) \to A (ran V) \in SubRing (S)$
50	7 48 49	syl2anc	$⊢ φ \to A (ran V) \in SubRing (S)$
51	1 2 8	mplval2	$⊢ P = S ↾_{𝑠} {Base}_{P}$
52	51	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}))$
53	26 52	syl	$⊢ φ \to (A (ran V) \in SubRing (P) \leftrightarrow (A (ran V) \in SubRing (S) \land A (ran V) \subseteq {Base}_{P}))$
54	50 31 53	mpbir2and	$⊢ φ \to A (ran V) \in SubRing (P)$
55		subrgsubg	$⊢ A (ran V) \in SubRing (P) \to A (ran V) \in SubGrp (P)$
56	54 55	syl	$⊢ φ \to A (ran V) \in SubGrp (P)$
57	56	adantr	$⊢ (φ \land x \in {Base}_{P}) \to A (ran V) \in SubGrp (P)$
58	1 5 13	mpllmodd	$⊢ φ \to P \in LMod$
59	58	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to P \in LMod$
60	4 9 28	asplss	$⊢ (S \in AssAlg \land ran V \subseteq {Base}_{S}) \to A (ran V) \in LSubSp (S)$
61	7 48 60	syl2anc	$⊢ φ \to A (ran V) \in LSubSp (S)$
62	2 5 13	psrlmod	$⊢ φ \to S \in LMod$
63		eqid	$⊢ LSubSp (P) = LSubSp (P)$
64	51 28 63	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}))$
65	62 27 64	syl2anc	$⊢ φ \to (A (ran V) \in LSubSp (P) \leftrightarrow (A (ran V) \in LSubSp (S) \land A (ran V) \subseteq {Base}_{P}))$
66	61 31 65	mpbir2and	$⊢ φ \to A (ran V) \in LSubSp (P)$
67	66	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to A (ran V) \in LSubSp (P)$
68		eqid	$⊢ {Base}_{R} = {Base}_{R}$
69	1 68 8 32 38	mplelf	$⊢ (φ \land x \in {Base}_{P}) \to x : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
70	69	ffvelcdmda	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to x (k) \in {Base}_{R}$
71	1 35 37	mplsca	$⊢ (φ \land x \in {Base}_{P}) \to R = Scalar (P)$
72	71	adantr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to R = Scalar (P)$
73	72	fveq2d	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to {Base}_{R} = {Base}_{Scalar (P)}$
74	70 73	eleqtrd	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to x (k) \in {Base}_{Scalar (P)}$
75	5	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to I \in W$
76		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
77		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
78	6	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to R \in CRing$
79		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\}$
80	1 32 33 34 75 76 77 3 78 79	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))$
81		eqid	$⊢ 1_{P} = 1_{P}$
82	76 81	ringidval	$⊢ 1_{P} = 0_{{mulGrp}_{P}}$
83	1	mplcrng	$⊢ (I \in W \land R \in CRing) \to P \in CRing$
84	5 6 83	syl2anc	$⊢ φ \to P \in CRing$
85	76	crngmgp	$⊢ P \in CRing \to {mulGrp}_{P} \in CMnd$
86	84 85	syl	$⊢ φ \to {mulGrp}_{P} \in CMnd$
87	86	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to {mulGrp}_{P} \in CMnd$
88	54	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to A (ran V) \in SubRing (P)$
89	76	subrgsubm	$⊢ A (ran V) \in SubRing (P) \to A (ran V) \in SubMnd ({mulGrp}_{P})$
90	88 89	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})$
91		simplll	$⊢ (((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land z \in I) \to φ$
92	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))$
93	35 92	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))$
94	93	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)$
95	94	simpld	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to k : I ⟶ ℕ_{0}$
96	95	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}$
97	4 9	aspssid	$⊢ (S \in AssAlg \land ran V \subseteq {Base}_{S}) \to ran V \subseteq A (ran V)$
98	7 48 97	syl2anc	$⊢ φ \to ran V \subseteq A (ran V)$
99	98	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)$
100	15	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to V Fn I$
101		fnfvelrn	$⊢ (V Fn I \land z \in I) \to V (z) \in ran V$
102	100 101	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$
103	99 102	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)$
104	76 8	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
105		eqid	$⊢ \cdot_{P} = \cdot_{P}$
106	76 105	mgpplusg	$⊢ \cdot_{P} = +_{{mulGrp}_{P}}$
107	105	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)$
108	54 107	syl3an1	$⊢ (φ \land u \in A (ran V) \land v \in A (ran V)) \to u \cdot_{P} v \in A (ran V)$
109	81	subrg1cl	$⊢ A (ran V) \in SubRing (P) \to 1_{P} \in A (ran V)$
110	54 109	syl	$⊢ φ \to 1_{P} \in A (ran V)$
111	104 77 106 86 31 108 82 110	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)$
112	91 96 103 111	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)$
113	112	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)$
114	5	mptexd	$⊢ φ \to (z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z)) \in V$
115	114	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$
116		funmpt	$⊢ Fun (z \in I ⟼ k (z) \cdot_{{mulGrp}_{P}} V (z))$
117	116	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))$
118		fvexd	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to 1_{P} \in V$
119	94	simprd	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to k^{-1} [ℕ] \in Fin$
120		elrabi	$⊢ k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \to k \in ({ℕ_{0}}^{I})$
121		elmapi	$⊢ k \in ({ℕ_{0}}^{I}) \to k : I ⟶ ℕ_{0}$
122	121	adantl	$⊢ ((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \to k : I ⟶ ℕ_{0}$
123	5	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \to I \in W$
124		fcdmnn0supp	$⊢ (I \in W \land k : I ⟶ ℕ_{0}) \to k supp 0 = k^{-1} [ℕ]$
125	123 122 124	syl2anc	$⊢ ((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \to k supp 0 = k^{-1} [ℕ]$
126		eqimss	$⊢ k supp 0 = k^{-1} [ℕ] \to k supp 0 \subseteq k^{-1} [ℕ]$
127	125 126	syl	$⊢ ((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \to k supp 0 \subseteq k^{-1} [ℕ]$
128		c0ex	$⊢ 0 \in V$
129	128	a1i	$⊢ ((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \to 0 \in V$
130	122 127 123 129	suppssr	$⊢ (((φ \land x \in {Base}_{P}) \land k \in ({ℕ_{0}}^{I})) \land z \in (I ∖ k^{-1} [ℕ])) \to k (z) = 0$
131	120 130	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$
132	131	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)$
133	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$
134	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$
135		eldifi	$⊢ z \in (I ∖ k^{-1} [ℕ]) \to z \in I$
136	135	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$
137	1 3 8 133 134 136	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}$
138	104 82 77	mulg0	$⊢ V (z) \in {Base}_{P} \to 0 \cdot_{{mulGrp}_{P}} V (z) = 1_{P}$
139	137 138	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}$
140	132 139	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}$
141	140 75	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} [ℕ]$
142		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)))$
143	115 117 118 119 141 142	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)))$
144	82 87 75 90 113 143	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)$
145	80 144	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)$
146		eqid	$⊢ Scalar (P) = Scalar (P)$
147		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
148	146 36 147 63	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)$
149	59 67 74 145 148	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)$
150	149	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)$
151	45	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$
152		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})))$
153		fvex	$⊢ 0_{P} \in V$
154	151 152 153	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)$
155	154	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)$
156	1 2 9 33 8	mplelbas	$⊢ x \in {Base}_{P} \leftrightarrow (x \in {Base}_{S} \land {finSupp}_{0_{R}} (x))$
157	156	simprbi	$⊢ x \in {Base}_{P} \to {finSupp}_{0_{R}} (x)$
158	157	adantl	$⊢ (φ \land x \in {Base}_{P}) \to {finSupp}_{0_{R}} (x)$
159	158	fsuppimpd	$⊢ (φ \land x \in {Base}_{P}) \to x supp 0_{R} \in Fin$
160		ssidd	$⊢ (φ \land x \in {Base}_{P}) \to x supp 0_{R} \subseteq x supp 0_{R}$
161		fvexd	$⊢ (φ \land x \in {Base}_{P}) \to 0_{R} \in V$
162	69 160 47 161	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}$
163	71	fveq2d	$⊢ (φ \land x \in {Base}_{P}) \to 0_{R} = 0_{Scalar (P)}$
164	163	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)}$
165	162 164	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)}$
166	165	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}))$
167		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\}$
168	13	ad2antrr	$⊢ ((φ \land x \in {Base}_{P}) \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to R \in Ring$
169	1 8 33 34 32 75 168 79	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}$
170		eqid	$⊢ 0_{Scalar (P)} = 0_{Scalar (P)}$
171	8 146 36 170 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}$
172	59 169 171	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}$
173	167 172	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}$
174	166 173	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}$
175	174 47	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}$
176		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}))))$
177	155 159 175 176	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}))))$
178	40 44 47 57 150 177	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)$
179	39 178	eqeltrd	$⊢ (φ \land x \in {Base}_{P}) \to x \in A (ran V)$
180	31 179	eqelssd	$⊢ φ \to A (ran V) = {Base}_{P}$

Metamath Proof Explorer

Theorem mplbas2

Proof