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 33618

Description: Lemma for ply1degltdim 33619. (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 2729	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		ply1degltdim.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
4	3	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑁 ∈ ℕ₀)
5		ply1degltdim.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ DivRing)
6	5	drngringd 20646	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Ring)
7	6	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑅 ∈ Ring)
8		ply1degltdimlem.f	. . . . . 6 ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
9		eqid 2729	. . . . . 6 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
10		eqid 2729	. . . . . 6 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
11		elmapi 8822	. . . . . . . . 9 ⊢ (𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
12	11	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
13	1	ply1sca 22137	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ DivRing → 𝑅 = (Scalar‘𝑃))
14	5, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
15	14	fveq2d 6862	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
16	15	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
17	16	feq3d 6673	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → (𝑎:(0..^𝑁)⟶(Base‘𝑅) ↔ 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃))))
18	12, 17	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘𝑅))
19	18	ad2antrr 726	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎:(0..^𝑁)⟶(Base‘𝑅))
20		simpr 484	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸))
21		ovexd 7422	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (0..^𝑁) ∈ V)
22	1, 5	ply1lvec 33528	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ LVec)
23	22	lveclmodd 21014	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ LMod)
24		ply1degltdim.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (deg₁‘𝑅)
25		ply1degltdim.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (^◡𝐷 “ (-∞[,)𝑁))
26	1, 24, 25, 3, 6	ply1degltlss 33562	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃))
27		eqid 2729	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
28	27	lsssubg 20863	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝑆 ∈ (SubGrp‘𝑃))
29	23, 26, 28	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑃))
30		subgsubm 19080	. . . . . . . . . 10 ⊢ (𝑆 ∈ (SubGrp‘𝑃) → 𝑆 ∈ (SubMnd‘𝑃))
31	29, 30	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑃))
32	31	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑆 ∈ (SubMnd‘𝑃))
33		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑃) = (Base‘𝑃)
34	24, 1, 33	deg1xrf 25986	. . . . . . . . . . . . . 14 ⊢ 𝐷:(Base‘𝑃)⟶ℝ^*
35		ffn 6688	. . . . . . . . . . . . . 14 ⊢ (𝐷:(Base‘𝑃)⟶ℝ^* → 𝐷 Fn (Base‘𝑃))
36	34, 35	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷 Fn (Base‘𝑃))
37		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
38		eqid 2729	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝑃)
39		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
40	23	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑃 ∈ LMod)
41		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘(Scalar‘𝑃)))
42	33, 27	lssss 20842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (LSubSp‘𝑃) → 𝑆 ⊆ (Base‘𝑃))
43	26, 42	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑃))
44		ply1degltdim.e	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐸 = (𝑃 ↾_s 𝑆)
45	44, 33	ressbas2 17208	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ⊆ (Base‘𝑃) → 𝑆 = (Base‘𝐸))
46	43, 45	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 = (Base‘𝐸))
47	46, 43	eqsstrrd 3982	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐸) ⊆ (Base‘𝑃))
48	47	sselda 3946	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
49	48	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
50	33, 37, 38, 39, 40, 41, 49	lmodvscld 20785	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ (Base‘𝑃))
51		mnfxr 11231	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
52	51	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ∈ ℝ^*)
53	3	nn0red 12504	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℝ)
54	53	rexrd 11224	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
55	54	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑁 ∈ ℝ^*)
56	34	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷:(Base‘𝑃)⟶ℝ^*)
57	56, 50	ffvelcdmd 7057	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ∈ ℝ^*)
58	57	mnfled 13096	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ≤ (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)))
59	56, 49	ffvelcdmd 7057	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) ∈ ℝ^*)
60	6	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑅 ∈ Ring)
61	15	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
62	41, 61	eleqtrrd 2831	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘𝑅))
63	1, 24, 60, 33, 2, 38, 62, 49	deg1vscale 26009	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ≤ (𝐷‘𝑥))
64		simpll 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝜑)
65		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝐸))
66	46	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑆 = (Base‘𝐸))
67	65, 66	eleqtrrd 2831	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ 𝑆)
68	51	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → -∞ ∈ ℝ^*)
69	54	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℝ^*)
70	34, 35	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐷 Fn (Base‘𝑃))
71		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆)
72	71, 25	eleqtrdi 2838	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁)))
73		elpreima 7030	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 Fn (Base‘𝑃) → (𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁)) ↔ (𝑥 ∈ (Base‘𝑃) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁))))
74	73	simplbda 499	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 Fn (Base‘𝑃) ∧ 𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁))) → (𝐷‘𝑥) ∈ (-∞[,)𝑁))
75	70, 72, 74	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ (-∞[,)𝑁))
76		elico1 13349	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^) → ((𝐷‘𝑥) ∈ (-∞[,)𝑁) ↔ ((𝐷‘𝑥) ∈ ℝ^ ∧ -∞ ≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁)))
77	76	biimpa 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → ((𝐷‘𝑥) ∈ ℝ^ ∧ -∞ ≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁))
78	77	simp3d 1144	. . . . . . . . . . . . . . . . 17 ⊢ (((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → (𝐷‘𝑥) < 𝑁)
79	68, 69, 75, 78	syl21anc 837	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) < 𝑁)
80	64, 67, 79	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) < 𝑁)
81	57, 59, 55, 63, 80	xrlelttrd 13120	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) < 𝑁)
82	52, 55, 57, 58, 81	elicod 13356	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ∈ (-∞[,)𝑁))
83	36, 50, 82	elpreimad 7031	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
84	83, 25	eleqtrrdi 2839	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
85	84	anasss 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
86	85	ad5ant15 758	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
87	12	ad2antrr 726	. . . . . . . . 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 2729	. . . . . . . . . . . . . . . 16 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
90	89, 33	mgpbas 20054	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
91		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (._g‘(mulGrp‘𝑃)) = (._g‘(mulGrp‘𝑃))
92	1	ply1ring 22132	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
93	89	ringmgp 20148	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
94	6, 92, 93	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
95	94	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (mulGrp‘𝑃) ∈ Mnd)
96		elfzonn0 13668	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℕ₀)
97	96	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ₀)
98		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (var₁‘𝑅) = (var₁‘𝑅)
99	98, 1, 33	vr1cl 22102	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → (var₁‘𝑅) ∈ (Base‘𝑃))
100	6, 99	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (var₁‘𝑅) ∈ (Base‘𝑃))
101	100	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (var₁‘𝑅) ∈ (Base‘𝑃))
102	90, 91, 95, 97, 101	mulgnn0cld 19027	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
103	51	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ∈ ℝ^*)
104	54	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑁 ∈ ℝ^*)
105	24, 1, 33	deg1xrcl 25987	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ ℝ^*)
106	102, 105	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ ℝ^*)
107	106	mnfled 13096	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ≤ (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
108	96	nn0red 12504	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ)
109	108	rexrd 11224	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ^*)
110	109	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℝ^*)
111	24, 1, 98, 89, 91	deg1pwle 26025	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ₀) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ≤ 𝑛)
112	6, 96, 111	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ≤ 𝑛)
113		elfzolt2 13629	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 < 𝑁)
114	113	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 < 𝑁)
115	106, 110, 104, 112, 114	xrlelttrd 13120	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) < 𝑁)
116	103, 104, 106, 107, 115	elicod 13356	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ (-∞[,)𝑁))
117	88, 102, 116	elpreimad 7031	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
118	117, 25	eleqtrrdi 2839	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝑆)
119	46	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑆 = (Base‘𝐸))
120	118, 119	eleqtrd 2830	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸))
121	120, 8	fmptd 7086	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
122	121	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
123		inidm 4190	. . . . . . . . 9 ⊢ ((0..^𝑁) ∩ (0..^𝑁)) = (0..^𝑁)
124	86, 87, 122, 21, 21, 123	off 7671	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹):(0..^𝑁)⟶𝑆)
125	21, 32, 124, 44	gsumsubm 18762	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
126		ringmnd 20152	. . . . . . . . . 10 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd)
127	6, 92, 126	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ Mnd)
128	34, 35	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 Fn (Base‘𝑃))
129	33, 10	mndidcl 18676	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Mnd → (0_g‘𝑃) ∈ (Base‘𝑃))
130	127, 129	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (0_g‘𝑃) ∈ (Base‘𝑃))
131	51	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ∈ ℝ^*)
132	24, 1, 33	deg1xrcl 25987	. . . . . . . . . . . . 13 ⊢ ((0_g‘𝑃) ∈ (Base‘𝑃) → (𝐷‘(0_g‘𝑃)) ∈ ℝ^*)
133	130, 132	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) ∈ ℝ^*)
134	133	mnfled 13096	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ≤ (𝐷‘(0_g‘𝑃)))
135	24, 1, 10	deg1z 25992	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (𝐷‘(0_g‘𝑃)) = -∞)
136	6, 135	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) = -∞)
137	53	mnfltd 13084	. . . . . . . . . . . . 13 ⊢ (𝜑 → -∞ < 𝑁)
138	136, 137	eqbrtrd 5129	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) < 𝑁)
139	131, 54, 133, 134, 138	elicod 13356	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) ∈ (-∞[,)𝑁))
140	128, 130, 139	elpreimad 7031	. . . . . . . . . 10 ⊢ (𝜑 → (0_g‘𝑃) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
141	140, 25	eleqtrrdi 2839	. . . . . . . . 9 ⊢ (𝜑 → (0_g‘𝑃) ∈ 𝑆)
142	44, 33, 10	ress0g 18689	. . . . . . . . 9 ⊢ ((𝑃 ∈ Mnd ∧ (0_g‘𝑃) ∈ 𝑆 ∧ 𝑆 ⊆ (Base‘𝑃)) → (0_g‘𝑃) = (0_g‘𝐸))
143	127, 141, 43, 142	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑃) = (0_g‘𝐸))
144	143	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (0_g‘𝑃) = (0_g‘𝐸))
145	20, 125, 144	3eqtr4d 2774	. . . . . 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 33564	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘𝑅)}))
147	14	fveq2d 6862	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
148	147	sneqd 4601	. . . . . . 7 ⊢ (𝜑 → {(0_g‘𝑅)} = {(0_g‘(Scalar‘𝑃))})
149	148	xpeq2d 5668	. . . . . 6 ⊢ (𝜑 → ((0..^𝑁) × {(0_g‘𝑅)}) = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
150	149	ad3antrrr 730	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → ((0..^𝑁) × {(0_g‘𝑅)}) = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
151	146, 150	eqtrd 2764	. . . 4 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
152	151	expl 457	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → ((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))})))
153	152	ralrimiva 3125	. 2 ⊢ (𝜑 → ∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))})))
154	118, 8	fmptd 7086	. . . . . 6 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶𝑆)
155	154	frnd 6696	. . . . 5 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑆)
156		eqid 2729	. . . . . 6 ⊢ (LSpan‘𝑃) = (LSpan‘𝑃)
157	27, 156	lspssp 20894	. . . . 5 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
158	23, 26, 155, 157	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
159		breq1 5110	. . . . . . . 8 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑎 finSupp (0_g‘(Scalar‘𝑃)) ↔ ((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃))))
160		oveq1 7394	. . . . . . . . . 10 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))
161	160	oveq2d 7403	. . . . . . . . 9 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
162	161	eqeq2d 2740	. . . . . . . 8 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) ↔ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
163	159, 162	anbi12d 632	. . . . . . 7 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → ((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹))) ↔ (((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
164		fvexd 6873	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘(Scalar‘𝑃)) ∈ V)
165		ovexd 7422	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ V)
166	43	sselda 3946	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑃))
167		eqid 2729	. . . . . . . . . . . 12 ⊢ (coe₁‘𝑥) = (coe₁‘𝑥)
168	167, 33, 1, 2	coe1f 22096	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (Base‘𝑃) → (coe₁‘𝑥):ℕ₀⟶(Base‘𝑅))
169	166, 168	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥):ℕ₀⟶(Base‘𝑅))
170	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
171	170	feq3d 6673	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥):ℕ₀⟶(Base‘𝑅) ↔ (coe₁‘𝑥):ℕ₀⟶(Base‘(Scalar‘𝑃))))
172	169, 171	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥):ℕ₀⟶(Base‘(Scalar‘𝑃)))
173		fzo0ssnn0 13707	. . . . . . . . . 10 ⊢ (0..^𝑁) ⊆ ℕ₀
174	173	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ ℕ₀)
175	172, 174	fssresd 6727	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)):(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
176	164, 165, 175	elmapdd 8814	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)) ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁)))
177	169	ffund 6692	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (coe₁‘𝑥))
178		fzofi 13939	. . . . . . . . . 10 ⊢ (0..^𝑁) ∈ Fin
179	178	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ Fin)
180		fvexd 6873	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0_g‘(Scalar‘𝑃)) ∈ V)
181	177, 179, 180	resfifsupp 9348	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)))
182		ringcmn 20191	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
183	6, 92, 182	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ CMnd)
184	183	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑃 ∈ CMnd)
185		nn0ex 12448	. . . . . . . . . . 11 ⊢ ℕ₀ ∈ V
186	185	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ℕ₀ ∈ V)
187	23	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑃 ∈ LMod)
188	172	ffvelcdmda 7056	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → ((coe₁‘𝑥)‘𝑖) ∈ (Base‘(Scalar‘𝑃)))
189	6	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑅 ∈ Ring)
190	189, 92, 93	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (mulGrp‘𝑃) ∈ Mnd)
191		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℕ₀)
192	189, 99	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (var₁‘𝑅) ∈ (Base‘𝑃))
193	90, 91, 190, 191, 192	mulgnn0cld 19027	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
194	33, 37, 38, 39, 187, 188, 193	lmodvscld 20785	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ (Base‘𝑃))
195		eqid 2729	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) = (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
196	194, 195	fmptd 7086	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))):ℕ₀⟶(Base‘𝑃))
197		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑥 ∈ 𝑆)
198	197, 194, 195	fnmptd 6659	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) Fn ℕ₀)
199		fveq2 6858	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((coe₁‘𝑥)‘𝑖) = ((coe₁‘𝑥)‘𝑗))
200		oveq1 7394	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
201	199, 200	oveq12d 7405	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
202		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℕ₀)
203		ovexd 7422	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ V)
204	195, 201, 202, 203	fvmptd3 6991	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
205	166	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑥 ∈ (Base‘𝑃))
206		icossxr 13393	. . . . . . . . . . . . . . . . 17 ⊢ (-∞[,)𝑁) ⊆ ℝ^*
207	206, 75	sselid 3944	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ ℝ^*)
208	207	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) ∈ ℝ^*)
209	54	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑁 ∈ ℝ^*)
210	202	nn0red 12504	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ)
211	210	rexrd 11224	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ^*)
212	79	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑁)
213		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑁 ≤ 𝑗)
214	208, 209, 211, 212, 213	xrltletrd 13121	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑗)
215	24, 1, 33, 9, 167	deg1lt 26002	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (Base‘𝑃) ∧ 𝑗 ∈ ℕ₀ ∧ (𝐷‘𝑥) < 𝑗) → ((coe₁‘𝑥)‘𝑗) = (0_g‘𝑅))
216	205, 202, 214, 215	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((coe₁‘𝑥)‘𝑗) = (0_g‘𝑅))
217	216	oveq1d 7402	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
218	147	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
219	218	oveq1d 7402	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
220	23	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑃 ∈ LMod)
221	94	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (mulGrp‘𝑃) ∈ Mnd)
222	100	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (var₁‘𝑅) ∈ (Base‘𝑃))
223	90, 91, 221, 202, 222	mulgnn0cld 19027	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
224		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
225	33, 37, 38, 224, 10	lmod0vs 20801	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ LMod ∧ (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃)) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
226	220, 223, 225	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
227	219, 226	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
228	204, 217, 227	3eqtrd 2768	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (0_g‘𝑃))
229	3	nn0zd 12555	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
230	229	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℤ)
231	198, 228, 230	suppssnn0 32730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) supp (0_g‘𝑃)) ⊆ (0..^𝑁))
232	186	mptexd 7198	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ∈ V)
233	198	fnfund 6619	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))))
234		fvexd 6873	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0_g‘𝑃) ∈ V)
235		suppssfifsupp 9331	. . . . . . . . . . 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 1380	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) finSupp (0_g‘𝑃))
237	33, 10, 184, 186, 196, 231, 236	gsumres 19843	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σ_g ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁))) = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
238		fvexd 6873	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥) ∈ V)
239		ovexd 7422	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^𝑁) ∈ V)
240	154, 239	fexd 7201	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ V)
241	240	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 ∈ V)
242		offres 7962	. . . . . . . . . . . 12 ⊢ (((coe₁‘𝑥) ∈ V ∧ 𝐹 ∈ V) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))))
243	238, 241, 242	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))))
244	169	ffnd 6689	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥) Fn ℕ₀)
245	154	ffnd 6689	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 Fn (0..^𝑁))
246	245	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 Fn (0..^𝑁))
247		sseqin2 4186	. . . . . . . . . . . . . . . 16 ⊢ ((0..^𝑁) ⊆ ℕ₀ ↔ (ℕ₀ ∩ (0..^𝑁)) = (0..^𝑁))
248	173, 247	mpbi 230	. . . . . . . . . . . . . . 15 ⊢ (ℕ₀ ∩ (0..^𝑁)) = (0..^𝑁)
249		eqidd 2730	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) → ((coe₁‘𝑥)‘𝑗) = ((coe₁‘𝑥)‘𝑗))
250		oveq1 7394	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
251		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
252		ovexd 7422	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ V)
253	8, 250, 251, 252	fvmptd3 6991	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹‘𝑗) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
254	244, 246, 186, 165, 248, 249, 253	ofval 7664	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
255	173, 251	sselid 3944	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ₀)
256		ovexd 7422	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ V)
257	195, 201, 255, 256	fvmptd3 6991	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
258	254, 257	eqtr4d 2767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗))
259	258	ralrimiva 3125	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑗 ∈ (0..^𝑁)(((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗))
260	244, 246, 186, 165, 248	offn 7666	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) Fn (0..^𝑁))
261		ssidd 3970	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ (0..^𝑁))
262		fvreseq0 7010	. . . . . . . . . . . . 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 838	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)) ↔ ∀𝑗 ∈ (0..^𝑁)(((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗)))
264	259, 263	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)))
265		fnresdm 6637	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn (0..^𝑁) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
266	245, 265	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) = 𝐹)
267	266	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
268	267	oveq2d 7403	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))
269	243, 264, 268	3eqtr3rd 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)))
270	269	oveq2d 7403	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝑃 Σ_g ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁))))
271	6	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ Ring)
272	1, 98, 33, 38, 89, 91, 167	ply1coe 22185	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
273	271, 166, 272	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
274	237, 270, 273	3eqtr4rd 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
275	181, 274	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
276	163, 176, 275	rspcedvdw 3591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
277	102, 8	fmptd 7086	. . . . . . . 8 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝑃))
278	156, 33, 39, 37, 224, 38, 277, 23, 239	ellspd 21711	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
279	278	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
280	276, 279	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
281		imadmrn 6041	. . . . . . . 8 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
282	154	fdmd 6698	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = (0..^𝑁))
283	282	imaeq2d 6031	. . . . . . . 8 ⊢ (𝜑 → (𝐹 “ dom 𝐹) = (𝐹 “ (0..^𝑁)))
284	281, 283	eqtr3id 2778	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 = (𝐹 “ (0..^𝑁)))
285	284	fveq2d 6862	. . . . . 6 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
286	285	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
287	280, 286	eleqtrrd 2831	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘ran 𝐹))
288	158, 287	eqelssd 3968	. . 3 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = 𝑆)
289		eqid 2729	. . . . . 6 ⊢ (LSpan‘𝐸) = (LSpan‘𝐸)
290	44, 156, 289, 27	lsslsp 20921	. . . . 5 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝐸)‘ran 𝐹) = ((LSpan‘𝑃)‘ran 𝐹))
291	290	eqcomd 2735	. . . 4 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
292	23, 26, 155, 291	syl3anc 1373	. . 3 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
293	288, 292, 46	3eqtr3d 2772	. 2 ⊢ (𝜑 → ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸))
294		eqid 2729	. . 3 ⊢ (Base‘𝐸) = (Base‘𝐸)
295	24	fvexi 6872	. . . . . . 7 ⊢ 𝐷 ∈ V
296		cnvexg 7900	. . . . . . 7 ⊢ (𝐷 ∈ V → ^◡𝐷 ∈ V)
297		imaexg 7889	. . . . . . 7 ⊢ (^◡𝐷 ∈ V → (^◡𝐷 “ (-∞[,)𝑁)) ∈ V)
298	295, 296, 297	mp2b 10	. . . . . 6 ⊢ (^◡𝐷 “ (-∞[,)𝑁)) ∈ V
299	25, 298	eqeltri 2824	. . . . 5 ⊢ 𝑆 ∈ V
300	44, 37	resssca 17306	. . . . 5 ⊢ (𝑆 ∈ V → (Scalar‘𝑃) = (Scalar‘𝐸))
301	299, 300	ax-mp 5	. . . 4 ⊢ (Scalar‘𝑃) = (Scalar‘𝐸)
302	301	fveq2i 6861	. . 3 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝐸))
303		eqid 2729	. . 3 ⊢ (Scalar‘𝐸) = (Scalar‘𝐸)
304	44, 38	ressvsca 17307	. . . 4 ⊢ (𝑆 ∈ V → ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝐸))
305	299, 304	ax-mp 5	. . 3 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝐸)
306		eqid 2729	. . 3 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
307	301	fveq2i 6861	. . 3 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝐸))
308		eqid 2729	. . 3 ⊢ (LBasis‘𝐸) = (LBasis‘𝐸)
309	44, 27	lsslvec 21016	. . . . 5 ⊢ ((𝑃 ∈ LVec ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝐸 ∈ LVec)
310	22, 26, 309	syl2anc 584	. . . 4 ⊢ (𝜑 → 𝐸 ∈ LVec)
311	310	lveclmodd 21014	. . 3 ⊢ (𝜑 → 𝐸 ∈ LMod)
312	14, 5	eqeltrrd 2829	. . . . 5 ⊢ (𝜑 → (Scalar‘𝑃) ∈ DivRing)
313		drngnzr 20657	. . . . 5 ⊢ ((Scalar‘𝑃) ∈ DivRing → (Scalar‘𝑃) ∈ NzRing)
314	312, 313	syl 17	. . . 4 ⊢ (𝜑 → (Scalar‘𝑃) ∈ NzRing)
315	301, 314	eqeltrrid 2833	. . 3 ⊢ (𝜑 → (Scalar‘𝐸) ∈ NzRing)
316	120	ralrimiva 3125	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸))
317		drngnzr 20657	. . . . . . . . . 10 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
318	5, 317	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ NzRing)
319	318	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑅 ∈ NzRing)
320	97	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ₀)
321		elfzonn0 13668	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℕ₀)
322	321	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ ℕ₀)
323	1, 98, 91, 319, 320, 322	ply1moneq 33555	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ↔ 𝑛 = 𝑖))
324	323	biimpd 229	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
325	324	anasss 466	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ (0..^𝑁) ∧ 𝑖 ∈ (0..^𝑁))) → ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
326	325	ralrimivva 3180	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
327		oveq1 7394	. . . . 5 ⊢ (𝑛 = 𝑖 → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
328	8, 327	f1mpt 7236	. . . 4 ⊢ (𝐹:(0..^𝑁)–1-1→(Base‘𝐸) ↔ (∀𝑛 ∈ (0..^𝑁)(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸) ∧ ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖)))
329	316, 326, 328	sylanbrc 583	. . 3 ⊢ (𝜑 → 𝐹:(0..^𝑁)–1-1→(Base‘𝐸))
330	294, 302, 303, 305, 306, 307, 308, 289, 311, 315, 239, 329	islbs5 33351	. 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 713	1 ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 Vcvv 3447 ∩ cin 3913 ⊆ wss 3914 {csn 4589 class class class wbr 5107 ↦ cmpt 5188 × cxp 5636 ^◡ccnv 5637 dom cdm 5638 ran crn 5639 ↾ cres 5640 “ cima 5641 Fun wfun 6505 Fn wfn 6506 ⟶wf 6507 –1-1→wf1 6508 ‘cfv 6511 (class class class)co 7387 ∘_f cof 7651 supp csupp 8139 ↑_m cmap 8799 Fincfn 8918 finSupp cfsupp 9312 0cc0 11068 -∞cmnf 11206 ℝ^*cxr 11207 < clt 11208 ≤ cle 11209 ℕ₀cn0 12442 ℤcz 12529 [,)cico 13308 ..^cfzo 13615 Basecbs 17179 ↾_s cress 17200 Scalarcsca 17223 ·_𝑠 cvsca 17224 0_gc0g 17402 Σ_g cgsu 17403 Mndcmnd 18661 SubMndcsubmnd 18709 ._gcmg 18999 SubGrpcsubg 19052 CMndccmn 19710 mulGrpcmgp 20049 Ringcrg 20142 NzRingcnzr 20421 DivRingcdr 20638 LModclmod 20766 LSubSpclss 20837 LSpanclspn 20877 LBasisclbs 20981 LVecclvec 21009 var₁cv1 22060 Poly₁cpl1 22061 coe₁cco1 22062 deg₁cdg1 25959

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146 ax-addf 11147

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-of 7653 df-ofr 7654 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-tpos 8205 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-er 8671 df-map 8801 df-pm 8802 df-ixp 8871 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fsupp 9313 df-sup 9393 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-ico 13312 df-fz 13469 df-fzo 13616 df-seq 13967 df-hash 14296 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-0g 17404 df-gsum 17405 df-prds 17410 df-pws 17412 df-mre 17547 df-mrc 17548 df-acs 17550 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-mhm 18710 df-submnd 18711 df-grp 18868 df-minusg 18869 df-sbg 18870 df-mulg 19000 df-subg 19055 df-ghm 19145 df-cntz 19249 df-cmn 19712 df-abl 19713 df-mgp 20050 df-rng 20062 df-ur 20091 df-srg 20096 df-ring 20144 df-cring 20145 df-oppr 20246 df-dvdsr 20266 df-unit 20267 df-nzr 20422 df-subrng 20455 df-subrg 20479 df-drng 20640 df-lmod 20768 df-lss 20838 df-lsp 20878 df-lmhm 20929 df-lbs 20982 df-lvec 21010 df-sra 21080 df-rgmod 21081 df-cnfld 21265 df-dsmm 21641 df-frlm 21656 df-uvc 21692 df-lindf 21715 df-linds 21716 df-psr 21818 df-mvr 21819 df-mpl 21820 df-opsr 21822 df-psr1 22064 df-vr1 22065 df-ply1 22066 df-coe1 22067 df-mdeg 25960 df-deg1 25961

This theorem is referenced by: ply1degltdim 33619

W3C validator