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 33816

Description: Lemma for ply1degltdim 33817. (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 2741	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		ply1degltdim.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
4	3	ad3antrrr 737	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑁 ∈ ℕ₀)
5		ply1degltdim.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ DivRing)
6	5	drngringd 20712	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Ring)
7	6	ad3antrrr 737	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑅 ∈ Ring)
8		ply1degltdimlem.f	. . . . . 6 ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
9		eqid 2741	. . . . . 6 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
10		eqid 2741	. . . . . 6 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
11		elmapi 8790	. . . . . . . . 9 ⊢ (𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
12	11	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
13	1	ply1sca 22240	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ DivRing → 𝑅 = (Scalar‘𝑃))
14	5, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
15	14	fveq2d 6834	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
16	15	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
17	16	feq3d 6643	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → (𝑎:(0..^𝑁)⟶(Base‘𝑅) ↔ 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃))))
18	12, 17	mpbird 259	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘𝑅))
19	18	ad2antrr 733	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎:(0..^𝑁)⟶(Base‘𝑅))
20		simpr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸))
21		ovexd 7394	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (0..^𝑁) ∈ V)
22	1, 5	ply1lvec 33652	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ LVec)
23	22	lveclmodd 21100	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ LMod)
24		ply1degltdim.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (deg₁‘𝑅)
25		ply1degltdim.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (^◡𝐷 “ (-∞[,)𝑁))
26	1, 24, 25, 3, 6	ply1degltlss 33689	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃))
27		eqid 2741	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
28	27	lsssubg 20950	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝑆 ∈ (SubGrp‘𝑃))
29	23, 26, 28	syl2anc 591	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑃))
30		subgsubm 19119	. . . . . . . . . 10 ⊢ (𝑆 ∈ (SubGrp‘𝑃) → 𝑆 ∈ (SubMnd‘𝑃))
31	29, 30	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑃))
32	31	ad3antrrr 737	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑆 ∈ (SubMnd‘𝑃))
33		eqid 2741	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑃) = (Base‘𝑃)
34	24, 1, 33	deg1xrf 26067	. . . . . . . . . . . . . 14 ⊢ 𝐷:(Base‘𝑃)⟶ℝ^*
35		ffn 6658	. . . . . . . . . . . . . 14 ⊢ (𝐷:(Base‘𝑃)⟶ℝ^* → 𝐷 Fn (Base‘𝑃))
36	34, 35	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷 Fn (Base‘𝑃))
37		eqid 2741	. . . . . . . . . . . . . 14 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
38		eqid 2741	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝑃)
39		eqid 2741	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
40	23	ad2antrr 733	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑃 ∈ LMod)
41		simplr 775	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘(Scalar‘𝑃)))
42	33, 27	lssss 20929	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (LSubSp‘𝑃) → 𝑆 ⊆ (Base‘𝑃))
43	26, 42	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑃))
44		ply1degltdim.e	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐸 = (𝑃 ↾_s 𝑆)
45	44, 33	ressbas2 17203	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ⊆ (Base‘𝑃) → 𝑆 = (Base‘𝐸))
46	43, 45	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 = (Base‘𝐸))
47	46, 43	eqsstrrd 3951	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐸) ⊆ (Base‘𝑃))
48	47	sselda 3916	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
49	48	adantlr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
50	33, 37, 38, 39, 40, 41, 49	lmodvscld 20872	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ (Base‘𝑃))
51		mnfxr 11198	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
52	51	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ∈ ℝ^*)
53	3	nn0red 12494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℝ)
54	53	rexrd 11191	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
55	54	ad2antrr 733	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑁 ∈ ℝ^*)
56	34	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷:(Base‘𝑃)⟶ℝ^*)
57	56, 50	ffvelcdmd 7029	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ∈ ℝ^*)
58	57	mnfled 13082	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ≤ (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)))
59	56, 49	ffvelcdmd 7029	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) ∈ ℝ^*)
60	6	ad2antrr 733	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑅 ∈ Ring)
61	15	ad2antrr 733	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
62	41, 61	eleqtrrd 2844	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘𝑅))
63	1, 24, 60, 33, 2, 38, 62, 49	deg1vscale 26090	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ≤ (𝐷‘𝑥))
64		simpll 773	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝜑)
65		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝐸))
66	46	ad2antrr 733	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑆 = (Base‘𝐸))
67	65, 66	eleqtrrd 2844	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ 𝑆)
68	51	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -∞ ∈ ℝ^*)
69	54	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℝ^*)
70	34, 35	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐷 Fn (Base‘𝑃))
71		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
72	71, 25	eleqtrdi 2851	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁)))
73		elpreima 7002	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 Fn (Base‘𝑃) → (𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁)) ↔ (𝑥 ∈ (Base‘𝑃) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁))))
74	73	simplbda 501	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 Fn (Base‘𝑃) ∧ 𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁))) → (𝐷‘𝑥) ∈ (-∞[,)𝑁))
75	70, 72, 74	syl2anc 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ (-∞[,)𝑁))
76		elico1 13336	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^) → ((𝐷‘𝑥) ∈ (-∞[,)𝑁) ↔ ((𝐷‘𝑥) ∈ ℝ^ ∧ -∞ ≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁)))
77	76	biimpa 478	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → ((𝐷‘𝑥) ∈ ℝ^ ∧ -∞ ≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁))
78	77	simp3d 1151	. . . . . . . . . . . . . . . . 17 ⊢ (((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → (𝐷‘𝑥) < 𝑁)
79	68, 69, 75, 78	syl21anc 844	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) < 𝑁)
80	64, 67, 79	syl2anc 591	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) < 𝑁)
81	57, 59, 55, 63, 80	xrlelttrd 13106	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) < 𝑁)
82	52, 55, 57, 58, 81	elicod 13343	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ∈ (-∞[,)𝑁))
83	36, 50, 82	elpreimad 7003	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
84	83, 25	eleqtrrdi 2852	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
85	84	anasss 468	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
86	85	ad5ant15 765	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
87	12	ad2antrr 733	. . . . . . . . 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 2741	. . . . . . . . . . . . . . . 16 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
90	89, 33	mgpbas 20120	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
91		eqid 2741	. . . . . . . . . . . . . . 15 ⊢ (._g‘(mulGrp‘𝑃)) = (._g‘(mulGrp‘𝑃))
92	1	ply1ring 22235	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
93	89	ringmgp 20214	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
94	6, 92, 93	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
95	94	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (mulGrp‘𝑃) ∈ Mnd)
96		elfzonn0 13657	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℕ₀)
97	96	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ₀)
98		eqid 2741	. . . . . . . . . . . . . . . . . 18 ⊢ (var₁‘𝑅) = (var₁‘𝑅)
99	98, 1, 33	vr1cl 22205	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → (var₁‘𝑅) ∈ (Base‘𝑃))
100	6, 99	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (var₁‘𝑅) ∈ (Base‘𝑃))
101	100	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (var₁‘𝑅) ∈ (Base‘𝑃))
102	90, 91, 95, 97, 101	mulgnn0cld 19066	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
103	51	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ∈ ℝ^*)
104	54	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑁 ∈ ℝ^*)
105	24, 1, 33	deg1xrcl 26068	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ ℝ^*)
106	102, 105	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ ℝ^*)
107	106	mnfled 13082	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ≤ (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
108	96	nn0red 12494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ)
109	108	rexrd 11191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ^*)
110	109	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℝ^*)
111	24, 1, 98, 89, 91	deg1pwle 26106	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ₀) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ≤ 𝑛)
112	6, 96, 111	syl2an 603	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ≤ 𝑛)
113		elfzolt2 13618	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 < 𝑁)
114	113	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 < 𝑁)
115	106, 110, 104, 112, 114	xrlelttrd 13106	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) < 𝑁)
116	103, 104, 106, 107, 115	elicod 13343	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ (-∞[,)𝑁))
117	88, 102, 116	elpreimad 7003	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
118	117, 25	eleqtrrdi 2852	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝑆)
119	46	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑆 = (Base‘𝐸))
120	118, 119	eleqtrd 2843	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸))
121	120, 8	fmptd 7058	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
122	121	ad3antrrr 737	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
123		inidm 4157	. . . . . . . . 9 ⊢ ((0..^𝑁) ∩ (0..^𝑁)) = (0..^𝑁)
124	86, 87, 122, 21, 21, 123	off 7641	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹):(0..^𝑁)⟶𝑆)
125	21, 32, 124, 44	gsumsubm 18798	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
126		ringmnd 20218	. . . . . . . . . 10 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd)
127	6, 92, 126	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ Mnd)
128	34, 35	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 Fn (Base‘𝑃))
129	33, 10	mndidcl 18712	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Mnd → (0_g‘𝑃) ∈ (Base‘𝑃))
130	127, 129	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (0_g‘𝑃) ∈ (Base‘𝑃))
131	51	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ∈ ℝ^*)
132	24, 1, 33	deg1xrcl 26068	. . . . . . . . . . . . 13 ⊢ ((0_g‘𝑃) ∈ (Base‘𝑃) → (𝐷‘(0_g‘𝑃)) ∈ ℝ^*)
133	130, 132	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) ∈ ℝ^*)
134	133	mnfled 13082	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ≤ (𝐷‘(0_g‘𝑃)))
135	24, 1, 10	deg1z 26073	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (𝐷‘(0_g‘𝑃)) = -∞)
136	6, 135	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) = -∞)
137	53	mnfltd 13070	. . . . . . . . . . . . 13 ⊢ (𝜑 → -∞ < 𝑁)
138	136, 137	eqbrtrd 5096	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) < 𝑁)
139	131, 54, 133, 134, 138	elicod 13343	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) ∈ (-∞[,)𝑁))
140	128, 130, 139	elpreimad 7003	. . . . . . . . . 10 ⊢ (𝜑 → (0_g‘𝑃) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
141	140, 25	eleqtrrdi 2852	. . . . . . . . 9 ⊢ (𝜑 → (0_g‘𝑃) ∈ 𝑆)
142	44, 33, 10	ress0g 18725	. . . . . . . . 9 ⊢ ((𝑃 ∈ Mnd ∧ (0_g‘𝑃) ∈ 𝑆 ∧ 𝑆 ⊆ (Base‘𝑃)) → (0_g‘𝑃) = (0_g‘𝐸))
143	127, 141, 43, 142	syl3anc 1380	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑃) = (0_g‘𝐸))
144	143	ad3antrrr 737	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (0_g‘𝑃) = (0_g‘𝐸))
145	20, 125, 144	3eqtr4d 2786	. . . . . 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 33692	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘𝑅)}))
147	14	fveq2d 6834	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
148	147	sneqd 4569	. . . . . . 7 ⊢ (𝜑 → {(0_g‘𝑅)} = {(0_g‘(Scalar‘𝑃))})
149	148	xpeq2d 5650	. . . . . 6 ⊢ (𝜑 → ((0..^𝑁) × {(0_g‘𝑅)}) = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
150	149	ad3antrrr 737	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → ((0..^𝑁) × {(0_g‘𝑅)}) = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
151	146, 150	eqtrd 2776	. . . 4 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
152	151	expl 459	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → ((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))})))
153	152	ralrimiva 3133	. 2 ⊢ (𝜑 → ∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))})))
154	118, 8	fmptd 7058	. . . . . 6 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶𝑆)
155	154	frnd 6666	. . . . 5 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑆)
156		eqid 2741	. . . . . 6 ⊢ (LSpan‘𝑃) = (LSpan‘𝑃)
157	27, 156	lspssp 20981	. . . . 5 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
158	23, 26, 155, 157	syl3anc 1380	. . . 4 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
159		breq1 5077	. . . . . . . 8 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑎 finSupp (0_g‘(Scalar‘𝑃)) ↔ ((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃))))
160		oveq1 7366	. . . . . . . . . 10 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))
161	160	oveq2d 7375	. . . . . . . . 9 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
162	161	eqeq2d 2752	. . . . . . . 8 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) ↔ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
163	159, 162	anbi12d 639	. . . . . . 7 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → ((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹))) ↔ (((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
164		fvexd 6845	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘(Scalar‘𝑃)) ∈ V)
165		ovexd 7394	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ V)
166	43	sselda 3916	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑃))
167		eqid 2741	. . . . . . . . . . . 12 ⊢ (coe₁‘𝑥) = (coe₁‘𝑥)
168	167, 33, 1, 2	coe1f 22199	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (Base‘𝑃) → (coe₁‘𝑥):ℕ₀⟶(Base‘𝑅))
169	166, 168	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥):ℕ₀⟶(Base‘𝑅))
170	15	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
171	170	feq3d 6643	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥):ℕ₀⟶(Base‘𝑅) ↔ (coe₁‘𝑥):ℕ₀⟶(Base‘(Scalar‘𝑃))))
172	169, 171	mpbid 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥):ℕ₀⟶(Base‘(Scalar‘𝑃)))
173		fzo0ssnn0 13696	. . . . . . . . . 10 ⊢ (0..^𝑁) ⊆ ℕ₀
174	173	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ ℕ₀)
175	172, 174	fssresd 6697	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)):(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
176	164, 165, 175	elmapdd 8782	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)) ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁)))
177	169	ffund 6662	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (coe₁‘𝑥))
178		fzofi 13931	. . . . . . . . . 10 ⊢ (0..^𝑁) ∈ Fin
179	178	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ Fin)
180		fvexd 6845	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0_g‘(Scalar‘𝑃)) ∈ V)
181	177, 179, 180	resfifsupp 9304	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)))
182		ringcmn 20257	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
183	6, 92, 182	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ CMnd)
184	183	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑃 ∈ CMnd)
185		nn0ex 12438	. . . . . . . . . . 11 ⊢ ℕ₀ ∈ V
186	185	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ℕ₀ ∈ V)
187	23	ad2antrr 733	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑃 ∈ LMod)
188	172	ffvelcdmda 7028	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → ((coe₁‘𝑥)‘𝑖) ∈ (Base‘(Scalar‘𝑃)))
189	6	ad2antrr 733	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑅 ∈ Ring)
190	189, 92, 93	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (mulGrp‘𝑃) ∈ Mnd)
191		simpr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℕ₀)
192	189, 99	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (var₁‘𝑅) ∈ (Base‘𝑃))
193	90, 91, 190, 191, 192	mulgnn0cld 19066	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
194	33, 37, 38, 39, 187, 188, 193	lmodvscld 20872	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ (Base‘𝑃))
195		eqid 2741	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) = (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
196	194, 195	fmptd 7058	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))):ℕ₀⟶(Base‘𝑃))
197		nfv 1922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑥 ∈ 𝑆)
198	197, 194, 195	fnmptd 6629	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) Fn ℕ₀)
199		fveq2 6830	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((coe₁‘𝑥)‘𝑖) = ((coe₁‘𝑥)‘𝑗))
200		oveq1 7366	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
201	199, 200	oveq12d 7377	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
202		simplr 775	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℕ₀)
203		ovexd 7394	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ V)
204	195, 201, 202, 203	fvmptd3 6962	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
205	166	ad2antrr 733	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑥 ∈ (Base‘𝑃))
206		icossxr 13380	. . . . . . . . . . . . . . . . 17 ⊢ (-∞[,)𝑁) ⊆ ℝ^*
207	206, 75	sselid 3914	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ ℝ^*)
208	207	ad2antrr 733	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) ∈ ℝ^*)
209	54	ad3antrrr 737	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑁 ∈ ℝ^*)
210	202	nn0red 12494	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ)
211	210	rexrd 11191	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ^*)
212	79	ad2antrr 733	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑁)
213		simpr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑁 ≤ 𝑗)
214	208, 209, 211, 212, 213	xrltletrd 13107	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑗)
215	24, 1, 33, 9, 167	deg1lt 26083	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (Base‘𝑃) ∧ 𝑗 ∈ ℕ₀ ∧ (𝐷‘𝑥) < 𝑗) → ((coe₁‘𝑥)‘𝑗) = (0_g‘𝑅))
216	205, 202, 214, 215	syl3anc 1380	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((coe₁‘𝑥)‘𝑗) = (0_g‘𝑅))
217	216	oveq1d 7374	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
218	147	ad3antrrr 737	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
219	218	oveq1d 7374	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
220	23	ad3antrrr 737	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑃 ∈ LMod)
221	94	ad3antrrr 737	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (mulGrp‘𝑃) ∈ Mnd)
222	100	ad3antrrr 737	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (var₁‘𝑅) ∈ (Base‘𝑃))
223	90, 91, 221, 202, 222	mulgnn0cld 19066	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
224		eqid 2741	. . . . . . . . . . . . . . 15 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
225	33, 37, 38, 224, 10	lmod0vs 20888	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ LMod ∧ (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃)) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
226	220, 223, 225	syl2anc 591	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
227	219, 226	eqtrd 2776	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
228	204, 217, 227	3eqtrd 2780	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (0_g‘𝑃))
229	3	nn0zd 12544	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
230	229	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℤ)
231	198, 228, 230	suppssnn0 32899	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) supp (0_g‘𝑃)) ⊆ (0..^𝑁))
232	186	mptexd 7171	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ∈ V)
233	198	fnfund 6589	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))))
234		fvexd 6845	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0_g‘𝑃) ∈ V)
235		suppssfifsupp 9287	. . . . . . . . . . 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 1387	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) finSupp (0_g‘𝑃))
237	33, 10, 184, 186, 196, 231, 236	gsumres 19882	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σ_g ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁))) = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
238		fvexd 6845	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥) ∈ V)
239		ovexd 7394	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^𝑁) ∈ V)
240	154, 239	fexd 7174	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ V)
241	240	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 ∈ V)
242		offres 7927	. . . . . . . . . . . 12 ⊢ (((coe₁‘𝑥) ∈ V ∧ 𝐹 ∈ V) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))))
243	238, 241, 242	syl2anc 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))))
244	169	ffnd 6659	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥) Fn ℕ₀)
245	154	ffnd 6659	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 Fn (0..^𝑁))
246	245	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 Fn (0..^𝑁))
247		sseqin2 4154	. . . . . . . . . . . . . . . 16 ⊢ ((0..^𝑁) ⊆ ℕ₀ ↔ (ℕ₀ ∩ (0..^𝑁)) = (0..^𝑁))
248	173, 247	mpbi 232	. . . . . . . . . . . . . . 15 ⊢ (ℕ₀ ∩ (0..^𝑁)) = (0..^𝑁)
249		eqidd 2742	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) → ((coe₁‘𝑥)‘𝑗) = ((coe₁‘𝑥)‘𝑗))
250		oveq1 7366	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
251		simpr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
252		ovexd 7394	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ V)
253	8, 250, 251, 252	fvmptd3 6962	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹‘𝑗) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
254	244, 246, 186, 165, 248, 249, 253	ofval 7634	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
255	173, 251	sselid 3914	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ₀)
256		ovexd 7394	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ V)
257	195, 201, 255, 256	fvmptd3 6962	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
258	254, 257	eqtr4d 2779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗))
259	258	ralrimiva 3133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑗 ∈ (0..^𝑁)(((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗))
260	244, 246, 186, 165, 248	offn 7636	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) Fn (0..^𝑁))
261		ssidd 3939	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ (0..^𝑁))
262		fvreseq0 6982	. . . . . . . . . . . . 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 845	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)) ↔ ∀𝑗 ∈ (0..^𝑁)(((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗)))
264	259, 263	mpbird 259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)))
265		fnresdm 6607	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn (0..^𝑁) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
266	245, 265	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) = 𝐹)
267	266	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
268	267	oveq2d 7375	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))
269	243, 264, 268	3eqtr3rd 2785	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)))
270	269	oveq2d 7375	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝑃 Σ_g ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁))))
271	6	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ Ring)
272	1, 98, 33, 38, 89, 91, 167	ply1coe 22287	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
273	271, 166, 272	syl2anc 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
274	237, 270, 273	3eqtr4rd 2787	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
275	181, 274	jca 517	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
276	163, 176, 275	rspcedvdw 3564	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
277	102, 8	fmptd 7058	. . . . . . . 8 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝑃))
278	156, 33, 39, 37, 224, 38, 277, 23, 239	ellspd 21780	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
279	278	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
280	276, 279	mpbird 259	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
281		imadmrn 6028	. . . . . . . 8 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
282	154	fdmd 6668	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = (0..^𝑁))
283	282	imaeq2d 6018	. . . . . . . 8 ⊢ (𝜑 → (𝐹 “ dom 𝐹) = (𝐹 “ (0..^𝑁)))
284	281, 283	eqtr3id 2790	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 = (𝐹 “ (0..^𝑁)))
285	284	fveq2d 6834	. . . . . 6 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
286	285	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
287	280, 286	eleqtrrd 2844	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘ran 𝐹))
288	158, 287	eqelssd 3937	. . 3 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = 𝑆)
289		eqid 2741	. . . . . 6 ⊢ (LSpan‘𝐸) = (LSpan‘𝐸)
290	44, 156, 289, 27	lsslsp 21008	. . . . 5 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝐸)‘ran 𝐹) = ((LSpan‘𝑃)‘ran 𝐹))
291	290	eqcomd 2747	. . . 4 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
292	23, 26, 155, 291	syl3anc 1380	. . 3 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
293	288, 292, 46	3eqtr3d 2784	. 2 ⊢ (𝜑 → ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸))
294		eqid 2741	. . 3 ⊢ (Base‘𝐸) = (Base‘𝐸)
295	24	fvexi 6844	. . . . . . 7 ⊢ 𝐷 ∈ V
296		cnvexg 7868	. . . . . . 7 ⊢ (𝐷 ∈ V → ^◡𝐷 ∈ V)
297		imaexg 7857	. . . . . . 7 ⊢ (^◡𝐷 ∈ V → (^◡𝐷 “ (-∞[,)𝑁)) ∈ V)
298	295, 296, 297	mp2b 10	. . . . . 6 ⊢ (^◡𝐷 “ (-∞[,)𝑁)) ∈ V
299	25, 298	eqeltri 2837	. . . . 5 ⊢ 𝑆 ∈ V
300	44, 37	resssca 17301	. . . . 5 ⊢ (𝑆 ∈ V → (Scalar‘𝑃) = (Scalar‘𝐸))
301	299, 300	ax-mp 5	. . . 4 ⊢ (Scalar‘𝑃) = (Scalar‘𝐸)
302	301	fveq2i 6833	. . 3 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝐸))
303		eqid 2741	. . 3 ⊢ (Scalar‘𝐸) = (Scalar‘𝐸)
304	44, 38	ressvsca 17302	. . . 4 ⊢ (𝑆 ∈ V → ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝐸))
305	299, 304	ax-mp 5	. . 3 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝐸)
306		eqid 2741	. . 3 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
307	301	fveq2i 6833	. . 3 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝐸))
308		eqid 2741	. . 3 ⊢ (LBasis‘𝐸) = (LBasis‘𝐸)
309	44, 27	lsslvec 21102	. . . . 5 ⊢ ((𝑃 ∈ LVec ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝐸 ∈ LVec)
310	22, 26, 309	syl2anc 591	. . . 4 ⊢ (𝜑 → 𝐸 ∈ LVec)
311	310	lveclmodd 21100	. . 3 ⊢ (𝜑 → 𝐸 ∈ LMod)
312	14, 5	eqeltrrd 2842	. . . . 5 ⊢ (𝜑 → (Scalar‘𝑃) ∈ DivRing)
313		drngnzr 20723	. . . . 5 ⊢ ((Scalar‘𝑃) ∈ DivRing → (Scalar‘𝑃) ∈ NzRing)
314	312, 313	syl 17	. . . 4 ⊢ (𝜑 → (Scalar‘𝑃) ∈ NzRing)
315	301, 314	eqeltrrid 2846	. . 3 ⊢ (𝜑 → (Scalar‘𝐸) ∈ NzRing)
316	120	ralrimiva 3133	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸))
317		drngnzr 20723	. . . . . . . . . 10 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
318	5, 317	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ NzRing)
319	318	ad2antrr 733	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑅 ∈ NzRing)
320	97	adantr 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ₀)
321		elfzonn0 13657	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℕ₀)
322	321	adantl 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ ℕ₀)
323	1, 98, 91, 319, 320, 322	ply1moneq 33681	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ↔ 𝑛 = 𝑖))
324	323	biimpd 231	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
325	324	anasss 468	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (0..^𝑁) ∧ 𝑖 ∈ (0..^𝑁))) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
326	325	ralrimivva 3184	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
327		oveq1 7366	. . . . 5 ⊢ (𝑛 = 𝑖 → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
328	8, 327	f1mpt 7208	. . . 4 ⊢ (𝐹:(0..^𝑁)–1-1→(Base‘𝐸) ↔ (∀𝑛 ∈ (0..^𝑁)(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸) ∧ ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖)))
329	316, 326, 328	sylanbrc 590	. . 3 ⊢ (𝜑 → 𝐹:(0..^𝑁)–1-1→(Base‘𝐸))
330	294, 302, 303, 305, 306, 307, 308, 289, 311, 315, 239, 329	islbs5 33465	. 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 720	1 ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 397 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ∀wral 3055 ∃wrex 3065 Vcvv 3433 ∩ cin 3883 ⊆ wss 3884 {csn 4557 class class class wbr 5074 ↦ cmpt 5155 × cxp 5618 ^◡ccnv 5619 dom cdm 5620 ran crn 5621 ↾ cres 5622 “ cima 5623 Fun wfun 6482 Fn wfn 6483 ⟶wf 6484 –1-1→wf1 6485 ‘cfv 6488 (class class class)co 7359 ∘_f cof 7621 supp csupp 8102 ↑_m cmap 8767 Fincfn 8887 finSupp cfsupp 9268 0cc0 11034 -∞cmnf 11173 ℝ^*cxr 11174 < clt 11175 ≤ cle 11176 ℕ₀cn0 12432 ℤcz 12519 [,)cico 13295 ..^cfzo 13603 Basecbs 17174 ↾_s cress 17195 Scalarcsca 17218 ·_𝑠 cvsca 17219 0_gc0g 17397 Σ_g cgsu 17398 Mndcmnd 18697 SubMndcsubmnd 18745 ._gcmg 19038 SubGrpcsubg 19091 CMndccmn 19749 mulGrpcmgp 20115 Ringcrg 20208 NzRingcnzr 20487 DivRingcdr 20704 LModclmod 20853 LSubSpclss 20924 LSpanclspn 20964 LBasisclbs 21067 LVecclvec 21095 var₁cv1 22164 Poly₁cpl1 22165 coe₁cco1 22166 deg₁cdg1 26040

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5201 ax-sep 5220 ax-nul 5230 ax-pow 5296 ax-pr 5364 ax-un 7681 ax-cnex 11090 ax-resscn 11091 ax-1cn 11092 ax-icn 11093 ax-addcl 11094 ax-addrcl 11095 ax-mulcl 11096 ax-mulrcl 11097 ax-mulcom 11098 ax-addass 11099 ax-mulass 11100 ax-distr 11101 ax-i2m1 11102 ax-1ne0 11103 ax-1rid 11104 ax-rnegex 11105 ax-rrecex 11106 ax-cnre 11107 ax-pre-lttri 11108 ax-pre-lttrn 11109 ax-pre-ltadd 11110 ax-pre-mulgt0 11111 ax-pre-sup 11112 ax-addf 11113

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3725 df-csb 3833 df-dif 3887 df-un 3889 df-in 3891 df-ss 3901 df-pss 3904 df-nul 4264 df-if 4457 df-pw 4533 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4841 df-int 4880 df-iun 4925 df-iin 4926 df-br 5075 df-opab 5137 df-mpt 5156 df-tr 5182 df-id 5515 df-eprel 5520 df-po 5528 df-so 5529 df-fr 5573 df-se 5574 df-we 5575 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-isom 6497 df-riota 7316 df-ov 7362 df-oprab 7363 df-mpo 7364 df-of 7623 df-ofr 7624 df-om 7810 df-1st 7933 df-2nd 7934 df-supp 8103 df-tpos 8168 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8343 df-1o 8399 df-2o 8400 df-er 8637 df-map 8769 df-pm 8770 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-sup 9349 df-oi 9419 df-card 9858 df-pnf 11177 df-mnf 11178 df-xr 11179 df-ltxr 11180 df-le 11181 df-sub 11375 df-neg 11376 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 df-7 12244 df-8 12245 df-9 12246 df-n0 12433 df-z 12520 df-dec 12640 df-uz 12784 df-ico 13299 df-fz 13457 df-fzo 13604 df-seq 13959 df-hash 14288 df-struct 17112 df-sets 17129 df-slot 17147 df-ndx 17159 df-base 17175 df-ress 17196 df-plusg 17228 df-mulr 17229 df-starv 17230 df-sca 17231 df-vsca 17232 df-ip 17233 df-tset 17234 df-ple 17235 df-ds 17237 df-unif 17238 df-hom 17239 df-cco 17240 df-0g 17399 df-gsum 17400 df-prds 17405 df-pws 17407 df-mre 17543 df-mrc 17544 df-acs 17546 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-mhm 18746 df-submnd 18747 df-grp 18907 df-minusg 18908 df-sbg 18909 df-mulg 19039 df-subg 19094 df-ghm 19183 df-cntz 19286 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-srg 20162 df-ring 20210 df-cring 20211 df-oppr 20311 df-dvdsr 20331 df-unit 20332 df-nzr 20488 df-subrng 20521 df-subrg 20545 df-drng 20706 df-lmod 20855 df-lss 20925 df-lsp 20965 df-lmhm 21015 df-lbs 21068 df-lvec 21096 df-sra 21166 df-rgmod 21167 df-cnfld 21351 df-dsmm 21710 df-frlm 21725 df-uvc 21761 df-lindf 21784 df-linds 21785 df-psr 21887 df-mvr 21888 df-mpl 21889 df-opsr 21891 df-psr1 22168 df-vr1 22169 df-ply1 22170 df-coe1 22171 df-mdeg 26041 df-deg1 26042

This theorem is referenced by: ply1degltdim 33817

W3C validator