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 33390

Description: Lemma for ply1degltdim 33391. (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 2725	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		ply1degltdim.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
4	3	ad3antrrr 728	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑁 ∈ ℕ₀)
5		ply1degltdim.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ DivRing)
6	5	drngringd 20636	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Ring)
7	6	ad3antrrr 728	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑅 ∈ Ring)
8		ply1degltdimlem.f	. . . . . 6 ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
9		eqid 2725	. . . . . 6 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
10		eqid 2725	. . . . . 6 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
11		elmapi 8866	. . . . . . . . 9 ⊢ (𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
12	11	adantl 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
13	1	ply1sca 22180	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ DivRing → 𝑅 = (Scalar‘𝑃))
14	5, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
15	14	fveq2d 6898	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
16	15	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
17	16	feq3d 6708	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → (𝑎:(0..^𝑁)⟶(Base‘𝑅) ↔ 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃))))
18	12, 17	mpbird 256	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘𝑅))
19	18	ad2antrr 724	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎:(0..^𝑁)⟶(Base‘𝑅))
20		simpr 483	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸))
21		ovexd 7452	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (0..^𝑁) ∈ V)
22	1, 5	ply1lvec 33317	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ LVec)
23	22	lveclmodd 20996	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ LMod)
24		ply1degltdim.d	. . . . . . . . . . . 12 ⊢ 𝐷 = ( deg₁ ‘𝑅)
25		ply1degltdim.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (^◡𝐷 “ (-∞[,)𝑁))
26	1, 24, 25, 3, 6	ply1degltlss 33337	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃))
27		eqid 2725	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
28	27	lsssubg 20845	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝑆 ∈ (SubGrp‘𝑃))
29	23, 26, 28	syl2anc 582	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑃))
30		subgsubm 19107	. . . . . . . . . 10 ⊢ (𝑆 ∈ (SubGrp‘𝑃) → 𝑆 ∈ (SubMnd‘𝑃))
31	29, 30	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑃))
32	31	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑆 ∈ (SubMnd‘𝑃))
33		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑃) = (Base‘𝑃)
34	24, 1, 33	deg1xrf 26047	. . . . . . . . . . . . . 14 ⊢ 𝐷:(Base‘𝑃)⟶ℝ^*
35		ffn 6721	. . . . . . . . . . . . . 14 ⊢ (𝐷:(Base‘𝑃)⟶ℝ^* → 𝐷 Fn (Base‘𝑃))
36	34, 35	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷 Fn (Base‘𝑃))
37		eqid 2725	. . . . . . . . . . . . . 14 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
38		eqid 2725	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝑃)
39		eqid 2725	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
40	23	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑃 ∈ LMod)
41		simplr 767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘(Scalar‘𝑃)))
42	33, 27	lssss 20824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (LSubSp‘𝑃) → 𝑆 ⊆ (Base‘𝑃))
43	26, 42	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑃))
44		ply1degltdim.e	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐸 = (𝑃 ↾_s 𝑆)
45	44, 33	ressbas2 17217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ⊆ (Base‘𝑃) → 𝑆 = (Base‘𝐸))
46	43, 45	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 = (Base‘𝐸))
47	46, 43	eqsstrrd 4017	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐸) ⊆ (Base‘𝑃))
48	47	sselda 3977	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
49	48	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
50	33, 37, 38, 39, 40, 41, 49	lmodvscld 20766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ (Base‘𝑃))
51		mnfxr 11301	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
52	51	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ∈ ℝ^*)
53	3	nn0red 12563	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℝ)
54	53	rexrd 11294	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
55	54	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑁 ∈ ℝ^*)
56	34	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷:(Base‘𝑃)⟶ℝ^*)
57	56, 50	ffvelcdmd 7092	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ∈ ℝ^*)
58	57	mnfled 13147	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ≤ (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)))
59	56, 49	ffvelcdmd 7092	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) ∈ ℝ^*)
60	6	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑅 ∈ Ring)
61	15	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
62	41, 61	eleqtrrd 2828	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘𝑅))
63	1, 24, 60, 33, 2, 38, 62, 49	deg1vscale 26070	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ≤ (𝐷‘𝑥))
64		simpll 765	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝜑)
65		simpr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝐸))
66	46	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑆 = (Base‘𝐸))
67	65, 66	eleqtrrd 2828	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ 𝑆)
68	51	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -∞ ∈ ℝ^*)
69	54	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℝ^*)
70	34, 35	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐷 Fn (Base‘𝑃))
71		simpr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
72	71, 25	eleqtrdi 2835	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁)))
73		elpreima 7064	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 Fn (Base‘𝑃) → (𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁)) ↔ (𝑥 ∈ (Base‘𝑃) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁))))
74	73	simplbda 498	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 Fn (Base‘𝑃) ∧ 𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁))) → (𝐷‘𝑥) ∈ (-∞[,)𝑁))
75	70, 72, 74	syl2anc 582	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ (-∞[,)𝑁))
76		elico1 13399	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^) → ((𝐷‘𝑥) ∈ (-∞[,)𝑁) ↔ ((𝐷‘𝑥) ∈ ℝ^ ∧ -∞ ≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁)))
77	76	biimpa 475	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → ((𝐷‘𝑥) ∈ ℝ^ ∧ -∞ ≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁))
78	77	simp3d 1141	. . . . . . . . . . . . . . . . 17 ⊢ (((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → (𝐷‘𝑥) < 𝑁)
79	68, 69, 75, 78	syl21anc 836	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) < 𝑁)
80	64, 67, 79	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) < 𝑁)
81	57, 59, 55, 63, 80	xrlelttrd 13171	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) < 𝑁)
82	52, 55, 57, 58, 81	elicod 13406	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ∈ (-∞[,)𝑁))
83	36, 50, 82	elpreimad 7065	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
84	83, 25	eleqtrrdi 2836	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
85	84	anasss 465	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
86	85	ad5ant15 757	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
87	12	ad2antrr 724	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
88	34, 35	mp1i 13	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝐷 Fn (Base‘𝑃))
89		eqid 2725	. . . . . . . . . . . . . . . 16 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
90	89, 33	mgpbas 20084	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
91		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ (._g‘(mulGrp‘𝑃)) = (._g‘(mulGrp‘𝑃))
92	1	ply1ring 22175	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
93	89	ringmgp 20183	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
94	6, 92, 93	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
95	94	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (mulGrp‘𝑃) ∈ Mnd)
96		elfzonn0 13709	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℕ₀)
97	96	adantl 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ₀)
98		eqid 2725	. . . . . . . . . . . . . . . . . 18 ⊢ (var₁‘𝑅) = (var₁‘𝑅)
99	98, 1, 33	vr1cl 22145	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → (var₁‘𝑅) ∈ (Base‘𝑃))
100	6, 99	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (var₁‘𝑅) ∈ (Base‘𝑃))
101	100	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (var₁‘𝑅) ∈ (Base‘𝑃))
102	90, 91, 95, 97, 101	mulgnn0cld 19054	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
103	51	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ∈ ℝ^*)
104	54	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑁 ∈ ℝ^*)
105	24, 1, 33	deg1xrcl 26048	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ ℝ^*)
106	102, 105	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ ℝ^*)
107	106	mnfled 13147	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ≤ (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
108	96	nn0red 12563	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ)
109	108	rexrd 11294	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ^*)
110	109	adantl 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℝ^*)
111	24, 1, 98, 89, 91	deg1pwle 26085	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ₀) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ≤ 𝑛)
112	6, 96, 111	syl2an 594	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ≤ 𝑛)
113		elfzolt2 13673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 < 𝑁)
114	113	adantl 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 < 𝑁)
115	106, 110, 104, 112, 114	xrlelttrd 13171	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) < 𝑁)
116	103, 104, 106, 107, 115	elicod 13406	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ (-∞[,)𝑁))
117	88, 102, 116	elpreimad 7065	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
118	117, 25	eleqtrrdi 2836	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝑆)
119	46	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑆 = (Base‘𝐸))
120	118, 119	eleqtrd 2827	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸))
121	120, 8	fmptd 7121	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
122	121	ad3antrrr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
123		inidm 4218	. . . . . . . . 9 ⊢ ((0..^𝑁) ∩ (0..^𝑁)) = (0..^𝑁)
124	86, 87, 122, 21, 21, 123	off 7701	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹):(0..^𝑁)⟶𝑆)
125	21, 32, 124, 44	gsumsubm 18791	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
126		ringmnd 20187	. . . . . . . . . 10 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd)
127	6, 92, 126	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ Mnd)
128	34, 35	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 Fn (Base‘𝑃))
129	33, 10	mndidcl 18708	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Mnd → (0_g‘𝑃) ∈ (Base‘𝑃))
130	127, 129	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (0_g‘𝑃) ∈ (Base‘𝑃))
131	51	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ∈ ℝ^*)
132	24, 1, 33	deg1xrcl 26048	. . . . . . . . . . . . 13 ⊢ ((0_g‘𝑃) ∈ (Base‘𝑃) → (𝐷‘(0_g‘𝑃)) ∈ ℝ^*)
133	130, 132	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) ∈ ℝ^*)
134	133	mnfled 13147	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ≤ (𝐷‘(0_g‘𝑃)))
135	24, 1, 10	deg1z 26053	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (𝐷‘(0_g‘𝑃)) = -∞)
136	6, 135	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) = -∞)
137	53	mnfltd 13136	. . . . . . . . . . . . 13 ⊢ (𝜑 → -∞ < 𝑁)
138	136, 137	eqbrtrd 5170	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) < 𝑁)
139	131, 54, 133, 134, 138	elicod 13406	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) ∈ (-∞[,)𝑁))
140	128, 130, 139	elpreimad 7065	. . . . . . . . . 10 ⊢ (𝜑 → (0_g‘𝑃) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
141	140, 25	eleqtrrdi 2836	. . . . . . . . 9 ⊢ (𝜑 → (0_g‘𝑃) ∈ 𝑆)
142	44, 33, 10	ress0g 18721	. . . . . . . . 9 ⊢ ((𝑃 ∈ Mnd ∧ (0_g‘𝑃) ∈ 𝑆 ∧ 𝑆 ⊆ (Base‘𝑃)) → (0_g‘𝑃) = (0_g‘𝐸))
143	127, 141, 43, 142	syl3anc 1368	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑃) = (0_g‘𝐸))
144	143	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (0_g‘𝑃) = (0_g‘𝐸))
145	20, 125, 144	3eqtr4d 2775	. . . . . 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 33339	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘𝑅)}))
147	14	fveq2d 6898	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
148	147	sneqd 4641	. . . . . . 7 ⊢ (𝜑 → {(0_g‘𝑅)} = {(0_g‘(Scalar‘𝑃))})
149	148	xpeq2d 5707	. . . . . 6 ⊢ (𝜑 → ((0..^𝑁) × {(0_g‘𝑅)}) = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
150	149	ad3antrrr 728	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → ((0..^𝑁) × {(0_g‘𝑅)}) = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
151	146, 150	eqtrd 2765	. . . 4 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
152	151	expl 456	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → ((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))})))
153	152	ralrimiva 3136	. 2 ⊢ (𝜑 → ∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))})))
154	118, 8	fmptd 7121	. . . . . 6 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶𝑆)
155	154	frnd 6729	. . . . 5 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑆)
156		eqid 2725	. . . . . 6 ⊢ (LSpan‘𝑃) = (LSpan‘𝑃)
157	27, 156	lspssp 20876	. . . . 5 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
158	23, 26, 155, 157	syl3anc 1368	. . . 4 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
159		breq1 5151	. . . . . . . 8 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑎 finSupp (0_g‘(Scalar‘𝑃)) ↔ ((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃))))
160		oveq1 7424	. . . . . . . . . 10 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))
161	160	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
162	161	eqeq2d 2736	. . . . . . . 8 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) ↔ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
163	159, 162	anbi12d 630	. . . . . . 7 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → ((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹))) ↔ (((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
164		fvexd 6909	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘(Scalar‘𝑃)) ∈ V)
165		ovexd 7452	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ V)
166	43	sselda 3977	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑃))
167		eqid 2725	. . . . . . . . . . . 12 ⊢ (coe₁‘𝑥) = (coe₁‘𝑥)
168	167, 33, 1, 2	coe1f 22139	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (Base‘𝑃) → (coe₁‘𝑥):ℕ₀⟶(Base‘𝑅))
169	166, 168	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥):ℕ₀⟶(Base‘𝑅))
170	15	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
171	170	feq3d 6708	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥):ℕ₀⟶(Base‘𝑅) ↔ (coe₁‘𝑥):ℕ₀⟶(Base‘(Scalar‘𝑃))))
172	169, 171	mpbid 231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥):ℕ₀⟶(Base‘(Scalar‘𝑃)))
173		fzo0ssnn0 13745	. . . . . . . . . 10 ⊢ (0..^𝑁) ⊆ ℕ₀
174	173	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ ℕ₀)
175	172, 174	fssresd 6762	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)):(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
176	164, 165, 175	elmapdd 8858	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)) ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁)))
177	169	ffund 6725	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (coe₁‘𝑥))
178		fzofi 13971	. . . . . . . . . 10 ⊢ (0..^𝑁) ∈ Fin
179	178	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ Fin)
180		fvexd 6909	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0_g‘(Scalar‘𝑃)) ∈ V)
181	177, 179, 180	resfifsupp 9420	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)))
182		ringcmn 20222	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
183	6, 92, 182	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ CMnd)
184	183	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑃 ∈ CMnd)
185		nn0ex 12508	. . . . . . . . . . 11 ⊢ ℕ₀ ∈ V
186	185	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ℕ₀ ∈ V)
187	23	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑃 ∈ LMod)
188	172	ffvelcdmda 7091	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → ((coe₁‘𝑥)‘𝑖) ∈ (Base‘(Scalar‘𝑃)))
189	6	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑅 ∈ Ring)
190	189, 92, 93	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (mulGrp‘𝑃) ∈ Mnd)
191		simpr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℕ₀)
192	189, 99	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (var₁‘𝑅) ∈ (Base‘𝑃))
193	90, 91, 190, 191, 192	mulgnn0cld 19054	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
194	33, 37, 38, 39, 187, 188, 193	lmodvscld 20766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ (Base‘𝑃))
195		eqid 2725	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) = (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
196	194, 195	fmptd 7121	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))):ℕ₀⟶(Base‘𝑃))
197		nfv 1909	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑥 ∈ 𝑆)
198	197, 194, 195	fnmptd 6695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) Fn ℕ₀)
199		fveq2 6894	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((coe₁‘𝑥)‘𝑖) = ((coe₁‘𝑥)‘𝑗))
200		oveq1 7424	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
201	199, 200	oveq12d 7435	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
202		simplr 767	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℕ₀)
203		ovexd 7452	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ V)
204	195, 201, 202, 203	fvmptd3 7025	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
205	166	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑥 ∈ (Base‘𝑃))
206		icossxr 13441	. . . . . . . . . . . . . . . . 17 ⊢ (-∞[,)𝑁) ⊆ ℝ^*
207	206, 75	sselid 3975	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ ℝ^*)
208	207	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) ∈ ℝ^*)
209	54	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑁 ∈ ℝ^*)
210	202	nn0red 12563	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ)
211	210	rexrd 11294	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ^*)
212	79	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑁)
213		simpr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑁 ≤ 𝑗)
214	208, 209, 211, 212, 213	xrltletrd 13172	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑗)
215	24, 1, 33, 9, 167	deg1lt 26063	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (Base‘𝑃) ∧ 𝑗 ∈ ℕ₀ ∧ (𝐷‘𝑥) < 𝑗) → ((coe₁‘𝑥)‘𝑗) = (0_g‘𝑅))
216	205, 202, 214, 215	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((coe₁‘𝑥)‘𝑗) = (0_g‘𝑅))
217	216	oveq1d 7432	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
218	147	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
219	218	oveq1d 7432	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
220	23	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑃 ∈ LMod)
221	94	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (mulGrp‘𝑃) ∈ Mnd)
222	100	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (var₁‘𝑅) ∈ (Base‘𝑃))
223	90, 91, 221, 202, 222	mulgnn0cld 19054	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
224		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
225	33, 37, 38, 224, 10	lmod0vs 20782	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ LMod ∧ (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃)) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
226	220, 223, 225	syl2anc 582	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
227	219, 226	eqtrd 2765	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
228	204, 217, 227	3eqtrd 2769	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (0_g‘𝑃))
229	3	nn0zd 12614	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
230	229	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℤ)
231	198, 228, 230	suppssnn0 32631	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) supp (0_g‘𝑃)) ⊆ (0..^𝑁))
232	186	mptexd 7234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ∈ V)
233	198	fnfund 6654	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))))
234		fvexd 6909	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0_g‘𝑃) ∈ V)
235		suppssfifsupp 9403	. . . . . . . . . . 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 1375	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) finSupp (0_g‘𝑃))
237	33, 10, 184, 186, 196, 231, 236	gsumres 19872	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σ_g ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁))) = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
238		fvexd 6909	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥) ∈ V)
239		ovexd 7452	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^𝑁) ∈ V)
240	154, 239	fexd 7237	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ V)
241	240	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 ∈ V)
242		offres 7986	. . . . . . . . . . . 12 ⊢ (((coe₁‘𝑥) ∈ V ∧ 𝐹 ∈ V) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))))
243	238, 241, 242	syl2anc 582	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))))
244	169	ffnd 6722	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥) Fn ℕ₀)
245	154	ffnd 6722	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 Fn (0..^𝑁))
246	245	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 Fn (0..^𝑁))
247		sseqin2 4214	. . . . . . . . . . . . . . . 16 ⊢ ((0..^𝑁) ⊆ ℕ₀ ↔ (ℕ₀ ∩ (0..^𝑁)) = (0..^𝑁))
248	173, 247	mpbi 229	. . . . . . . . . . . . . . 15 ⊢ (ℕ₀ ∩ (0..^𝑁)) = (0..^𝑁)
249		eqidd 2726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) → ((coe₁‘𝑥)‘𝑗) = ((coe₁‘𝑥)‘𝑗))
250		oveq1 7424	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
251		simpr 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
252		ovexd 7452	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ V)
253	8, 250, 251, 252	fvmptd3 7025	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹‘𝑗) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
254	244, 246, 186, 165, 248, 249, 253	ofval 7694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
255	173, 251	sselid 3975	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ₀)
256		ovexd 7452	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ V)
257	195, 201, 255, 256	fvmptd3 7025	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
258	254, 257	eqtr4d 2768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗))
259	258	ralrimiva 3136	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑗 ∈ (0..^𝑁)(((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗))
260	244, 246, 186, 165, 248	offn 7696	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) Fn (0..^𝑁))
261		ssidd 4001	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ (0..^𝑁))
262		fvreseq0 7044	. . . . . . . . . . . . 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 837	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)) ↔ ∀𝑗 ∈ (0..^𝑁)(((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗)))
264	259, 263	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)))
265		fnresdm 6673	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn (0..^𝑁) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
266	245, 265	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) = 𝐹)
267	266	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
268	267	oveq2d 7433	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))
269	243, 264, 268	3eqtr3rd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)))
270	269	oveq2d 7433	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝑃 Σ_g ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁))))
271	6	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ Ring)
272	1, 98, 33, 38, 89, 91, 167	ply1coe 22226	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
273	271, 166, 272	syl2anc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
274	237, 270, 273	3eqtr4rd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
275	181, 274	jca 510	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
276	163, 176, 275	rspcedvdw 3610	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
277	102, 8	fmptd 7121	. . . . . . . 8 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝑃))
278	156, 33, 39, 37, 224, 38, 277, 23, 239	ellspd 21740	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
279	278	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
280	276, 279	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
281		imadmrn 6073	. . . . . . . 8 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
282	154	fdmd 6731	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = (0..^𝑁))
283	282	imaeq2d 6063	. . . . . . . 8 ⊢ (𝜑 → (𝐹 “ dom 𝐹) = (𝐹 “ (0..^𝑁)))
284	281, 283	eqtr3id 2779	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 = (𝐹 “ (0..^𝑁)))
285	284	fveq2d 6898	. . . . . 6 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
286	285	adantr 479	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
287	280, 286	eleqtrrd 2828	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘ran 𝐹))
288	158, 287	eqelssd 3999	. . 3 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = 𝑆)
289		eqid 2725	. . . . . 6 ⊢ (LSpan‘𝐸) = (LSpan‘𝐸)
290	44, 156, 289, 27	lsslsp 20903	. . . . 5 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝐸)‘ran 𝐹) = ((LSpan‘𝑃)‘ran 𝐹))
291	290	eqcomd 2731	. . . 4 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
292	23, 26, 155, 291	syl3anc 1368	. . 3 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
293	288, 292, 46	3eqtr3d 2773	. 2 ⊢ (𝜑 → ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸))
294		eqid 2725	. . 3 ⊢ (Base‘𝐸) = (Base‘𝐸)
295	24	fvexi 6908	. . . . . . 7 ⊢ 𝐷 ∈ V
296		cnvexg 7930	. . . . . . 7 ⊢ (𝐷 ∈ V → ^◡𝐷 ∈ V)
297		imaexg 7919	. . . . . . 7 ⊢ (^◡𝐷 ∈ V → (^◡𝐷 “ (-∞[,)𝑁)) ∈ V)
298	295, 296, 297	mp2b 10	. . . . . 6 ⊢ (^◡𝐷 “ (-∞[,)𝑁)) ∈ V
299	25, 298	eqeltri 2821	. . . . 5 ⊢ 𝑆 ∈ V
300	44, 37	resssca 17323	. . . . 5 ⊢ (𝑆 ∈ V → (Scalar‘𝑃) = (Scalar‘𝐸))
301	299, 300	ax-mp 5	. . . 4 ⊢ (Scalar‘𝑃) = (Scalar‘𝐸)
302	301	fveq2i 6897	. . 3 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝐸))
303		eqid 2725	. . 3 ⊢ (Scalar‘𝐸) = (Scalar‘𝐸)
304	44, 38	ressvsca 17324	. . . 4 ⊢ (𝑆 ∈ V → ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝐸))
305	299, 304	ax-mp 5	. . 3 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝐸)
306		eqid 2725	. . 3 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
307	301	fveq2i 6897	. . 3 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝐸))
308		eqid 2725	. . 3 ⊢ (LBasis‘𝐸) = (LBasis‘𝐸)
309	44, 27	lsslvec 20998	. . . . 5 ⊢ ((𝑃 ∈ LVec ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝐸 ∈ LVec)
310	22, 26, 309	syl2anc 582	. . . 4 ⊢ (𝜑 → 𝐸 ∈ LVec)
311	310	lveclmodd 20996	. . 3 ⊢ (𝜑 → 𝐸 ∈ LMod)
312	14, 5	eqeltrrd 2826	. . . . 5 ⊢ (𝜑 → (Scalar‘𝑃) ∈ DivRing)
313		drngnzr 20648	. . . . 5 ⊢ ((Scalar‘𝑃) ∈ DivRing → (Scalar‘𝑃) ∈ NzRing)
314	312, 313	syl 17	. . . 4 ⊢ (𝜑 → (Scalar‘𝑃) ∈ NzRing)
315	301, 314	eqeltrrid 2830	. . 3 ⊢ (𝜑 → (Scalar‘𝐸) ∈ NzRing)
316	120	ralrimiva 3136	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸))
317		drngnzr 20648	. . . . . . . . . 10 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
318	5, 317	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ NzRing)
319	318	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑅 ∈ NzRing)
320	97	adantr 479	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ₀)
321		elfzonn0 13709	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℕ₀)
322	321	adantl 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ ℕ₀)
323	1, 98, 91, 319, 320, 322	ply1moneq 33334	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ↔ 𝑛 = 𝑖))
324	323	biimpd 228	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
325	324	anasss 465	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (0..^𝑁) ∧ 𝑖 ∈ (0..^𝑁))) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
326	325	ralrimivva 3191	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
327		oveq1 7424	. . . . 5 ⊢ (𝑛 = 𝑖 → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
328	8, 327	f1mpt 7269	. . . 4 ⊢ (𝐹:(0..^𝑁)–1-1→(Base‘𝐸) ↔ (∀𝑛 ∈ (0..^𝑁)(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸) ∧ ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖)))
329	316, 326, 328	sylanbrc 581	. . 3 ⊢ (𝜑 → 𝐹:(0..^𝑁)–1-1→(Base‘𝐸))
330	294, 302, 303, 305, 306, 307, 308, 289, 311, 315, 239, 329	islbs5 33157	. 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 711	1 ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∀wral 3051 ∃wrex 3060 Vcvv 3463 ∩ cin 3944 ⊆ wss 3945 {csn 4629 class class class wbr 5148 ↦ cmpt 5231 × cxp 5675 ^◡ccnv 5676 dom cdm 5677 ran crn 5678 ↾ cres 5679 “ cima 5680 Fun wfun 6541 Fn wfn 6542 ⟶wf 6543 –1-1→wf1 6544 ‘cfv 6547 (class class class)co 7417 ∘_f cof 7681 supp csupp 8163 ↑_m cmap 8843 Fincfn 8962 finSupp cfsupp 9385 0cc0 11138 -∞cmnf 11276 ℝ^*cxr 11277 < clt 11278 ≤ cle 11279 ℕ₀cn0 12502 ℤcz 12588 [,)cico 13358 ..^cfzo 13659 Basecbs 17179 ↾_s cress 17208 Scalarcsca 17235 ·_𝑠 cvsca 17236 0_gc0g 17420 Σ_g cgsu 17421 Mndcmnd 18693 SubMndcsubmnd 18738 ._gcmg 19027 SubGrpcsubg 19079 CMndccmn 19739 mulGrpcmgp 20078 Ringcrg 20177 NzRingcnzr 20455 DivRingcdr 20628 LModclmod 20747 LSubSpclss 20819 LSpanclspn 20859 LBasisclbs 20963 LVecclvec 20991 var₁cv1 22103 Poly₁cpl1 22104 coe₁cco1 22105 deg₁ cdg1 26017

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5364 ax-pr 5428 ax-un 7739 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216 ax-addf 11217

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3965 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4909 df-int 4950 df-iun 4998 df-iin 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6499 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-isom 6556 df-riota 7373 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7683 df-ofr 7684 df-om 7870 df-1st 7992 df-2nd 7993 df-supp 8164 df-tpos 8230 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-er 8723 df-map 8845 df-pm 8846 df-ixp 8915 df-en 8963 df-dom 8964 df-sdom 8965 df-fin 8966 df-fsupp 9386 df-sup 9465 df-oi 9533 df-card 9962 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11476 df-neg 11477 df-nn 12243 df-2 12305 df-3 12306 df-4 12307 df-5 12308 df-6 12309 df-7 12310 df-8 12311 df-9 12312 df-n0 12503 df-z 12589 df-dec 12708 df-uz 12853 df-ico 13362 df-fz 13517 df-fzo 13660 df-seq 13999 df-hash 14322 df-struct 17115 df-sets 17132 df-slot 17150 df-ndx 17162 df-base 17180 df-ress 17209 df-plusg 17245 df-mulr 17246 df-starv 17247 df-sca 17248 df-vsca 17249 df-ip 17250 df-tset 17251 df-ple 17252 df-ds 17254 df-unif 17255 df-hom 17256 df-cco 17257 df-0g 17422 df-gsum 17423 df-prds 17428 df-pws 17430 df-mre 17565 df-mrc 17566 df-acs 17568 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-mhm 18739 df-submnd 18740 df-grp 18897 df-minusg 18898 df-sbg 18899 df-mulg 19028 df-subg 19082 df-ghm 19172 df-cntz 19272 df-cmn 19741 df-abl 19742 df-mgp 20079 df-rng 20097 df-ur 20126 df-srg 20131 df-ring 20179 df-cring 20180 df-oppr 20277 df-dvdsr 20300 df-unit 20301 df-nzr 20456 df-subrng 20487 df-subrg 20512 df-drng 20630 df-lmod 20749 df-lss 20820 df-lsp 20860 df-lmhm 20911 df-lbs 20964 df-lvec 20992 df-sra 21062 df-rgmod 21063 df-cnfld 21284 df-dsmm 21670 df-frlm 21685 df-uvc 21721 df-lindf 21744 df-linds 21745 df-psr 21846 df-mvr 21847 df-mpl 21848 df-opsr 21850 df-psr1 22107 df-vr1 22108 df-ply1 22109 df-coe1 22110 df-mdeg 26018 df-deg1 26019

This theorem is referenced by: ply1degltdim 33391

W3C validator