mplbas2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mplbas2		Structured version Visualization version GIF version

Theorem mplbas2 21816

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 21753	. . . 4 ⊢ (𝜑 → 𝑆 ∈ AssAlg)
5		mplbas2.p	. . . . . 6 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
6		eqid 2732	. . . . . 6 ⊢ (Base‘𝑃) = (Base‘𝑃)
7		eqid 2732	. . . . . 6 ⊢ (Base‘𝑆) = (Base‘𝑆)
8	5, 1, 6, 7	mplbasss 21775	. . . . 5 ⊢ (Base‘𝑃) ⊆ (Base‘𝑆)
9	8	a1i 11	. . . 4 ⊢ (𝜑 → (Base‘𝑃) ⊆ (Base‘𝑆))
10		mplbas2.v	. . . . . . . 8 ⊢ 𝑉 = (𝐼 mVar 𝑅)
11		crngring 20139	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
12	3, 11	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Ring)
13	1, 10, 7, 2, 12	mvrf 21763	. . . . . . 7 ⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑆))
14	13	ffnd 6718	. . . . . 6 ⊢ (𝜑 → 𝑉 Fn 𝐼)
15	2	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐼 ∈ 𝑊)
16	12	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring)
17		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼)
18	5, 10, 6, 15, 16, 17	mvrcl 21770	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ (Base‘𝑃))
19	18	ralrimiva 3146	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃))
20		ffnfv 7120	. . . . . 6 ⊢ (𝑉:𝐼⟶(Base‘𝑃) ↔ (𝑉 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ (Base‘𝑃)))
21	14, 19, 20	sylanbrc 583	. . . . 5 ⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑃))
22	21	frnd 6725	. . . 4 ⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑃))
23		mplbas2.a	. . . . 5 ⊢ 𝐴 = (AlgSpan‘𝑆)
24	23, 7	aspss 21650	. . . 4 ⊢ ((𝑆 ∈ AssAlg ∧ (Base‘𝑃) ⊆ (Base‘𝑆) ∧ ran 𝑉 ⊆ (Base‘𝑃)) → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃)))
25	4, 9, 22, 24	syl3anc 1371	. . 3 ⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (𝐴‘(Base‘𝑃)))
26	1, 5, 6, 2, 12	mplsubrg 21783	. . . 4 ⊢ (𝜑 → (Base‘𝑃) ∈ (SubRing‘𝑆))
27	1, 5, 6, 2, 12	mpllss 21781	. . . 4 ⊢ (𝜑 → (Base‘𝑃) ∈ (LSubSp‘𝑆))
28		eqid 2732	. . . . 5 ⊢ (LSubSp‘𝑆) = (LSubSp‘𝑆)
29	23, 7, 28	aspid 21648	. . . 4 ⊢ ((𝑆 ∈ AssAlg ∧ (Base‘𝑃) ∈ (SubRing‘𝑆) ∧ (Base‘𝑃) ∈ (LSubSp‘𝑆)) → (𝐴‘(Base‘𝑃)) = (Base‘𝑃))
30	4, 26, 27, 29	syl3anc 1371	. . 3 ⊢ (𝜑 → (𝐴‘(Base‘𝑃)) = (Base‘𝑃))
31	25, 30	sseqtrd 4022	. 2 ⊢ (𝜑 → (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))
32		eqid 2732	. . . 4 ⊢ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} = {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}
33		eqid 2732	. . . 4 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
34		eqid 2732	. . . 4 ⊢ (1_r‘𝑅) = (1_r‘𝑅)
35	2	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝐼 ∈ 𝑊)
36		eqid 2732	. . . 4 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝑃)
37	12	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 ∈ Ring)
38		simpr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (Base‘𝑃))
39	5, 32, 33, 34, 35, 6, 36, 37, 38	mplcoe1 21811	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σ_g (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))))))
40		eqid 2732	. . . 4 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
41	5	mplring 21797	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ Ring)
42	2, 12, 41	syl2anc 584	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Ring)
43		ringabl 20169	. . . . . 6 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Abel)
44	42, 43	syl 17	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ Abel)
45	44	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑃 ∈ Abel)
46		ovex 7444	. . . . . 6 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
47	46	rabex 5332	. . . . 5 ⊢ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ∈ V
48	47	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ∈ V)
49	13	frnd 6725	. . . . . . . 8 ⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑆))
50	23, 7	aspsubrg 21649	. . . . . . . 8 ⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆))
51	4, 49, 50	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑆))
52	5, 1, 6	mplval2 21774	. . . . . . . . 9 ⊢ 𝑃 = (𝑆 ↾_s (Base‘𝑃))
53	52	subsubrg 20488	. . . . . . . 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 20467	. . . . . 6 ⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
57	55, 56	syl 17	. . . . 5 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
58	57	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝐴‘ran 𝑉) ∈ (SubGrp‘𝑃))
59	5	mpllmod 21796	. . . . . . . 8 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring) → 𝑃 ∈ LMod)
60	2, 12, 59	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ LMod)
61	60	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → 𝑃 ∈ LMod)
62	23, 7, 28	asplss 21647	. . . . . . . . 9 ⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆))
63	4, 49, 62	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆))
64	1, 2, 12	psrlmod 21740	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ LMod)
65		eqid 2732	. . . . . . . . . 10 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
66	52, 28, 65	lsslss 20716	. . . . . . . . 9 ⊢ ((𝑆 ∈ LMod ∧ (Base‘𝑃) ∈ (LSubSp‘𝑆)) → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
67	64, 27, 66	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃) ↔ ((𝐴‘ran 𝑉) ∈ (LSubSp‘𝑆) ∧ (𝐴‘ran 𝑉) ⊆ (Base‘𝑃))))
68	63, 31, 67	mpbir2and 711	. . . . . . 7 ⊢ (𝜑 → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃))
69	68	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃))
70		eqid 2732	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅)
71	5, 70, 6, 32, 38	mplelf 21776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥:{𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}⟶(Base‘𝑅))
72	71	ffvelcdmda 7086	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘𝑅))
73	5, 35, 37	mplsca 21791	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑅 = (Scalar‘𝑃))
74	73	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 = (Scalar‘𝑃))
75	74	fveq2d 6895	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
76	72, 75	eleqtrd 2835	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃)))
77	2	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → 𝐼 ∈ 𝑊)
78		eqid 2732	. . . . . . . 8 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
79		eqid 2732	. . . . . . . 8 ⊢ (._g‘(mulGrp‘𝑃)) = (._g‘(mulGrp‘𝑃))
80	3	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ CRing)
81		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin})
82	5, 32, 33, 34, 77, 78, 79, 10, 80, 81	mplcoe2 21815	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))) = ((mulGrp‘𝑃) Σ_g (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧)))))
83		eqid 2732	. . . . . . . . 9 ⊢ (1_r‘𝑃) = (1_r‘𝑃)
84	78, 83	ringidval 20077	. . . . . . . 8 ⊢ (1_r‘𝑃) = (0_g‘(mulGrp‘𝑃))
85	5	mplcrng 21799	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑃 ∈ CRing)
86	2, 3, 85	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ CRing)
87	78	crngmgp 20135	. . . . . . . . . 10 ⊢ (𝑃 ∈ CRing → (mulGrp‘𝑃) ∈ CMnd)
88	86, 87	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ CMnd)
89	88	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (mulGrp‘𝑃) ∈ CMnd)
90	55	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubRing‘𝑃))
91	78	subrgsubm 20475	. . . . . . . . 9 ⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃)))
92	90, 91	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝐴‘ran 𝑉) ∈ (SubMnd‘(mulGrp‘𝑃)))
93		simplll 773	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → 𝜑)
94	32	psrbag 21689	. . . . . . . . . . . . . 14 ⊢ (𝐼 ∈ 𝑊 → (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ₀ ∧ (^◡𝑘 “ ℕ) ∈ Fin)))
95	35, 94	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↔ (𝑘:𝐼⟶ℕ₀ ∧ (^◡𝑘 “ ℕ) ∈ Fin)))
96	95	biimpa 477	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝑘:𝐼⟶ℕ₀ ∧ (^◡𝑘 “ ℕ) ∈ Fin))
97	96	simpld 495	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → 𝑘:𝐼⟶ℕ₀)
98	97	ffvelcdmda 7086	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑘‘𝑧) ∈ ℕ₀)
99	23, 7	aspssid 21651	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘𝑆)) → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
100	4, 49, 99	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
101	100	ad3antrrr 728	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ran 𝑉 ⊆ (𝐴‘ran 𝑉))
102	14	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → 𝑉 Fn 𝐼)
103		fnfvelrn 7082	. . . . . . . . . . . 12 ⊢ ((𝑉 Fn 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉)
104	102, 103	sylan 580	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ ran 𝑉)
105	101, 104	sseldd 3983	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉))
106	78, 6	mgpbas 20034	. . . . . . . . . . 11 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
107		eqid 2732	. . . . . . . . . . . 12 ⊢ (._r‘𝑃) = (._r‘𝑃)
108	78, 107	mgpplusg 20032	. . . . . . . . . . 11 ⊢ (._r‘𝑃) = (+_g‘(mulGrp‘𝑃))
109	107	subrgmcl 20474	. . . . . . . . . . . 12 ⊢ (((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(._r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉))
110	55, 109	syl3an1 1163	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴‘ran 𝑉) ∧ 𝑣 ∈ (𝐴‘ran 𝑉)) → (𝑢(._r‘𝑃)𝑣) ∈ (𝐴‘ran 𝑉))
111	83	subrg1cl 20470	. . . . . . . . . . . 12 ⊢ ((𝐴‘ran 𝑉) ∈ (SubRing‘𝑃) → (1_r‘𝑃) ∈ (𝐴‘ran 𝑉))
112	55, 111	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (1_r‘𝑃) ∈ (𝐴‘ran 𝑉))
113	106, 79, 108, 88, 31, 110, 84, 112	mulgnn0subcl 19003	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘‘𝑧) ∈ ℕ₀ ∧ (𝑉‘𝑧) ∈ (𝐴‘ran 𝑉)) → ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉))
114	93, 98, 105, 113	syl3anc 1371	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ 𝐼) → ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧)) ∈ (𝐴‘ran 𝑉))
115	114	fmpttd 7116	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧))):𝐼⟶(𝐴‘ran 𝑉))
116	2	mptexd 7228	. . . . . . . . . 10 ⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V)
117	116	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V)
118		funmpt 6586	. . . . . . . . . 10 ⊢ Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧)))
119	118	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧))))
120		fvexd 6906	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (1_r‘𝑃) ∈ V)
121	96	simprd 496	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (^◡𝑘 “ ℕ) ∈ Fin)
122		elrabi 3677	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} → 𝑘 ∈ (ℕ₀ ↑_m 𝐼))
123		elmapi 8845	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (ℕ₀ ↑_m 𝐼) → 𝑘:𝐼⟶ℕ₀)
124	123	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ₀ ↑_m 𝐼)) → 𝑘:𝐼⟶ℕ₀)
125	2	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ₀ ↑_m 𝐼)) → 𝐼 ∈ 𝑊)
126		fcdmnn0supp 12532	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘:𝐼⟶ℕ₀) → (𝑘 supp 0) = (^◡𝑘 “ ℕ))
127	125, 124, 126	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ₀ ↑_m 𝐼)) → (𝑘 supp 0) = (^◡𝑘 “ ℕ))
128		eqimss 4040	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 supp 0) = (^◡𝑘 “ ℕ) → (𝑘 supp 0) ⊆ (^◡𝑘 “ ℕ))
129	127, 128	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ₀ ↑_m 𝐼)) → (𝑘 supp 0) ⊆ (^◡𝑘 “ ℕ))
130		c0ex 11212	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
131	130	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ₀ ↑_m 𝐼)) → 0 ∈ V)
132	124, 129, 125, 131	suppssr 8183	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ (ℕ₀ ↑_m 𝐼)) ∧ 𝑧 ∈ (𝐼 ∖ (^◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0)
133	122, 132	sylanl2 679	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (^◡𝑘 “ ℕ))) → (𝑘‘𝑧) = 0)
134	133	oveq1d 7426	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (^◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (0(._g‘(mulGrp‘𝑃))(𝑉‘𝑧)))
135	2	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (^◡𝑘 “ ℕ))) → 𝐼 ∈ 𝑊)
136	12	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (^◡𝑘 “ ℕ))) → 𝑅 ∈ Ring)
137		eldifi 4126	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝐼 ∖ (^◡𝑘 “ ℕ)) → 𝑧 ∈ 𝐼)
138	137	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (^◡𝑘 “ ℕ))) → 𝑧 ∈ 𝐼)
139	5, 10, 6, 135, 136, 138	mvrcl 21770	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (^◡𝑘 “ ℕ))) → (𝑉‘𝑧) ∈ (Base‘𝑃))
140	106, 84, 79	mulg0 18993	. . . . . . . . . . . 12 ⊢ ((𝑉‘𝑧) ∈ (Base‘𝑃) → (0(._g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1_r‘𝑃))
141	139, 140	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (^◡𝑘 “ ℕ))) → (0(._g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1_r‘𝑃))
142	134, 141	eqtrd 2772	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) ∧ 𝑧 ∈ (𝐼 ∖ (^◡𝑘 “ ℕ))) → ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧)) = (1_r‘𝑃))
143	142, 77	suppss2 8187	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1_r‘𝑃)) ⊆ (^◡𝑘 “ ℕ))
144		suppssfifsupp 9380	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∈ V ∧ Fun (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧))) ∧ (1_r‘𝑃) ∈ V) ∧ ((^◡𝑘 “ ℕ) ∈ Fin ∧ ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧))) supp (1_r‘𝑃)) ⊆ (^◡𝑘 “ ℕ))) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1_r‘𝑃))
145	117, 119, 120, 121, 143, 144	syl32anc 1378	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧))) finSupp (1_r‘𝑃))
146	84, 89, 77, 92, 115, 145	gsumsubmcl 19828	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → ((mulGrp‘𝑃) Σ_g (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧)(._g‘(mulGrp‘𝑃))(𝑉‘𝑧)))) ∈ (𝐴‘ran 𝑉))
147	82, 146	eqeltrd 2833	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))) ∈ (𝐴‘ran 𝑉))
148		eqid 2732	. . . . . . 7 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
149		eqid 2732	. . . . . . 7 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
150	148, 36, 149, 65	lssvscl 20710	. . . . . 6 ⊢ (((𝑃 ∈ LMod ∧ (𝐴‘ran 𝑉) ∈ (LSubSp‘𝑃)) ∧ ((𝑥‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))) ∈ (𝐴‘ran 𝑉))) → ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))) ∈ (𝐴‘ran 𝑉))
151	61, 69, 76, 147, 150	syl22anc 837	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))) ∈ (𝐴‘ran 𝑉))
152	151	fmpttd 7116	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))):{𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}⟶(𝐴‘ran 𝑉))
153	46	mptrabex 7229	. . . . . . 7 ⊢ (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) ∈ V
154		funmpt 6586	. . . . . . 7 ⊢ Fun (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))))
155		fvex 6904	. . . . . . 7 ⊢ (0_g‘𝑃) ∈ V
156	153, 154, 155	3pm3.2i 1339	. . . . . 6 ⊢ ((𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) ∧ (0_g‘𝑃) ∈ V)
157	156	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) ∧ (0_g‘𝑃) ∈ V))
158	5, 1, 7, 33, 6	mplelbas 21769	. . . . . . . 8 ⊢ (𝑥 ∈ (Base‘𝑃) ↔ (𝑥 ∈ (Base‘𝑆) ∧ 𝑥 finSupp (0_g‘𝑅)))
159	158	simprbi 497	. . . . . . 7 ⊢ (𝑥 ∈ (Base‘𝑃) → 𝑥 finSupp (0_g‘𝑅))
160	159	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 finSupp (0_g‘𝑅))
161	160	fsuppimpd 9371	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0_g‘𝑅)) ∈ Fin)
162		ssidd 4005	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑥 supp (0_g‘𝑅)) ⊆ (𝑥 supp (0_g‘𝑅)))
163		fvexd 6906	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0_g‘𝑅) ∈ V)
164	71, 162, 48, 163	suppssr 8183	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0_g‘𝑅)))) → (𝑥‘𝑘) = (0_g‘𝑅))
165	73	fveq2d 6895	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
166	165	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0_g‘𝑅)))) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
167	164, 166	eqtrd 2772	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0_g‘𝑅)))) → (𝑥‘𝑘) = (0_g‘(Scalar‘𝑃)))
168	167	oveq1d 7426	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0_g‘𝑅)))) → ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))) = ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))))
169		eldifi 4126	. . . . . . . 8 ⊢ (𝑘 ∈ ({𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0_g‘𝑅))) → 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin})
170	12	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → 𝑅 ∈ Ring)
171	5, 6, 33, 34, 32, 77, 170, 81	mplmon 21809	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → (𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))) ∈ (Base‘𝑃))
172		eqid 2732	. . . . . . . . . 10 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
173	6, 148, 36, 172, 40	lmod0vs 20649	. . . . . . . . 9 ⊢ ((𝑃 ∈ LMod ∧ (𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))) ∈ (Base‘𝑃)) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))) = (0_g‘𝑃))
174	61, 171, 173	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))) = (0_g‘𝑃))
175	169, 174	sylan2 593	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0_g‘𝑅)))) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))) = (0_g‘𝑃))
176	168, 175	eqtrd 2772	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) ∧ 𝑘 ∈ ({𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ∖ (𝑥 supp (0_g‘𝑅)))) → ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))) = (0_g‘𝑃))
177	176, 48	suppss2 8187	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → ((𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) supp (0_g‘𝑃)) ⊆ (𝑥 supp (0_g‘𝑅)))
178		suppssfifsupp 9380	. . . . 5 ⊢ ((((𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) ∈ V ∧ Fun (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) ∧ (0_g‘𝑃) ∈ V) ∧ ((𝑥 supp (0_g‘𝑅)) ∈ Fin ∧ ((𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) supp (0_g‘𝑃)) ⊆ (𝑥 supp (0_g‘𝑅)))) → (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) finSupp (0_g‘𝑃))
179	157, 161, 177, 178	syl12anc 835	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅))))) finSupp (0_g‘𝑃))
180	40, 45, 48, 58, 152, 179	gsumsubgcl 19829	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → (𝑃 Σ_g (𝑘 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ ((𝑥‘𝑘)( ·_𝑠 ‘𝑃)(𝑦 ∈ {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin} ↦ if(𝑦 = 𝑘, (1_r‘𝑅), (0_g‘𝑅)))))) ∈ (𝐴‘ran 𝑉))
181	39, 180	eqeltrd 2833	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 ∈ (𝐴‘ran 𝑉))
182	31, 181	eqelssd 4003	1 ⊢ (𝜑 → (𝐴‘ran 𝑉) = (Base‘𝑃))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3061 {crab 3432 Vcvv 3474 ∖ cdif 3945 ⊆ wss 3948 ifcif 4528 class class class wbr 5148 ↦ cmpt 5231 ^◡ccnv 5675 ran crn 5677 “ cima 5679 Fun wfun 6537 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 (class class class)co 7411 supp csupp 8148 ↑_m cmap 8822 Fincfn 8941 finSupp cfsupp 9363 0cc0 11112 ℕcn 12216 ℕ₀cn0 12476 Basecbs 17148 ._rcmulr 17202 Scalarcsca 17204 ·_𝑠 cvsca 17205 0_gc0g 17389 Σ_g cgsu 17390 SubMndcsubmnd 18704 ._gcmg 18986 SubGrpcsubg 19036 CMndccmn 19689 Abelcabl 19690 mulGrpcmgp 20028 1_rcur 20075 Ringcrg 20127 CRingccrg 20128 SubRingcsubrg 20457 LModclmod 20614 LSubSpclss 20686 AssAlgcasa 21624 AlgSpancasp 21625 mPwSer cmps 21676 mVar cmvr 21677 mPoly cmpl 21678

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7672 df-ofr 7673 df-om 7858 df-1st 7977 df-2nd 7978 df-supp 8149 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-sup 9439 df-oi 9507 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-z 12563 df-dec 12682 df-uz 12827 df-fz 13489 df-fzo 13632 df-seq 13971 df-hash 14295 df-struct 17084 df-sets 17101 df-slot 17119 df-ndx 17131 df-base 17149 df-ress 17178 df-plusg 17214 df-mulr 17215 df-sca 17217 df-vsca 17218 df-ip 17219 df-tset 17220 df-ple 17221 df-ds 17223 df-hom 17225 df-cco 17226 df-0g 17391 df-gsum 17392 df-prds 17397 df-pws 17399 df-mre 17534 df-mrc 17535 df-acs 17537 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-mhm 18705 df-submnd 18706 df-grp 18858 df-minusg 18859 df-sbg 18860 df-mulg 18987 df-subg 19039 df-ghm 19128 df-cntz 19222 df-cmn 19691 df-abl 19692 df-mgp 20029 df-rng 20047 df-ur 20076 df-srg 20081 df-ring 20129 df-cring 20130 df-subrng 20434 df-subrg 20459 df-lmod 20616 df-lss 20687 df-assa 21627 df-asp 21628 df-psr 21681 df-mvr 21682 df-mpl 21683

This theorem is referenced by: mplind 21850 evlseu 21865

W3C validator