Theorem mplbas2 21998

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 21931	. . . 4 ⊢ (𝜑 → 𝑆 ∈ AssAlg)
5		mplbas2.p	. . . . . 6 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
6		eqid 2735	. . . . . 6 ⊢ (Base‘𝑃) = (Base‘𝑃)
7		eqid 2735	. . . . . 6 ⊢ (Base‘𝑆) = (Base‘𝑆)
8	5, 1, 6, 7	mplbasss 21955	. . . . 5 ⊢ (Base‘𝑃) ⊆ (Base‘𝑆)
9	8	a1i 11	. . . 4 ⊢ (𝜑 → (Base‘𝑃) ⊆ (Base‘𝑆))
10		mplbas2.v	. . . . . . . 8 ⊢ 𝑉 = (𝐼 mVar 𝑅)
11		crngring 20203	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
12	3, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Ring)
13	1, 10, 7, 2, 12	mvrf 21943	. . . . . . 7 ⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑆))
14	13	ffnd 6706	. . . . . 6 ⊢ (𝜑 → 𝑉 Fn 𝐼)
15	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊)
16	12	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring)
17		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
18	5, 10, 6, 15, 16, 17	mvrcl 21950	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ (Base‘𝑃))
19	18	ralrimiva 3132	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃))
20		ffnfv 7108	. . . . . 6 ⊢ (𝑉:𝐼⟶(Base‘𝑃) ↔ (𝑉 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃)))
21	14, 19, 20	sylanbrc 583	. . . . 5 ⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑃))
22	21	frnd 6713	. . . 4 ⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑃))
23		mplbas2.a	. . . . 5 ⊢ 𝐴 = (AlgSpan‘𝑆)
24	23, 7	aspss 21835	. . . 4 ⊢ ((𝑆 ∈ AssAlg ∧ (Base‘𝑃) ⊆ (Base‘𝑆) ∧ ran 𝑉 ⊆ (Base‘𝑃)) → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃)))
25	4, 9, 22, 24	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃)))
26	1, 5, 6, 2, 12	mplsubrg 21963	. . . 4 ⊢ (𝜑 → (Base‘𝑃) ∈ (SubRing‘𝑆))
27	1, 5, 6, 2, 12	mpllss 21961	. . . 4 ⊢ (𝜑 → (Base‘𝑃) ∈ (LSubSp‘𝑆))
28		eqid 2735	. . . . 5 ⊢ (LSubSp‘𝑆) = (LSubSp‘𝑆)
29	23, 7, 28	aspid 21833	. . . 4 ⊢ ((𝑆 ∈ AssAlg ∧ (Base‘𝑃) ∈ (SubRing‘𝑆) ∧ (Base‘𝑃) ∈ (LSubSp‘𝑆)) → (𝐴‘(Base‘𝑃)) = (Base‘𝑃))
30	4, 26, 27, 29	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝐴‘(Base‘𝑃)) = (Base‘𝑃))
31	25, 30	sseqtrd 3995	. 2 ⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))
32		eqid 2735	. . . 4 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
33		eqid 2735	. . . 4 ⊢ (0g‘𝑅) = (0g‘𝑅)
34		eqid 2735	. . . 4 ⊢ (1r‘𝑅) = (1r‘𝑅)
35	2	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝐼 ∈ 𝑊)
36		eqid 2735	. . . 4 ⊢ ( ·𝑠 ‘𝑃) = ( ·𝑠 ‘𝑃)
37	12	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 ∈ Ring)
38		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (Base‘𝑃))
39	5, 32, 33, 34, 35, 6, 36, 37, 38	mplcoe1 21993	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))))
40		eqid 2735	. . . 4 ⊢ (0g‘𝑃) = (0g‘𝑃)
41	5, 2, 12	mplringd 21981	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Ring)
42		ringabl 20239	. . . . . 6 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Abel)
43	41, 42	syl 17	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ Abel)
44	43	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑃 ∈ Abel)
45		ovex 7436	. . . . . 6 ⊢ (ℕ0 ↑m 𝐼) ∈ V
46	45	rabex 5309	. . . . 5 ⊢ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈ V
47	46	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∈ V)
48	13	frnd 6713	. . . . . . . 8 ⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑆))
49	23, 7	aspsubrg 21834	. . . . . . . 8 ⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆))
50	4, 48, 49	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆))
51	5, 1, 6	mplval2 21954	. . . . . . . . 9 ⊢ 𝑃 = (𝑆 ↾s (Base‘𝑃))
52	51	subsubrg 20556	. . . . . . . 8 ⊢ ((Base‘𝑃) ∈ (SubRing‘𝑆) → ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
53	26, 52	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
54	50, 31, 53	mpbir2and 713	. . . . . 6 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃))
55		subrgsubg 20535	. . . . . 6 ⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
56	54, 55	syl 17	. . . . 5 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
57	56	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
58	5, 2, 12	mpllmodd 21982	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ LMod)
59	58	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑃 ∈ LMod)
60	23, 7, 28	asplss 21832	. . . . . . . . 9 ⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆))
61	4, 48, 60	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆))
62	1, 2, 12	psrlmod 21918	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ LMod)
63		eqid 2735	. . . . . . . . . 10 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
64	51, 28, 63	lsslss 20916	. . . . . . . . 9 ⊢ ((𝑆 ∈ LMod ∧ (Base‘𝑃) ∈ (LSubSp‘𝑆)) → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
65	62, 27, 64	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
66	61, 31, 65	mpbir2and 713	. . . . . . 7 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃))
67	66	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃))
68		eqid 2735	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅)
69	5, 68, 6, 32, 38	mplelf 21956	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥:{𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶(Base‘𝑅))
70	69	ffvelcdmda 7073	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘𝑅))
71	5, 35, 37	mplsca 21971	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 = (Scalar‘𝑃))
72	71	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 = (Scalar‘𝑃))
73	72	fveq2d 6879	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
74	70, 73	eleqtrd 2836	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃)))
75	2	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝐼 ∈ 𝑊)
76		eqid 2735	. . . . . . . 8 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
77		eqid 2735	. . . . . . . 8 ⊢ (.g‘(mulGrp‘𝑃)) = (.g‘(mulGrp‘𝑃))
78	3	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ CRing)
79		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin})
80	5, 32, 33, 34, 75, 76, 77, 10, 78, 79	mplcoe2 21997	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) = ((mulGrp‘𝑃) Σg (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))))
81		eqid 2735	. . . . . . . . 9 ⊢ (1r‘𝑃) = (1r‘𝑃)
82	76, 81	ringidval 20141	. . . . . . . 8 ⊢ (1r‘𝑃) = (0g‘(mulGrp‘𝑃))
83	5	mplcrng 21979	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ CRing)
84	2, 3, 83	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ CRing)
85	76	crngmgp 20199	. . . . . . . . . 10 ⊢ (𝑃 ∈ CRing → (mulGrp‘𝑃) ∈ CMnd)
86	84, 85	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ CMnd)
87	86	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (mulGrp‘𝑃) ∈ CMnd)
88	54	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃))
89	76	subrgsubm 20543	. . . . . . . . 9 ⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃)))
90	88, 89	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃)))
91		simplll 774	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → 𝜑)
92	32	psrbag 21875	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ 𝑊 → (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈ Fin)))
93	35, 92	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈ Fin)))
94	93	biimpa 476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑘:𝐼⟶ℕ0 ∧ (◡𝑘 “ ℕ) ∈ Fin))
95	94	simpld 494	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑘:𝐼⟶ℕ0)
96	95	ffvelcdmda 7073	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑘‘𝑧) ∈ ℕ0)
97	23, 7	aspssid 21836	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
98	4, 48, 97	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
99	98	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
100	14	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑉 Fn 𝐼)
101		fnfvelrn 7069	. . . . . . . . . . . 12 ⊢ ((𝑉 Fn 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉)
102	100, 101	sylan 580	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉)
103	99, 102	sseldd 3959	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉))
104	76, 6	mgpbas 20103	. . . . . . . . . . 11 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
105		eqid 2735	. . . . . . . . . . . 12 ⊢ (.r‘𝑃) = (.r‘𝑃)
106	76, 105	mgpplusg 20102	. . . . . . . . . . 11 ⊢ (.r‘𝑃) = (+g‘(mulGrp‘𝑃))
107	105	subrgmcl 20542	. . . . . . . . . . . 12 ⊢ (((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉))
108	54, 107	syl3an1 1163	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(.r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉))
109	81	subrg1cl 20538	. . . . . . . . . . . 12 ⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (1r‘𝑃) ∈ (𝐴‘ran 𝑉))
110	54, 109	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1r‘𝑃) ∈ (𝐴‘ran 𝑉))
111	104, 77, 106, 86, 31, 108, 82, 110	mulgnn0subcl 19068	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘‘𝑧) ∈ ℕ0 ∧ (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉)) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉))
112	91, 96, 103, 111	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉))
113	112	fmpttd 7104	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))):𝐼⟶(𝐴‘ran 𝑉))
114	2	mptexd 7215	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V)
115	114	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V)
116		funmpt 6573	. . . . . . . . . 10 ⊢ Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))
117	116	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))))
118		fvexd 6890	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (1r‘𝑃) ∈ V)
119	94	simprd 495	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (◡𝑘 “ ℕ) ∈ Fin)
120		elrabi 3666	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} → 𝑘 ∈ (ℕ0 ↑m 𝐼))
121		elmapi 8861	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℕ0 ↑m 𝐼) → 𝑘:𝐼⟶ℕ0)
122	121	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) → 𝑘:𝐼⟶ℕ0)
123	2	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) → 𝐼 ∈ 𝑊)
124		fcdmnn0supp 12556	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘:𝐼⟶ℕ0) → (𝑘 supp 0) = (◡𝑘 “ ℕ))
125	123, 122, 124	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) → (𝑘 supp 0) = (◡𝑘 “ ℕ))
126		eqimss 4017	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 supp 0) = (◡𝑘 “ ℕ) → (𝑘 supp 0) ⊆ (◡𝑘 “ ℕ))
127	125, 126	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) → (𝑘 supp 0) ⊆ (◡𝑘 “ ℕ))
128		c0ex 11227	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
129	128	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) → 0 ∈ V)
130	122, 127, 123, 129	suppssr 8192	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ0 ↑m 𝐼)) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0)
131	120, 130	sylanl2 681	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0)
132	131	oveq1d 7418	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))
133	2	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝐼 ∈ 𝑊)
134	12	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝑅 ∈ Ring)
135		eldifi 4106	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ)) → 𝑧 ∈ 𝐼)
136	135	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → 𝑧 ∈ 𝐼)
137	5, 10, 6, 133, 134, 136	mvrcl 21950	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (𝑉‘𝑧) ∈ (Base‘𝑃))
138	104, 82, 77	mulg0 19055	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑧) ∈ (Base‘𝑃) → (0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃))
139	137, 138	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → (0(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃))
140	132, 139	eqtrd 2770	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1r‘𝑃))
141	140, 75	suppss2 8197	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1r‘𝑃)) ⊆ (◡𝑘 “ ℕ))
142		suppssfifsupp 9390	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V ∧ Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∧ (1r‘𝑃) ∈ V) ∧ ((◡𝑘 “ ℕ) ∈ Fin ∧ ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1r‘𝑃)) ⊆ (◡𝑘 “ ℕ))) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1r‘𝑃))
143	115, 117, 118, 119, 141, 142	syl32anc 1380	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1r‘𝑃))
144	82, 87, 75, 90, 113, 143	gsumsubmcl 19898	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((mulGrp‘𝑃) Σg (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(.g‘(mulGrp‘𝑃))(𝑉‘𝑧)))) ∈ (𝐴‘ran 𝑉))
145	80, 144	eqeltrd 2834	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (𝐴‘ran 𝑉))
146		eqid 2735	. . . . . . 7 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
147		eqid 2735	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
148	146, 36, 147, 63	lssvscl 20910	. . . . . 6 ⊢ (((𝑃 ∈ LMod ∧ (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) ∧ ((𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (𝐴‘ran 𝑉))) → ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) ∈ (𝐴‘ran 𝑉))
149	59, 67, 74, 145, 148	syl22anc 838	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) ∈ (𝐴‘ran 𝑉))
150	149	fmpttd 7104	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))):{𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}⟶(𝐴‘ran 𝑉))
151	45	mptrabex 7216	. . . . . . 7 ⊢ (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V
152		funmpt 6573	. . . . . . 7 ⊢ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))
153		fvex 6888	. . . . . . 7 ⊢ (0g‘𝑃) ∈ V
154	151, 152, 153	3pm3.2i 1340	. . . . . 6 ⊢ ((𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) ∧ (0g‘𝑃) ∈ V)
155	154	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))
156	5, 1, 7, 33, 6	mplelbas 21949	. . . . . . . 8 ⊢ (𝑥 ∈ (Base‘𝑃) ↔ (𝑥 ∈ (Base‘𝑆) ∧ 𝑥 finSupp (0g‘𝑅)))
157	156	simprbi 496	. . . . . . 7 ⊢ (𝑥 ∈ (Base‘𝑃) → 𝑥 finSupp (0g‘𝑅))
158	157	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 finSupp (0g‘𝑅))
159	158	fsuppimpd 9379	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g‘𝑅)) ∈ Fin)
160		ssidd 3982	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0g‘𝑅)) ⊆ (𝑥 supp (0g‘𝑅)))
161		fvexd 6890	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0g‘𝑅) ∈ V)
162	69, 160, 47, 161	suppssr 8192	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (𝑥‘𝑘) = (0g‘𝑅))
163	71	fveq2d 6879	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0g‘𝑅) = (0g‘(Scalar‘𝑃)))
164	163	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (0g‘𝑅) = (0g‘(Scalar‘𝑃)))
165	162, 164	eqtrd 2770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → (𝑥‘𝑘) = (0g‘(Scalar‘𝑃)))
166	165	oveq1d 7418	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = ((0g‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))
167		eldifi 4106	. . . . . . . 8 ⊢ (𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅))) → 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin})
168	12	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ Ring)
169	5, 6, 33, 34, 32, 75, 168, 79	mplmon 21991	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘𝑃))
170		eqid 2735	. . . . . . . . . 10 ⊢ (0g‘(Scalar‘𝑃)) = (0g‘(Scalar‘𝑃))
171	6, 146, 36, 170, 40	lmod0vs 20850	. . . . . . . . 9 ⊢ ((𝑃 ∈ LMod ∧ (𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))) ∈ (Base‘𝑃)) → ((0g‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃))
172	59, 169, 171	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}) → ((0g‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃))
173	167, 172	sylan2 593	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((0g‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃))
174	166, 173	eqtrd 2770	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0g‘𝑅)))) → ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))) = (0g‘𝑃))
175	174, 47	suppss2 8197	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) supp (0g‘𝑃)) ⊆ (𝑥 supp (0g‘𝑅)))
176		suppssfifsupp 9390	. . . . 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‘𝑃))
177	155, 159, 175, 176	syl12anc 836	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅))))) finSupp (0g‘𝑃))
178	40, 44, 47, 57, 150, 177	gsumsubgcl 19899	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑃 Σg (𝑘 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1r‘𝑅), (0g‘𝑅)))))) ∈ (𝐴‘ran 𝑉))
179	39, 178	eqeltrd 2834	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (𝐴‘ran 𝑉))
180	31, 179	eqelssd 3980	1 ⊢ (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  ∀wral 3051  {crab 3415  Vcvv 3459   ∖ cdif 3923   ⊆ wss 3926  ifcif 4500   class class class wbr 5119   ↦ cmpt 5201  ^◡ccnv 5653  ran crn 5655   “ cima 5657  Fun wfun 6524   Fn wfn 6525  ⟶wf 6526  ‘cfv 6530  (class class class)co 7403   supp csupp 8157   ↑_m cmap 8838  Fincfn 8957   finSupp cfsupp 9371  0cc0 11127  ℕcn 12238  ℕ₀cn0 12499  Basecbs 17226  ._rcmulr 17270  Scalarcsca 17272   ·_𝑠 cvsca 17273  0_gc0g 17451   Σ_g cgsu 17452  SubMndcsubmnd 18758  ._gcmg 19048  SubGrpcsubg 19101  CMndccmn 19759  Abelcabl 19760  mulGrpcmgp 20098  1_rcur 20139  Ringcrg 20191  CRingccrg 20192  SubRingcsubrg 20527  LModclmod 20815  LSubSpclss 20886  AssAlgcasa 21808  AlgSpancasp 21809   mPwSer cmps 21862   mVar cmvr 21863   mPoly cmpl 21864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-iin 4970  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-isom 6539  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-of 7669  df-ofr 7670  df-om 7860  df-1st 7986  df-2nd 7987  df-supp 8158  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-er 8717  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9372  df-sup 9452  df-oi 9522  df-card 9951  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305  df-7 12306  df-8 12307  df-9 12308  df-n0 12500  df-z 12587  df-dec 12707  df-uz 12851  df-fz 13523  df-fzo 13670  df-seq 14018  df-hash 14347  df-struct 17164  df-sets 17181  df-slot 17199  df-ndx 17211  df-base 17227  df-ress 17250  df-plusg 17282  df-mulr 17283  df-sca 17285  df-vsca 17286  df-ip 17287  df-tset 17288  df-ple 17289  df-ds 17291  df-hom 17293  df-cco 17294  df-0g 17453  df-gsum 17454  df-prds 17459  df-pws 17461  df-mre 17596  df-mrc 17597  df-acs 17599  df-mgm 18616  df-sgrp 18695  df-mnd 18711  df-mhm 18759  df-submnd 18760  df-grp 18917  df-minusg 18918  df-sbg 18919  df-mulg 19049  df-subg 19104  df-ghm 19194  df-cntz 19298  df-cmn 19761  df-abl 19762  df-mgp 20099  df-rng 20111  df-ur 20140  df-srg 20145  df-ring 20193  df-cring 20194  df-subrng 20504  df-subrg 20528  df-lmod 20817  df-lss 20887  df-assa 21811  df-asp 21812  df-psr 21867  df-mvr 21868  df-mpl 21869

This theorem is referenced by:  mplind  22026  evlseu  22039