ply1degltdimlem - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ply1degltdimlem		Structured version Visualization version GIF version

Theorem ply1degltdimlem 33978

Description: Lemma for ply1degltdim 33979. (Contributed by Thierry Arnoux, 20-Feb-2025.)

**Hypotheses**
Ref	Expression
ply1degltdim.p	⊢ 𝑃 = (Poly₁‘𝑅)
ply1degltdim.d	⊢ 𝐷 = (deg₁‘𝑅)
ply1degltdim.s	⊢ 𝑆 = (^◡𝐷 “ (-∞[,)𝑁))
ply1degltdim.n	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
ply1degltdim.r	⊢ (𝜑 → 𝑅 ∈ DivRing)
ply1degltdim.e	⊢ 𝐸 = (𝑃 ↾_s 𝑆)
ply1degltdimlem.f	⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))

**Assertion**
Ref	Expression
ply1degltdimlem	⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))

Distinct variable groups: 𝑛,𝐸 𝑛,𝐹 𝑛,𝑁 𝑃,𝑛 𝑅,𝑛 𝑆,𝑛 𝜑,𝑛 Allowed substitution hint: 𝐷(𝑛)

Proof of Theorem ply1degltdimlem Dummy variables 𝑎 𝑖 𝑗 𝑘 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ply1degltdim.p	. . . . . 6 ⊢ 𝑃 = (Poly₁‘𝑅)
2		eqid 2761	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		ply1degltdim.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
4	3	ad3antrrr 742	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑁 ∈ ℕ₀)
5		ply1degltdim.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ DivRing)
6	5	drngringd 20820	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Ring)
7	6	ad3antrrr 742	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑅 ∈ Ring)
8		ply1degltdimlem.f	. . . . . 6 ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
9		eqid 2761	. . . . . 6 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
10		eqid 2761	. . . . . 6 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
11		elmapi 8845	. . . . . . . . 9 ⊢ (𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
12	11	adantl 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
13	1	ply1sca 22391	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ DivRing → 𝑅 = (Scalar‘𝑃))
14	5, 13	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
15	14	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
16	15	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
17	16	feq3d 6690	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → (𝑎:(0..^𝑁)⟶(Base‘𝑅) ↔ 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃))))
18	12, 17	mpbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘𝑅))
19	18	ad2antrr 738	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎:(0..^𝑁)⟶(Base‘𝑅))
20		simpr 489	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸))
21		ovexd 7445	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (0..^𝑁) ∈ V)
22	1, 5	ply1lvec 33815	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ LVec)
23	22	lveclmodd 21207	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ LMod)
24		ply1degltdim.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (deg₁‘𝑅)
25		ply1degltdim.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (^◡𝐷 “ (-∞[,)𝑁))
26	1, 24, 25, 3, 6	ply1degltlss 33852	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃))
27		eqid 2761	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
28	27	lsssubg 21057	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝑆 ∈ (SubGrp‘𝑃))
29	23, 26, 28	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑃))
30		subgsubm 19214	. . . . . . . . . 10 ⊢ (𝑆 ∈ (SubGrp‘𝑃) → 𝑆 ∈ (SubMnd‘𝑃))
31	29, 30	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑃))
32	31	ad3antrrr 742	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑆 ∈ (SubMnd‘𝑃))
33		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑃) = (Base‘𝑃)
34	24, 1, 33	deg1xrf 26217	. . . . . . . . . . . . . 14 ⊢ 𝐷:(Base‘𝑃)⟶ℝ^*
35		ffn 6705	. . . . . . . . . . . . . 14 ⊢ (𝐷:(Base‘𝑃)⟶ℝ^* → 𝐷 Fn (Base‘𝑃))
36	34, 35	mp1i 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷 Fn (Base‘𝑃))
37		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
38		eqid 2761	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝑃)
39		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
40	23	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑃 ∈ LMod)
41		simplr 780	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘(Scalar‘𝑃)))
42	33, 27	lssss 21036	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (LSubSp‘𝑃) → 𝑆 ⊆ (Base‘𝑃))
43	26, 42	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑃))
44		ply1degltdim.e	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐸 = (𝑃 ↾_s 𝑆)
45	44, 33	ressbas2 17297	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ⊆ (Base‘𝑃) → 𝑆 = (Base‘𝐸))
46	43, 45	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 = (Base‘𝐸))
47	46, 43	eqsstrrd 3971	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐸) ⊆ (Base‘𝑃))
48	47	sselda 3936	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
49	48	adantlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
50	33, 37, 38, 39, 40, 41, 49	lmodvscld 20979	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ (Base‘𝑃))
51		mnfxr 11265	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
52	51	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ∈ ℝ^*)
53	3	nn0red 12565	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℝ)
54	53	rexrd 11258	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
55	54	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑁 ∈ ℝ^*)
56	34	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷:(Base‘𝑃)⟶ℝ^*)
57	56, 50	ffvelcdmd 7080	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ∈ ℝ^*)
58	57	mnfled 13160	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ≤ (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)))
59	56, 49	ffvelcdmd 7080	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) ∈ ℝ^*)
60	6	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑅 ∈ Ring)
61	15	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
62	41, 61	eleqtrrd 2864	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘𝑅))
63	1, 24, 60, 33, 2, 38, 62, 49	deg1vscale 26240	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ≤ (𝐷‘𝑥))
64		simpll 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝜑)
65		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝐸))
66	46	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑆 = (Base‘𝐸))
67	65, 66	eleqtrrd 2864	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ 𝑆)
68	51	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -∞ ∈ ℝ^*)
69	54	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℝ^*)
70	34, 35	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐷 Fn (Base‘𝑃))
71		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
72	71, 25	eleqtrdi 2871	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁)))
73		elpreima 7053	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 Fn (Base‘𝑃) → (𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁)) ↔ (𝑥 ∈ (Base‘𝑃) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁))))
74	73	simplbda 504	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 Fn (Base‘𝑃) ∧ 𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁))) → (𝐷‘𝑥) ∈ (-∞[,)𝑁))
75	70, 72, 74	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ (-∞[,)𝑁))
76		elico1 13414	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^) → ((𝐷‘𝑥) ∈ (-∞[,)𝑁) ↔ ((𝐷‘𝑥) ∈ ℝ^ ∧ -∞ ≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁)))
77	76	biimpa 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → ((𝐷‘𝑥) ∈ ℝ^ ∧ -∞ ≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁))
78	77	simp3d 1160	. . . . . . . . . . . . . . . . 17 ⊢ (((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → (𝐷‘𝑥) < 𝑁)
79	68, 69, 75, 78	syl21anc 850	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) < 𝑁)
80	64, 67, 79	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) < 𝑁)
81	57, 59, 55, 63, 80	xrlelttrd 13184	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) < 𝑁)
82	52, 55, 57, 58, 81	elicod 13421	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ∈ (-∞[,)𝑁))
83	36, 50, 82	elpreimad 7054	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
84	83, 25	eleqtrrdi 2872	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
85	84	anasss 471	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
86	85	ad5ant15 770	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
87	12	ad2antrr 738	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
88	34, 35	mp1i 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝐷 Fn (Base‘𝑃))
89		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
90	89, 33	mgpbas 20220	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
91		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (._g‘(mulGrp‘𝑃)) = (._g‘(mulGrp‘𝑃))
92	1	ply1ring 22386	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
93	89	ringmgp 20320	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
94	6, 92, 93	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
95	94	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (mulGrp‘𝑃) ∈ Mnd)
96		elfzonn0 13735	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℕ₀)
97	96	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ₀)
98		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (var₁‘𝑅) = (var₁‘𝑅)
99	98, 1, 33	vr1cl 22356	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → (var₁‘𝑅) ∈ (Base‘𝑃))
100	6, 99	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (var₁‘𝑅) ∈ (Base‘𝑃))
101	100	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (var₁‘𝑅) ∈ (Base‘𝑃))
102	90, 91, 95, 97, 101	mulgnn0cld 19160	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
103	51	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ∈ ℝ^*)
104	54	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑁 ∈ ℝ^*)
105	24, 1, 33	deg1xrcl 26218	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ ℝ^*)
106	102, 105	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ ℝ^*)
107	106	mnfled 13160	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ≤ (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
108	96	nn0red 12565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ)
109	108	rexrd 11258	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ^*)
110	109	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℝ^*)
111	24, 1, 98, 89, 91	deg1pwle 26256	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ₀) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ≤ 𝑛)
112	6, 96, 111	syl2an 607	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ≤ 𝑛)
113		elfzolt2 13696	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 < 𝑁)
114	113	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 < 𝑁)
115	106, 110, 104, 112, 114	xrlelttrd 13184	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) < 𝑁)
116	103, 104, 106, 107, 115	elicod 13421	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ (-∞[,)𝑁))
117	88, 102, 116	elpreimad 7054	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
118	117, 25	eleqtrrdi 2872	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝑆)
119	46	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑆 = (Base‘𝐸))
120	118, 119	eleqtrd 2863	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸))
121	120, 8	fmptd 7109	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
122	121	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
123		inidm 4178	. . . . . . . . 9 ⊢ ((0..^𝑁) ∩ (0..^𝑁)) = (0..^𝑁)
124	86, 87, 122, 21, 21, 123	off 7692	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹):(0..^𝑁)⟶𝑆)
125	21, 32, 124, 44	gsumsubm 18893	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
126		ringmnd 20324	. . . . . . . . . 10 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd)
127	6, 92, 126	3syl 19	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ Mnd)
128	34, 35	mp1i 14	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 Fn (Base‘𝑃))
129	33, 10	mndidcl 18806	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Mnd → (0_g‘𝑃) ∈ (Base‘𝑃))
130	127, 129	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (0_g‘𝑃) ∈ (Base‘𝑃))
131	51	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ∈ ℝ^*)
132	24, 1, 33	deg1xrcl 26218	. . . . . . . . . . . . 13 ⊢ ((0_g‘𝑃) ∈ (Base‘𝑃) → (𝐷‘(0_g‘𝑃)) ∈ ℝ^*)
133	130, 132	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) ∈ ℝ^*)
134	133	mnfled 13160	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ≤ (𝐷‘(0_g‘𝑃)))
135	24, 1, 10	deg1z 26223	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (𝐷‘(0_g‘𝑃)) = -∞)
136	6, 135	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) = -∞)
137	53	mnfltd 13148	. . . . . . . . . . . . 13 ⊢ (𝜑 → -∞ < 𝑁)
138	136, 137	eqbrtrd 5132	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) < 𝑁)
139	131, 54, 133, 134, 138	elicod 13421	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) ∈ (-∞[,)𝑁))
140	128, 130, 139	elpreimad 7054	. . . . . . . . . 10 ⊢ (𝜑 → (0_g‘𝑃) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
141	140, 25	eleqtrrdi 2872	. . . . . . . . 9 ⊢ (𝜑 → (0_g‘𝑃) ∈ 𝑆)
142	44, 33, 10	ress0g 18819	. . . . . . . . 9 ⊢ ((𝑃 ∈ Mnd ∧ (0_g‘𝑃) ∈ 𝑆 ∧ 𝑆 ⊆ (Base‘𝑃)) → (0_g‘𝑃) = (0_g‘𝐸))
143	127, 141, 43, 142	syl3anc 1396	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑃) = (0_g‘𝐸))
144	143	ad3antrrr 742	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (0_g‘𝑃) = (0_g‘𝐸))
145	20, 125, 144	3eqtr4d 2806	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝑃))
146	1, 2, 4, 7, 8, 9, 10, 19, 145	ply1gsumz 33855	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘𝑅)}))
147	14	fveq2d 6885	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
148	147	sneqd 4600	. . . . . . 7 ⊢ (𝜑 → {(0_g‘𝑅)} = {(0_g‘(Scalar‘𝑃))})
149	148	xpeq2d 5691	. . . . . 6 ⊢ (𝜑 → ((0..^𝑁) × {(0_g‘𝑅)}) = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
150	149	ad3antrrr 742	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → ((0..^𝑁) × {(0_g‘𝑅)}) = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
151	146, 150	eqtrd 2796	. . . 4 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
152	151	expl 462	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → ((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))})))
153	152	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))})))
154	118, 8	fmptd 7109	. . . . . 6 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶𝑆)
155	154	frnd 6714	. . . . 5 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑆)
156		eqid 2761	. . . . . 6 ⊢ (LSpan‘𝑃) = (LSpan‘𝑃)
157	27, 156	lspssp 21088	. . . . 5 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
158	23, 26, 155, 157	syl3anc 1396	. . . 4 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
159		breq1 5111	. . . . . . . 8 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑎 finSupp (0_g‘(Scalar‘𝑃)) ↔ ((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃))))
160		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))
161	160	oveq2d 7426	. . . . . . . . 9 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
162	161	eqeq2d 2772	. . . . . . . 8 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) ↔ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
163	159, 162	anbi12d 643	. . . . . . 7 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → ((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹))) ↔ (((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
164		fvexd 6896	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘(Scalar‘𝑃)) ∈ V)
165		ovexd 7445	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ V)
166	43	sselda 3936	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑃))
167		eqid 2761	. . . . . . . . . . . 12 ⊢ (coe₁‘𝑥) = (coe₁‘𝑥)
168	167, 33, 1, 2	coe1f 22350	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (Base‘𝑃) → (coe₁‘𝑥):ℕ₀⟶(Base‘𝑅))
169	166, 168	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥):ℕ₀⟶(Base‘𝑅))
170	15	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
171	170	feq3d 6690	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥):ℕ₀⟶(Base‘𝑅) ↔ (coe₁‘𝑥):ℕ₀⟶(Base‘(Scalar‘𝑃))))
172	169, 171	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥):ℕ₀⟶(Base‘(Scalar‘𝑃)))
173		fzo0ssnn0 13774	. . . . . . . . . 10 ⊢ (0..^𝑁) ⊆ ℕ₀
174	173	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ ℕ₀)
175	172, 174	fssresd 6745	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)):(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
176	164, 165, 175	elmapdd 8837	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)) ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁)))
177	169	ffund 6710	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (coe₁‘𝑥))
178		fzofi 14009	. . . . . . . . . 10 ⊢ (0..^𝑁) ∈ Fin
179	178	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ Fin)
180		fvexd 6896	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0_g‘(Scalar‘𝑃)) ∈ V)
181	177, 179, 180	resfifsupp 9356	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)))
182		ringcmn 20364	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
183	6, 92, 182	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ CMnd)
184	183	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑃 ∈ CMnd)
185		nn0ex 12509	. . . . . . . . . . 11 ⊢ ℕ₀ ∈ V
186	185	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ℕ₀ ∈ V)
187	23	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑃 ∈ LMod)
188	172	ffvelcdmda 7079	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → ((coe₁‘𝑥)‘𝑖) ∈ (Base‘(Scalar‘𝑃)))
189	6	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑅 ∈ Ring)
190	189, 92, 93	3syl 19	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (mulGrp‘𝑃) ∈ Mnd)
191		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℕ₀)
192	189, 99	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (var₁‘𝑅) ∈ (Base‘𝑃))
193	90, 91, 190, 191, 192	mulgnn0cld 19160	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
194	33, 37, 38, 39, 187, 188, 193	lmodvscld 20979	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ (Base‘𝑃))
195		eqid 2761	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) = (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
196	194, 195	fmptd 7109	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))):ℕ₀⟶(Base‘𝑃))
197		nfv 1942	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑥 ∈ 𝑆)
198	197, 194, 195	fnmptd 6676	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) Fn ℕ₀)
199		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((coe₁‘𝑥)‘𝑖) = ((coe₁‘𝑥)‘𝑗))
200		oveq1 7417	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
201	199, 200	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
202		simplr 780	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℕ₀)
203		ovexd 7445	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ V)
204	195, 201, 202, 203	fvmptd3 7013	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
205	166	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑥 ∈ (Base‘𝑃))
206		icossxr 13458	. . . . . . . . . . . . . . . . 17 ⊢ (-∞[,)𝑁) ⊆ ℝ^*
207	206, 75	sselid 3934	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ ℝ^*)
208	207	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) ∈ ℝ^*)
209	54	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑁 ∈ ℝ^*)
210	202	nn0red 12565	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ)
211	210	rexrd 11258	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ^*)
212	79	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑁)
213		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑁 ≤ 𝑗)
214	208, 209, 211, 212, 213	xrltletrd 13185	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑗)
215	24, 1, 33, 9, 167	deg1lt 26233	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (Base‘𝑃) ∧ 𝑗 ∈ ℕ₀ ∧ (𝐷‘𝑥) < 𝑗) → ((coe₁‘𝑥)‘𝑗) = (0_g‘𝑅))
216	205, 202, 214, 215	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((coe₁‘𝑥)‘𝑗) = (0_g‘𝑅))
217	216	oveq1d 7425	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
218	147	ad3antrrr 742	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
219	218	oveq1d 7425	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
220	23	ad3antrrr 742	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑃 ∈ LMod)
221	94	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (mulGrp‘𝑃) ∈ Mnd)
222	100	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (var₁‘𝑅) ∈ (Base‘𝑃))
223	90, 91, 221, 202, 222	mulgnn0cld 19160	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
224		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
225	33, 37, 38, 224, 10	lmod0vs 20995	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ LMod ∧ (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃)) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
226	220, 223, 225	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
227	219, 226	eqtrd 2796	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
228	204, 217, 227	3eqtrd 2800	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (0_g‘𝑃))
229	3	nn0zd 12615	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
230	229	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℤ)
231	198, 228, 230	suppssnn0 33116	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) supp (0_g‘𝑃)) ⊆ (0..^𝑁))
232	186	mptexd 7222	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ∈ V)
233	198	fnfund 6636	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))))
234		fvexd 6896	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0_g‘𝑃) ∈ V)
235		suppssfifsupp 9339	. . . . . . . . . . 11 ⊢ ((((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ∈ V ∧ Fun (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ∧ (0_g‘𝑃) ∈ V) ∧ ((0..^𝑁) ∈ Fin ∧ ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) supp (0_g‘𝑃)) ⊆ (0..^𝑁))) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) finSupp (0_g‘𝑃))
236	232, 233, 234, 179, 231, 235	syl32anc 1403	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) finSupp (0_g‘𝑃))
237	33, 10, 184, 186, 196, 231, 236	gsumres 19982	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σ_g ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁))) = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
238		fvexd 6896	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥) ∈ V)
239		ovexd 7445	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^𝑁) ∈ V)
240	154, 239	fexd 7225	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ V)
241	240	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 ∈ V)
242		offres 7979	. . . . . . . . . . . 12 ⊢ (((coe₁‘𝑥) ∈ V ∧ 𝐹 ∈ V) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))))
243	238, 241, 242	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))))
244	169	ffnd 6706	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥) Fn ℕ₀)
245	154	ffnd 6706	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 Fn (0..^𝑁))
246	245	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 Fn (0..^𝑁))
247		sseqin2 4175	. . . . . . . . . . . . . . . 16 ⊢ ((0..^𝑁) ⊆ ℕ₀ ↔ (ℕ₀ ∩ (0..^𝑁)) = (0..^𝑁))
248	173, 247	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ (ℕ₀ ∩ (0..^𝑁)) = (0..^𝑁)
249		eqidd 2762	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) → ((coe₁‘𝑥)‘𝑗) = ((coe₁‘𝑥)‘𝑗))
250		oveq1 7417	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
251		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
252		ovexd 7445	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ V)
253	8, 250, 251, 252	fvmptd3 7013	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹‘𝑗) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
254	244, 246, 186, 165, 248, 249, 253	ofval 7685	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
255	173, 251	sselid 3934	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ₀)
256		ovexd 7445	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ V)
257	195, 201, 255, 256	fvmptd3 7013	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
258	254, 257	eqtr4d 2799	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗))
259	258	ralrimiva 3155	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑗 ∈ (0..^𝑁)(((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗))
260	244, 246, 186, 165, 248	offn 7687	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) Fn (0..^𝑁))
261		ssidd 3959	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ (0..^𝑁))
262		fvreseq0 7033	. . . . . . . . . . . . 13 ⊢ (((((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) Fn (0..^𝑁) ∧ (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) Fn ℕ₀) ∧ ((0..^𝑁) ⊆ (0..^𝑁) ∧ (0..^𝑁) ⊆ ℕ₀)) → ((((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)) ↔ ∀𝑗 ∈ (0..^𝑁)(((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗)))
263	260, 198, 261, 174, 262	syl22anc 851	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)) ↔ ∀𝑗 ∈ (0..^𝑁)(((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗)))
264	259, 263	mpbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)))
265		fnresdm 6654	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn (0..^𝑁) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
266	245, 265	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) = 𝐹)
267	266	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
268	267	oveq2d 7426	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))
269	243, 264, 268	3eqtr3rd 2805	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)))
270	269	oveq2d 7426	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝑃 Σ_g ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁))))
271	6	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ Ring)
272	1, 98, 33, 38, 89, 91, 167	ply1coe 22437	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
273	271, 166, 272	syl2anc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
274	237, 270, 273	3eqtr4rd 2807	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
275	181, 274	jca 520	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
276	163, 176, 275	rspcedvdw 3583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
277	102, 8	fmptd 7109	. . . . . . . 8 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝑃))
278	156, 33, 39, 37, 224, 38, 277, 23, 239	ellspd 21931	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
279	278	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
280	276, 279	mpbird 260	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
281		imadmrn 6072	. . . . . . . 8 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
282	154	fdmd 6716	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = (0..^𝑁))
283	282	imaeq2d 6062	. . . . . . . 8 ⊢ (𝜑 → (𝐹 “ dom 𝐹) = (𝐹 “ (0..^𝑁)))
284	281, 283	eqtr3id 2810	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 = (𝐹 “ (0..^𝑁)))
285	284	fveq2d 6885	. . . . . 6 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
286	285	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
287	280, 286	eleqtrrd 2864	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘ran 𝐹))
288	158, 287	eqelssd 3957	. . 3 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = 𝑆)
289		eqid 2761	. . . . . 6 ⊢ (LSpan‘𝐸) = (LSpan‘𝐸)
290	44, 156, 289, 27	lsslsp 21115	. . . . 5 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝐸)‘ran 𝐹) = ((LSpan‘𝑃)‘ran 𝐹))
291	290	eqcomd 2767	. . . 4 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
292	23, 26, 155, 291	syl3anc 1396	. . 3 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
293	288, 292, 46	3eqtr3d 2804	. 2 ⊢ (𝜑 → ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸))
294		eqid 2761	. . 3 ⊢ (Base‘𝐸) = (Base‘𝐸)
295	24	fvexi 6895	. . . . . . 7 ⊢ 𝐷 ∈ V
296		cnvexg 7920	. . . . . . 7 ⊢ (𝐷 ∈ V → ^◡𝐷 ∈ V)
297		imaexg 7909	. . . . . . 7 ⊢ (^◡𝐷 ∈ V → (^◡𝐷 “ (-∞[,)𝑁)) ∈ V)
298	295, 296, 297	mp2b 10	. . . . . 6 ⊢ (^◡𝐷 “ (-∞[,)𝑁)) ∈ V
299	25, 298	eqeltri 2857	. . . . 5 ⊢ 𝑆 ∈ V
300	44, 37	resssca 17395	. . . . 5 ⊢ (𝑆 ∈ V → (Scalar‘𝑃) = (Scalar‘𝐸))
301	299, 300	ax-mp 5	. . . 4 ⊢ (Scalar‘𝑃) = (Scalar‘𝐸)
302	301	fveq2i 6884	. . 3 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝐸))
303		eqid 2761	. . 3 ⊢ (Scalar‘𝐸) = (Scalar‘𝐸)
304	44, 38	ressvsca 17396	. . . 4 ⊢ (𝑆 ∈ V → ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝐸))
305	299, 304	ax-mp 5	. . 3 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝐸)
306		eqid 2761	. . 3 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
307	301	fveq2i 6884	. . 3 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝐸))
308		eqid 2761	. . 3 ⊢ (LBasis‘𝐸) = (LBasis‘𝐸)
309	44, 27	lsslvec 21209	. . . . 5 ⊢ ((𝑃 ∈ LVec ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝐸 ∈ LVec)
310	22, 26, 309	syl2anc 595	. . . 4 ⊢ (𝜑 → 𝐸 ∈ LVec)
311	310	lveclmodd 21207	. . 3 ⊢ (𝜑 → 𝐸 ∈ LMod)
312	14, 5	eqeltrrd 2862	. . . . 5 ⊢ (𝜑 → (Scalar‘𝑃) ∈ DivRing)
313		drngnzr 20833	. . . . 5 ⊢ ((Scalar‘𝑃) ∈ DivRing → (Scalar‘𝑃) ∈ NzRing)
314	312, 313	syl 18	. . . 4 ⊢ (𝜑 → (Scalar‘𝑃) ∈ NzRing)
315	301, 314	eqeltrrid 2866	. . 3 ⊢ (𝜑 → (Scalar‘𝐸) ∈ NzRing)
316	120	ralrimiva 3155	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸))
317		drngnzr 20833	. . . . . . . . . 10 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
318	5, 317	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ NzRing)
319	318	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑅 ∈ NzRing)
320	97	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ₀)
321		elfzonn0 13735	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℕ₀)
322	321	adantl 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ ℕ₀)
323	1, 98, 91, 319, 320, 322	ply1moneq 33844	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ↔ 𝑛 = 𝑖))
324	323	biimpd 232	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
325	324	anasss 471	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (0..^𝑁) ∧ 𝑖 ∈ (0..^𝑁))) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
326	325	ralrimivva 3206	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
327		oveq1 7417	. . . . 5 ⊢ (𝑛 = 𝑖 → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
328	8, 327	f1mpt 7259	. . . 4 ⊢ (𝐹:(0..^𝑁)–1-1→(Base‘𝐸) ↔ (∀𝑛 ∈ (0..^𝑁)(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸) ∧ ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖)))
329	316, 326, 328	sylanbrc 594	. . 3 ⊢ (𝜑 → 𝐹:(0..^𝑁)–1-1→(Base‘𝐸))
330	294, 302, 303, 305, 306, 307, 308, 289, 311, 315, 239, 329	islbs5 33659	. 2 ⊢ (𝜑 → (ran 𝐹 ∈ (LBasis‘𝐸) ↔ (∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))})) ∧ ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸))))
331	153, 293, 330	mpbir2and 725	1 ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1568 ∈ wcel 2141 ∀wral 3077 ∃wrex 3087 Vcvv 3453 ∩ cin 3903 ⊆ wss 3904 {csn 4588 class class class wbr 5108 ↦ cmpt 5191 × cxp 5659 ^◡ccnv 5660 dom cdm 5661 ran crn 5662 ↾ cres 5663 “ cima 5664 Fun wfun 6530 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 ‘cfv 6536 (class class class)co 7410 ∘_f cof 7672 supp csupp 8155 ↑_m cmap 8823 Fincfn 8942 finSupp cfsupp 9320 0cc0 11099 -∞cmnf 11240 ℝ^*cxr 11241 < clt 11242 ≤ cle 11243 ℕ₀cn0 12503 ℤcz 12590 [,)cico 13373 ..^cfzo 13681 Basecbs 17268 ↾_s cress 17289 Scalarcsca 17312 ·_𝑠 cvsca 17313 0_gc0g 17491 Σ_g cgsu 17492 Mndcmnd 18791 SubMndcsubmnd 18839 ._gcmg 19132 SubGrpcsubg 19185 CMndccmn 19849 mulGrpcmgp 20215 Ringcrg 20314 NzRingcnzr 20594 DivRingcdr 20812 LModclmod 20960 LSubSpclss 21031 LSpanclspn 21071 LBasisclbs 21174 LVecclvec 21202 var₁cv1 22315 Poly₁cpl1 22316 coe₁cco1 22317 deg₁cdg1 26190

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-pre-sup 11177 ax-addf 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-ofr 7675 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-tpos 8221 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-er 8693 df-map 8825 df-pm 8826 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-sup 9401 df-oi 9471 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-z 12591 df-dec 12711 df-uz 12862 df-ico 13377 df-fz 13535 df-fzo 13682 df-seq 14037 df-hash 14366 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-starv 17324 df-sca 17325 df-vsca 17326 df-ip 17327 df-tset 17328 df-ple 17329 df-ds 17331 df-unif 17332 df-hom 17333 df-cco 17334 df-0g 17493 df-gsum 17494 df-prds 17499 df-pws 17501 df-mre 17637 df-mrc 17638 df-acs 17640 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-mhm 18840 df-submnd 18841 df-grp 19002 df-minusg 19003 df-sbg 19004 df-mulg 19133 df-subg 19188 df-ghm 19283 df-cntz 19386 df-cmn 19851 df-abl 19852 df-mgp 20216 df-rng 20230 df-ur 20263 df-srg 20268 df-ring 20316 df-cring 20317 df-oppr 20418 df-dvdsr 20438 df-unit 20439 df-nzr 20595 df-subrng 20630 df-subrg 20654 df-drng 20814 df-lmod 20962 df-lss 21032 df-lsp 21072 df-lmhm 21122 df-lbs 21175 df-lvec 21203 df-sra 21273 df-rgmod 21274 df-cnfld 21502 df-dsmm 21861 df-frlm 21876 df-uvc 21912 df-lindf 21935 df-linds 21936 df-psr 22038 df-mvr 22039 df-mpl 22040 df-opsr 22042 df-psr1 22319 df-vr1 22320 df-ply1 22321 df-coe1 22322 df-mdeg 26191 df-deg1 26192

This theorem is referenced by: ply1degltdim 33979

W3C validator