Theorem mplbas2 20245

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.)

Hypotheses

Ref	Expression
mplbas2.p	⊢ 𝑃 = (𝐼 mPoly 𝑅)
mplbas2.s	⊢ 𝑆 = (𝐼 mPwSer 𝑅)
mplbas2.v	⊢ 𝑉 = (𝐼 mVar 𝑅)
mplbas2.a	⊢ 𝐴 = (AlgSpan‘𝑆)
mplbas2.i	⊢ (𝜑 → 𝐼 ∈ 𝑊)
mplbas2.r	⊢ (𝜑 → 𝑅 ∈ CRing)

Assertion

Ref	Expression
mplbas2	⊢ (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃))

Proof of Theorem mplbas2

Dummy variables 𝑢 𝑘 𝑣 𝑥 𝑧 𝑦 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mplbas2.s	. . . . 5 ⊢ 𝑆 = (𝐼 mPwSer 𝑅)
2		mplbas2.i	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
3		mplbas2.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CRing)
4	1, 2, 3	psrassa 20188	. . . 4 ⊢ (𝜑 → 𝑆 ∈ AssAlg)
5		mplbas2.p	. . . . . 6 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
6		eqid 2821	. . . . . 6 ⊢ (Base‘𝑃) = (Base‘𝑃)
7		eqid 2821	. . . . . 6 ⊢ (Base‘𝑆) = (Base‘𝑆)
8	5, 1, 6, 7	mplbasss 20206	. . . . 5 ⊢ (Base‘𝑃) ⊆ (Base‘𝑆)
9	8	a1i 11	. . . 4 ⊢ (𝜑 → (Base‘𝑃) ⊆ (Base‘𝑆))
10		mplbas2.v	. . . . . . . 8 ⊢ 𝑉 = (𝐼 mVar 𝑅)
11		crngring 19302	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
12	3, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Ring)
13	1, 10, 7, 2, 12	mvrf 20198	. . . . . . 7 ⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑆))
14	13	ffnd 6509	. . . . . 6 ⊢ (𝜑 → 𝑉 Fn 𝐼)
15	2	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊)
16	12	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring)
17		simpr 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
18	5, 10, 6, 15, 16, 17	mvrcl 20223	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ (Base‘𝑃))
19	18	ralrimiva 3182	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃))
20		ffnfv 6876	. . . . . 6 ⊢ (𝑉:𝐼⟶(Base‘𝑃) ↔ (𝑉 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃)))
21	14, 19, 20	sylanbrc 585	. . . . 5 ⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑃))
22	21	frnd 6515	. . . 4 ⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑃))
23		mplbas2.a	. . . . 5 ⊢ 𝐴 = (AlgSpan‘𝑆)
24	23, 7	aspss 20100	. . . 4 ⊢ ((𝑆 ∈ AssAlg ∧ (Base‘𝑃) ⊆ (Base‘𝑆) ∧ ran 𝑉 ⊆ (Base‘𝑃)) → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃)))
25	4, 9, 22, 24	syl3anc 1367	. . 3 ⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃)))
26	1, 5, 6, 2, 12	mplsubrg 20214	. . . 4 ⊢ (𝜑 → (Base‘𝑃) ∈ (SubRing‘𝑆))
27	1, 5, 6, 2, 12	mpllss 20212	. . . 4 ⊢ (𝜑 → (Base‘𝑃) ∈ (LSubSp‘𝑆))
28		eqid 2821	. . . . 5 ⊢ (LSubSp‘𝑆) = (LSubSp‘𝑆)
29	23, 7, 28	aspid 20098	. . . 4 ⊢ ((𝑆 ∈ AssAlg ∧ (Base‘𝑃) ∈ (SubRing‘𝑆) ∧ (Base‘𝑃) ∈ (LSubSp‘𝑆)) → (𝐴‘(Base‘𝑃)) = (Base‘𝑃))
30	4, 26, 27, 29	syl3anc 1367	. . 3 ⊢ (𝜑 → (𝐴‘(Base‘𝑃)) = (Base‘𝑃))
31	25, 30	sseqtrd 4006	. 2 ⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))
32		eqid 2821	. . . 4 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
33		eqid 2821	. . . 4 ⊢ (0g‘𝑅) = (0g‘𝑅)
34		eqid 2821	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
35	2	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝐼 ∈ 𝑊)
36		eqid 2821	. . . 4 ⊢ ( ·𝑠 ‘𝑃) = ( ·𝑠 ‘𝑃)
37	12	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 ∈ Ring)
38		simpr 487	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (Base‘𝑃))
39	5, 32, 33, 34, 35, 6, 36, 37, 38	mplcoe1 20240	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))))
40		eqid 2821	. . . 4 ⊢ (0g‘𝑃) = (0g‘𝑃)
41	5	mplring 20226	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring)
42	2, 12, 41	syl2anc 586	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Ring)
43		ringabl 19324	. . . . . 6 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Abel)
44	42, 43	syl 17	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ Abel)
45	44	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑃 ∈ Abel)
46		ovex 7183	. . . . . 6 ⊢ (ℕ0 ↑m 𝐼) ∈ V
47	46	rabex 5227	. . . . 5 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈ V
48	47	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈ V)
49	13	frnd 6515	. . . . . . . 8 ⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑆))
50	23, 7	aspsubrg 20099	. . . . . . . 8 ⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆))
51	4, 49, 50	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆))
52	5, 1, 6	mplval2 20205	. . . . . . . . 9 ⊢ 𝑃 = (𝑆 ↾s (Base‘𝑃))
53	52	subsubrg 19555	. . . . . . . 8 ⊢ ((Base‘𝑃) ∈ (SubRing‘𝑆) → ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
54	26, 53	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
55	51, 31, 54	mpbir2and 711	. . . . . 6 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃))
56		subrgsubg 19535	. . . . . 6 ⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
57	55, 56	syl 17	. . . . 5 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
58	57	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
59	5	mpllmod 20225	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod)
60	2, 12, 59	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ LMod)
61	60	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑃 ∈ LMod)
62	23, 7, 28	asplss 20097	. . . . . . . . 9 ⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆))
63	4, 49, 62	syl2anc 586	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆))
64	1, 2, 12	psrlmod 20175	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ LMod)
65		eqid 2821	. . . . . . . . . 10 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
66	52, 28, 65	lsslss 19727	. . . . . . . . 9 ⊢ ((𝑆 ∈ LMod ∧ (Base‘𝑃) ∈ (LSubSp‘𝑆)) → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
67	64, 27, 66	syl2anc 586	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
68	63, 31, 67	mpbir2and 711	. . . . . . 7 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃))
69	68	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃))
70		eqid 2821	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅)
71	5, 70, 6, 32, 38	mplelf 20207	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥:{𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶(Base‘𝑅))
72	71	ffvelrnda 6845	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘𝑅))
73	5, 35, 37	mplsca 20219	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 = (Scalar‘𝑃))
74	73	adantr 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 = (Scalar‘𝑃))
75	74	fveq2d 6668	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
76	72, 75	eleqtrd 2915	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃)))
77	2	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝐼 ∈ 𝑊)
78		eqid 2821	. . . . . . . 8 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
79		eqid 2821	. . . . . . . 8 ⊢ (.g‘(mulGrp‘𝑃)) = (.g‘(mulGrp‘𝑃))
80	3	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ CRing)
81		simpr 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin})
82	5, 32, 33, 34, 77, 78, 79, 10, 80, 81	mplcoe2 20244	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) = ((mulGrp‘𝑃) Σg (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))))
83		eqid 2821	. . . . . . . . 9 ⊢ (1r‘𝑃) = (1r‘𝑃)
84	78, 83	ringidval 19247	. . . . . . . 8 ⊢ (1r‘𝑃) = (0g‘(mulGrp‘𝑃))
85	5	mplcrng 20228	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ CRing)
86	2, 3, 85	syl2anc 586	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ CRing)
87	78	crngmgp 19299	. . . . . . . . . 10 ⊢ (𝑃 ∈ CRing → (mulGrp‘𝑃) ∈ CMnd)
88	86, 87	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ CMnd)
89	88	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (mulGrp‘𝑃) ∈ CMnd)
90	55	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃))
91	78	subrgsubm 19542	. . . . . . . . 9 ⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃)))
92	90, 91	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃)))
93		simplll 773	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → 𝜑)
94	32	psrbag 20138	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ 𝑊 → (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈ Fin)))
95	35, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈ Fin)))
96	95	biimpa 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈ Fin))
97	96	simpld 497	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑘:𝐼⟶ℕ0)
98	97	ffvelrnda 6845	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑘‘𝑧) ∈ ℕ0)
99	23, 7	aspssid 20101	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
100	4, 49, 99	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
101	100	ad3antrrr 728	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
102	14	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑉 Fn 𝐼)
103		fnfvelrn 6842	. . . . . . . . . . . 12 ⊢ ((𝑉 Fn 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉)
104	102, 103	sylan 582	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉)
105	101, 104	sseldd 3967	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉))
106	78, 6	mgpbas 19239	. . . . . . . . . . 11 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
107		eqid 2821	. . . . . . . . . . . 12 ⊢ (.r‘𝑃) = (.r‘𝑃)
108	78, 107	mgpplusg 19237	. . . . . . . . . . 11 ⊢ (.r‘𝑃) = (+g‘(mulGrp‘𝑃))
109	107	subrgmcl 19541	. . . . . . . . . . . 12 ⊢ (((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉))
110	55, 109	syl3an1 1159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉))
111	83	subrg1cl 19537	. . . . . . . . . . . 12 ⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (1r‘𝑃) ∈ (𝐴‘ran 𝑉))
112	55, 111	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1r‘𝑃) ∈ (𝐴‘ran 𝑉))
113	106, 79, 108, 88, 31, 110, 84, 112	mulgnn0subcl 18235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘‘𝑧) ∈ ℕ0 ∧ (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉)) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉))
114	93, 98, 105, 113	syl3anc 1367	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉))
115	114	fmpttd 6873	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))):𝐼⟶(𝐴‘ran 𝑉))
116	2	mptexd 6981	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V)
117	116	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V)
118		funmpt 6387	. . . . . . . . . 10 ⊢ Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))
119	118	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))))
120		fvexd 6679	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (1r‘𝑃) ∈ V)
121	96	simprd 498	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (◡𝑘 “ ℕ) ∈ Fin)
122		elrabi 3674	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} → 𝑘 ∈ (ℕ0 ↑m 𝐼))
123		elmapi 8422	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℕ0 ↑m 𝐼) → 𝑘:𝐼⟶ℕ0)
124	123	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) → 𝑘:𝐼⟶ℕ0)
125	2	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) → 𝐼 ∈ 𝑊)
126		frnnn0supp 11947	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘:𝐼⟶ℕ0) → (𝑘 supp 0) = (◡𝑘 “ ℕ))
127	125, 124, 126	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) → (𝑘 supp 0) = (◡𝑘 “ ℕ))
128		eqimss 4022	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 supp 0) = (◡𝑘 “ ℕ) → (𝑘 supp 0) ⊆ (◡𝑘 “ ℕ))
129	127, 128	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) → (𝑘 supp 0) ⊆ (◡𝑘 “ ℕ))
130		c0ex 10629	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
131	130	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) → 0 ∈ V)
132	124, 129, 125, 131	suppssr 7855	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0)
133	122, 132	sylanl2 679	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0)
134	133	oveq1d 7165	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))
135	2	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝐼 ∈ 𝑊)
136	12	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝑅 ∈ Ring)
137		eldifi 4102	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ)) → 𝑧 ∈ 𝐼)
138	137	adantl 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝑧 ∈ 𝐼)
139	5, 10, 6, 135, 136, 138	mvrcl 20223	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑉‘𝑧) ∈ (Base‘𝑃))
140	106, 84, 79	mulg0 18225	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑧) ∈ (Base‘𝑃) → (0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃))
141	139, 140	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃))
142	134, 141	eqtrd 2856	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃))
143	142, 77	suppss2 7858	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1r‘𝑃)) ⊆ (◡𝑘 “ ℕ))
144		suppssfifsupp 8842	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V ∧ Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∧ (1r‘𝑃) ∈ V) ∧ ((◡𝑘 “ ℕ) ∈ Fin ∧ ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1r‘𝑃)) ⊆ (◡𝑘 “ ℕ))) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1r‘𝑃))
145	117, 119, 120, 121, 143, 144	syl32anc 1374	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1r‘𝑃))
146	84, 89, 77, 92, 115, 145	gsumsubmcl 19033	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((mulGrp‘𝑃) Σg (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))) ∈ (𝐴‘ran 𝑉))
147	82, 146	eqeltrd 2913	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (𝐴‘ran 𝑉))
148		eqid 2821	. . . . . . 7 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
149		eqid 2821	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
150	148, 36, 149, 65	lssvscl 19721	. . . . . 6 ⊢ (((𝑃 ∈ LMod ∧ (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) ∧ ((𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (𝐴‘ran 𝑉))) → ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) ∈ (𝐴‘ran 𝑉))
151	61, 69, 76, 147, 150	syl22anc 836	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) ∈ (𝐴‘ran 𝑉))
152	151	fmpttd 6873	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))):{𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶(𝐴‘ran 𝑉))
153	46	mptrabex 6982	. . . . . . 7 ⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V
154		funmpt 6387	. . . . . . 7 ⊢ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))
155		fvex 6677	. . . . . . 7 ⊢ (0g‘𝑃) ∈ V
156	153, 154, 155	3pm3.2i 1335	. . . . . 6 ⊢ ((𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V)
157	156	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V))
158	5, 1, 7, 33, 6	mplelbas 20204	. . . . . . . 8 ⊢ (𝑥 ∈ (Base‘𝑃) ↔ (𝑥 ∈ (Base‘𝑆) ∧ 𝑥 finSupp (0g‘𝑅)))
159	158	simprbi 499	. . . . . . 7 ⊢ (𝑥 ∈ (Base‘𝑃) → 𝑥 finSupp (0g‘𝑅))
160	159	adantl 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 finSupp (0g‘𝑅))
161	160	fsuppimpd 8834	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g‘𝑅)) ∈ Fin)
162		ssidd 3989	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g‘𝑅)) ⊆ (𝑥 supp (0g‘𝑅)))
163		fvexd 6679	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0g‘𝑅) ∈ V)
164	71, 162, 48, 163	suppssr 7855	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (𝑥‘𝑘) = (0g‘𝑅))
165	73	fveq2d 6668	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0g‘𝑅) = (0g‘(Scalar‘𝑃)))
166	165	adantr 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (0g‘𝑅) = (0g‘(Scalar‘𝑃)))
167	164, 166	eqtrd 2856	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (𝑥‘𝑘) = (0g‘(Scalar‘𝑃)))
168	167	oveq1d 7165	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = ((0g‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))
169		eldifi 4102	. . . . . . . 8 ⊢ (𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅))) → 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin})
170	12	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ Ring)
171	5, 6, 33, 34, 32, 77, 170, 81	mplmon 20238	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘𝑃))
172		eqid 2821	. . . . . . . . . 10 ⊢ (0g‘(Scalar‘𝑃)) = (0g‘(Scalar‘𝑃))
173	6, 148, 36, 172, 40	lmod0vs 19661	. . . . . . . . 9 ⊢ ((𝑃 ∈ LMod ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘𝑃)) → ((0g‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃))
174	61, 171, 173	syl2anc 586	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((0g‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃))
175	169, 174	sylan2 594	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((0g‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃))
176	168, 175	eqtrd 2856	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃))
177	176, 48	suppss2 7858	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) supp (0g‘𝑃)) ⊆ (𝑥 supp (0g‘𝑅)))
178		suppssfifsupp 8842	. . . . 5 ⊢ ((((𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V) ∧ ((𝑥 supp (0g‘𝑅)) ∈ Fin ∧ ((𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) supp (0g‘𝑃)) ⊆ (𝑥 supp (0g‘𝑅)))) → (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) finSupp (0g‘𝑃))
179	157, 161, 177, 178	syl12anc 834	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) finSupp (0g‘𝑃))
180	40, 45, 48, 58, 152, 179	gsumsubgcl 19034	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))) ∈ (𝐴‘ran 𝑉))
181	39, 180	eqeltrd 2913	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (𝐴‘ran 𝑉))
182	31, 181	eqelssd 3987	1 ⊢ (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ∀wral 3138  {crab 3142  Vcvv 3494   ∖ cdif 3932   ⊆ wss 3935  ifcif 4466   class class class wbr 5058   ↦ cmpt 5138  ^◡ccnv 5548  ran crn 5550   “ cima 5552  Fun wfun 6343   Fn wfn 6344  ⟶wf 6345  ‘cfv 6349  (class class class)co 7150   supp csupp 7824   ↑_m cmap 8400  Fincfn 8503   finSupp cfsupp 8827  0cc0 10531  ℕcn 11632  ℕ₀cn0 11891  Basecbs 16477  ._rcmulr 16560  Scalarcsca 16562   ·_𝑠 cvsca 16563  0_gc0g 16707   Σ_g cgsu 16708  SubMndcsubmnd 17949  ._gcmg 18218  SubGrpcsubg 18267  CMndccmn 18900  Abelcabl 18901  mulGrpcmgp 19233  1_rcur 19245  Ringcrg 19291  CRingccrg 19292  SubRingcsubrg 19525  LModclmod 19628  LSubSpclss 19697  AssAlgcasa 20076  AlgSpancasp 20077   mPwSer cmps 20125   mVar cmvr 20126   mPoly cmpl 20127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-iin 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-ofr 7404  df-om 7575  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8283  df-map 8402  df-pm 8403  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-uz 12238  df-fz 12887  df-fzo 13028  df-seq 13364  df-hash 13685  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-sca 16575  df-vsca 16576  df-tset 16578  df-0g 16709  df-gsum 16710  df-mre 16851  df-mrc 16852  df-acs 16854  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-mhm 17950  df-submnd 17951  df-grp 18100  df-minusg 18101  df-sbg 18102  df-mulg 18219  df-subg 18270  df-ghm 18350  df-cntz 18441  df-cmn 18902  df-abl 18903  df-mgp 19234  df-ur 19246  df-srg 19250  df-ring 19293  df-cring 19294  df-subrg 19527  df-lmod 19630  df-lss 19698  df-assa 20079  df-asp 20080  df-psr 20130  df-mvr 20131  df-mpl 20132

This theorem is referenced by:  mplind  20276  evlseu  20290