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 33788

Description: Lemma for ply1degltdim 33789. (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 2737	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		ply1degltdim.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
4	3	ad3antrrr 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑁 ∈ ℕ₀)
5		ply1degltdim.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ DivRing)
6	5	drngringd 20711	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Ring)
7	6	ad3antrrr 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑅 ∈ Ring)
8		ply1degltdimlem.f	. . . . . 6 ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
9		eqid 2737	. . . . . 6 ⊢ (0_g‘𝑅) = (0_g‘𝑅)
10		eqid 2737	. . . . . 6 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
11		elmapi 8793	. . . . . . . . 9 ⊢ (𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
12	11	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
13	1	ply1sca 22232	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ DivRing → 𝑅 = (Scalar‘𝑃))
14	5, 13	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
15	14	fveq2d 6842	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
16	15	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
17	16	feq3d 6651	. . . . . . . 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 727	. . . . . 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 7399	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (0..^𝑁) ∈ V)
22	1, 5	ply1lvec 33640	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ LVec)
23	22	lveclmodd 21100	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ LMod)
24		ply1degltdim.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (deg₁‘𝑅)
25		ply1degltdim.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (^◡𝐷 “ (-∞[,)𝑁))
26	1, 24, 25, 3, 6	ply1degltlss 33677	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃))
27		eqid 2737	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑃) = (LSubSp‘𝑃)
28	27	lsssubg 20949	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝑆 ∈ (SubGrp‘𝑃))
29	23, 26, 28	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑃))
30		subgsubm 19121	. . . . . . . . . 10 ⊢ (𝑆 ∈ (SubGrp‘𝑃) → 𝑆 ∈ (SubMnd‘𝑃))
31	29, 30	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑃))
32	31	ad3antrrr 731	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑆 ∈ (SubMnd‘𝑃))
33		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑃) = (Base‘𝑃)
34	24, 1, 33	deg1xrf 26062	. . . . . . . . . . . . . 14 ⊢ 𝐷:(Base‘𝑃)⟶ℝ^*
35		ffn 6666	. . . . . . . . . . . . . 14 ⊢ (𝐷:(Base‘𝑃)⟶ℝ^* → 𝐷 Fn (Base‘𝑃))
36	34, 35	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷 Fn (Base‘𝑃))
37		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
38		eqid 2737	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝑃)
39		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
40	23	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑃 ∈ LMod)
41		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘(Scalar‘𝑃)))
42	33, 27	lssss 20928	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑆 ∈ (LSubSp‘𝑃) → 𝑆 ⊆ (Base‘𝑃))
43	26, 42	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑃))
44		ply1degltdim.e	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐸 = (𝑃 ↾_s 𝑆)
45	44, 33	ressbas2 17205	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑆 ⊆ (Base‘𝑃) → 𝑆 = (Base‘𝐸))
46	43, 45	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 = (Base‘𝐸))
47	46, 43	eqsstrrd 3958	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (Base‘𝐸) ⊆ (Base‘𝑃))
48	47	sselda 3922	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
49	48	adantlr 716	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃))
50	33, 37, 38, 39, 40, 41, 49	lmodvscld 20871	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ (Base‘𝑃))
51		mnfxr 11199	. . . . . . . . . . . . . . 15 ⊢ -∞ ∈ ℝ^*
52	51	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ∈ ℝ^*)
53	3	nn0red 12496	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℝ)
54	53	rexrd 11192	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℝ^*)
55	54	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑁 ∈ ℝ^*)
56	34	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷:(Base‘𝑃)⟶ℝ^*)
57	56, 50	ffvelcdmd 7035	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ∈ ℝ^*)
58	57	mnfled 13084	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ≤ (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)))
59	56, 49	ffvelcdmd 7035	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) ∈ ℝ^*)
60	6	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑅 ∈ Ring)
61	15	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
62	41, 61	eleqtrrd 2840	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘𝑅))
63	1, 24, 60, 33, 2, 38, 62, 49	deg1vscale 26085	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ≤ (𝐷‘𝑥))
64		simpll 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝜑)
65		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝐸))
66	46	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑆 = (Base‘𝐸))
67	65, 66	eleqtrrd 2840	. . . . . . . . . . . . . . . 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 2847	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁)))
73		elpreima 7008	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 Fn (Base‘𝑃) → (𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁)) ↔ (𝑥 ∈ (Base‘𝑃) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁))))
74	73	simplbda 499	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 Fn (Base‘𝑃) ∧ 𝑥 ∈ (^◡𝐷 “ (-∞[,)𝑁))) → (𝐷‘𝑥) ∈ (-∞[,)𝑁))
75	70, 72, 74	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ (-∞[,)𝑁))
76		elico1 13338	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^) → ((𝐷‘𝑥) ∈ (-∞[,)𝑁) ↔ ((𝐷‘𝑥) ∈ ℝ^ ∧ -∞ ≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁)))
77	76	biimpa 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → ((𝐷‘𝑥) ∈ ℝ^ ∧ -∞ ≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁))
78	77	simp3d 1145	. . . . . . . . . . . . . . . . 17 ⊢ (((-∞ ∈ ℝ^* ∧ 𝑁 ∈ ℝ^*) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → (𝐷‘𝑥) < 𝑁)
79	68, 69, 75, 78	syl21anc 838	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) < 𝑁)
80	64, 67, 79	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) < 𝑁)
81	57, 59, 55, 63, 80	xrlelttrd 13108	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) < 𝑁)
82	52, 55, 57, 58, 81	elicod 13345	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·_𝑠 ‘𝑃)𝑥)) ∈ (-∞[,)𝑁))
83	36, 50, 82	elpreimad 7009	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
84	83, 25	eleqtrrdi 2848	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
85	84	anasss 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
86	85	ad5ant15 759	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·_𝑠 ‘𝑃)𝑥) ∈ 𝑆)
87	12	ad2antrr 727	. . . . . . . . 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 2737	. . . . . . . . . . . . . . . 16 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
90	89, 33	mgpbas 20123	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
91		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (._g‘(mulGrp‘𝑃)) = (._g‘(mulGrp‘𝑃))
92	1	ply1ring 22227	. . . . . . . . . . . . . . . . 17 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
93	89	ringmgp 20217	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
94	6, 92, 93	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
95	94	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (mulGrp‘𝑃) ∈ Mnd)
96		elfzonn0 13659	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℕ₀)
97	96	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ₀)
98		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (var₁‘𝑅) = (var₁‘𝑅)
99	98, 1, 33	vr1cl 22197	. . . . . . . . . . . . . . . . 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 19068	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
103	51	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ∈ ℝ^*)
104	54	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑁 ∈ ℝ^*)
105	24, 1, 33	deg1xrcl 26063	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ ℝ^*)
106	102, 105	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ ℝ^*)
107	106	mnfled 13084	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ≤ (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
108	96	nn0red 12496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ)
109	108	rexrd 11192	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ^*)
110	109	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℝ^*)
111	24, 1, 98, 89, 91	deg1pwle 26101	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ₀) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ≤ 𝑛)
112	6, 96, 111	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ≤ 𝑛)
113		elfzolt2 13620	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 < 𝑁)
114	113	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 < 𝑁)
115	106, 110, 104, 112, 114	xrlelttrd 13108	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) < 𝑁)
116	103, 104, 106, 107, 115	elicod 13345	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ (-∞[,)𝑁))
117	88, 102, 116	elpreimad 7009	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
118	117, 25	eleqtrrdi 2848	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ 𝑆)
119	46	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑆 = (Base‘𝐸))
120	118, 119	eleqtrd 2839	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸))
121	120, 8	fmptd 7064	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
122	121	ad3antrrr 731	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝐹:(0..^𝑁)⟶(Base‘𝐸))
123		inidm 4168	. . . . . . . . 9 ⊢ ((0..^𝑁) ∩ (0..^𝑁)) = (0..^𝑁)
124	86, 87, 122, 21, 21, 123	off 7646	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹):(0..^𝑁)⟶𝑆)
125	21, 32, 124, 44	gsumsubm 18800	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
126		ringmnd 20221	. . . . . . . . . 10 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd)
127	6, 92, 126	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ Mnd)
128	34, 35	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 Fn (Base‘𝑃))
129	33, 10	mndidcl 18714	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Mnd → (0_g‘𝑃) ∈ (Base‘𝑃))
130	127, 129	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (0_g‘𝑃) ∈ (Base‘𝑃))
131	51	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ∈ ℝ^*)
132	24, 1, 33	deg1xrcl 26063	. . . . . . . . . . . . 13 ⊢ ((0_g‘𝑃) ∈ (Base‘𝑃) → (𝐷‘(0_g‘𝑃)) ∈ ℝ^*)
133	130, 132	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) ∈ ℝ^*)
134	133	mnfled 13084	. . . . . . . . . . . 12 ⊢ (𝜑 → -∞ ≤ (𝐷‘(0_g‘𝑃)))
135	24, 1, 10	deg1z 26068	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → (𝐷‘(0_g‘𝑃)) = -∞)
136	6, 135	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) = -∞)
137	53	mnfltd 13072	. . . . . . . . . . . . 13 ⊢ (𝜑 → -∞ < 𝑁)
138	136, 137	eqbrtrd 5108	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) < 𝑁)
139	131, 54, 133, 134, 138	elicod 13345	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷‘(0_g‘𝑃)) ∈ (-∞[,)𝑁))
140	128, 130, 139	elpreimad 7009	. . . . . . . . . 10 ⊢ (𝜑 → (0_g‘𝑃) ∈ (^◡𝐷 “ (-∞[,)𝑁)))
141	140, 25	eleqtrrdi 2848	. . . . . . . . 9 ⊢ (𝜑 → (0_g‘𝑃) ∈ 𝑆)
142	44, 33, 10	ress0g 18727	. . . . . . . . 9 ⊢ ((𝑃 ∈ Mnd ∧ (0_g‘𝑃) ∈ 𝑆 ∧ 𝑆 ⊆ (Base‘𝑃)) → (0_g‘𝑃) = (0_g‘𝐸))
143	127, 141, 43, 142	syl3anc 1374	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑃) = (0_g‘𝐸))
144	143	ad3antrrr 731	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → (0_g‘𝑃) = (0_g‘𝐸))
145	20, 125, 144	3eqtr4d 2782	. . . . . 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 33680	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘𝑅)}))
147	14	fveq2d 6842	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
148	147	sneqd 4580	. . . . . . 7 ⊢ (𝜑 → {(0_g‘𝑅)} = {(0_g‘(Scalar‘𝑃))})
149	148	xpeq2d 5658	. . . . . 6 ⊢ (𝜑 → ((0..^𝑁) × {(0_g‘𝑅)}) = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
150	149	ad3antrrr 731	. . . . 5 ⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))) ∧ 𝑎 finSupp (0_g‘(Scalar‘𝑃))) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → ((0..^𝑁) × {(0_g‘𝑅)}) = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))}))
151	146, 150	eqtrd 2772	. . . 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 3130	. 2 ⊢ (𝜑 → ∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ (𝐸 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (0_g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0_g‘(Scalar‘𝑃))})))
154	118, 8	fmptd 7064	. . . . . 6 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶𝑆)
155	154	frnd 6674	. . . . 5 ⊢ (𝜑 → ran 𝐹 ⊆ 𝑆)
156		eqid 2737	. . . . . 6 ⊢ (LSpan‘𝑃) = (LSpan‘𝑃)
157	27, 156	lspssp 20980	. . . . 5 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
158	23, 26, 155, 157	syl3anc 1374	. . . 4 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆)
159		breq1 5089	. . . . . . . 8 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑎 finSupp (0_g‘(Scalar‘𝑃)) ↔ ((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃))))
160		oveq1 7371	. . . . . . . . . 10 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))
161	160	oveq2d 7380	. . . . . . . . 9 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))
162	161	eqeq2d 2748	. . . . . . . 8 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → (𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹)) ↔ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
163	159, 162	anbi12d 633	. . . . . . 7 ⊢ (𝑎 = ((coe₁‘𝑥) ↾ (0..^𝑁)) → ((𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹))) ↔ (((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹)))))
164		fvexd 6853	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘(Scalar‘𝑃)) ∈ V)
165		ovexd 7399	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ V)
166	43	sselda 3922	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑃))
167		eqid 2737	. . . . . . . . . . . 12 ⊢ (coe₁‘𝑥) = (coe₁‘𝑥)
168	167, 33, 1, 2	coe1f 22191	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (Base‘𝑃) → (coe₁‘𝑥):ℕ₀⟶(Base‘𝑅))
169	166, 168	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥):ℕ₀⟶(Base‘𝑅))
170	15	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
171	170	feq3d 6651	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥):ℕ₀⟶(Base‘𝑅) ↔ (coe₁‘𝑥):ℕ₀⟶(Base‘(Scalar‘𝑃))))
172	169, 171	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥):ℕ₀⟶(Base‘(Scalar‘𝑃)))
173		fzo0ssnn0 13698	. . . . . . . . . 10 ⊢ (0..^𝑁) ⊆ ℕ₀
174	173	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ ℕ₀)
175	172, 174	fssresd 6705	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)):(0..^𝑁)⟶(Base‘(Scalar‘𝑃)))
176	164, 165, 175	elmapdd 8785	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)) ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁)))
177	169	ffund 6670	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (coe₁‘𝑥))
178		fzofi 13933	. . . . . . . . . 10 ⊢ (0..^𝑁) ∈ Fin
179	178	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ Fin)
180		fvexd 6853	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0_g‘(Scalar‘𝑃)) ∈ V)
181	177, 179, 180	resfifsupp 9307	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ↾ (0..^𝑁)) finSupp (0_g‘(Scalar‘𝑃)))
182		ringcmn 20260	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
183	6, 92, 182	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ CMnd)
184	183	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑃 ∈ CMnd)
185		nn0ex 12440	. . . . . . . . . . 11 ⊢ ℕ₀ ∈ V
186	185	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ℕ₀ ∈ V)
187	23	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → 𝑃 ∈ LMod)
188	172	ffvelcdmda 7034	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → ((coe₁‘𝑥)‘𝑖) ∈ (Base‘(Scalar‘𝑃)))
189	6	ad2antrr 727	. . . . . . . . . . . . . 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 19068	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
194	33, 37, 38, 39, 187, 188, 193	lmodvscld 20871	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ₀) → (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ (Base‘𝑃))
195		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) = (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
196	194, 195	fmptd 7064	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))):ℕ₀⟶(Base‘𝑃))
197		nfv 1916	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑥 ∈ 𝑆)
198	197, 194, 195	fnmptd 6637	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) Fn ℕ₀)
199		fveq2 6838	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → ((coe₁‘𝑥)‘𝑖) = ((coe₁‘𝑥)‘𝑗))
200		oveq1 7371	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑗 → (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
201	199, 200	oveq12d 7382	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑗 → (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
202		simplr 769	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℕ₀)
203		ovexd 7399	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ V)
204	195, 201, 202, 203	fvmptd3 6969	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
205	166	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑥 ∈ (Base‘𝑃))
206		icossxr 13382	. . . . . . . . . . . . . . . . 17 ⊢ (-∞[,)𝑁) ⊆ ℝ^*
207	206, 75	sselid 3920	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ ℝ^*)
208	207	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) ∈ ℝ^*)
209	54	ad3antrrr 731	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑁 ∈ ℝ^*)
210	202	nn0red 12496	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ)
211	210	rexrd 11192	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ^*)
212	79	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑁)
213		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑁 ≤ 𝑗)
214	208, 209, 211, 212, 213	xrltletrd 13109	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑗)
215	24, 1, 33, 9, 167	deg1lt 26078	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (Base‘𝑃) ∧ 𝑗 ∈ ℕ₀ ∧ (𝐷‘𝑥) < 𝑗) → ((coe₁‘𝑥)‘𝑗) = (0_g‘𝑅))
216	205, 202, 214, 215	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((coe₁‘𝑥)‘𝑗) = (0_g‘𝑅))
217	216	oveq1d 7379	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
218	147	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
219	218	oveq1d 7379	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
220	23	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → 𝑃 ∈ LMod)
221	94	ad3antrrr 731	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (mulGrp‘𝑃) ∈ Mnd)
222	100	ad3antrrr 731	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (var₁‘𝑅) ∈ (Base‘𝑃))
223	90, 91, 221, 202, 222	mulgnn0cld 19068	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃))
224		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
225	33, 37, 38, 224, 10	lmod0vs 20887	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ LMod ∧ (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝑃)) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
226	220, 223, 225	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘(Scalar‘𝑃))( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
227	219, 226	eqtrd 2772	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((0_g‘𝑅)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) = (0_g‘𝑃))
228	204, 217, 227	3eqtrd 2776	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (0_g‘𝑃))
229	3	nn0zd 12546	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℤ)
230	229	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℤ)
231	198, 228, 230	suppssnn0 32899	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) supp (0_g‘𝑃)) ⊆ (0..^𝑁))
232	186	mptexd 7176	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ∈ V)
233	198	fnfund 6597	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))))
234		fvexd 6853	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0_g‘𝑃) ∈ V)
235		suppssfifsupp 9290	. . . . . . . . . . 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 1381	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) finSupp (0_g‘𝑃))
237	33, 10, 184, 186, 196, 231, 236	gsumres 19885	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σ_g ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁))) = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
238		fvexd 6853	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥) ∈ V)
239		ovexd 7399	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^𝑁) ∈ V)
240	154, 239	fexd 7179	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ V)
241	240	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 ∈ V)
242		offres 7933	. . . . . . . . . . . 12 ⊢ (((coe₁‘𝑥) ∈ V ∧ 𝐹 ∈ V) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))))
243	238, 241, 242	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))))
244	169	ffnd 6667	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe₁‘𝑥) Fn ℕ₀)
245	154	ffnd 6667	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 Fn (0..^𝑁))
246	245	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 Fn (0..^𝑁))
247		sseqin2 4164	. . . . . . . . . . . . . . . 16 ⊢ ((0..^𝑁) ⊆ ℕ₀ ↔ (ℕ₀ ∩ (0..^𝑁)) = (0..^𝑁))
248	173, 247	mpbi 230	. . . . . . . . . . . . . . 15 ⊢ (ℕ₀ ∩ (0..^𝑁)) = (0..^𝑁)
249		eqidd 2738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ₀) → ((coe₁‘𝑥)‘𝑗) = ((coe₁‘𝑥)‘𝑗))
250		oveq1 7371	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
251		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
252		ovexd 7399	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ V)
253	8, 250, 251, 252	fvmptd3 6969	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹‘𝑗) = (𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
254	244, 246, 186, 165, 248, 249, 253	ofval 7639	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
255	173, 251	sselid 3920	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ₀)
256		ovexd 7399	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))) ∈ V)
257	195, 201, 255, 256	fvmptd3 6969	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗) = (((coe₁‘𝑥)‘𝑗)( ·_𝑠 ‘𝑃)(𝑗(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))
258	254, 257	eqtr4d 2775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗))
259	258	ralrimiva 3130	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑗 ∈ (0..^𝑁)(((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))‘𝑗))
260	244, 246, 186, 165, 248	offn 7641	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe₁‘𝑥) ∘_f ( ·_𝑠 ‘𝑃)𝐹) Fn (0..^𝑁))
261		ssidd 3946	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ (0..^𝑁))
262		fvreseq0 6988	. . . . . . . . . . . . 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 839	. . . . . . . . . . . 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 6615	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn (0..^𝑁) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
266	245, 265	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) = 𝐹)
267	266	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐹 ↾ (0..^𝑁)) = 𝐹)
268	267	oveq2d 7380	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))) = (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹))
269	243, 264, 268	3eqtr3rd 2781	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe₁‘𝑥) ↾ (0..^𝑁)) ∘_f ( ·_𝑠 ‘𝑃)𝐹) = ((𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))) ↾ (0..^𝑁)))
270	269	oveq2d 7380	. . . . . . . . 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 22279	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
273	271, 166, 272	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σ_g (𝑖 ∈ ℕ₀ ↦ (((coe₁‘𝑥)‘𝑖)( ·_𝑠 ‘𝑃)(𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅))))))
274	237, 270, 273	3eqtr4rd 2783	. . . . . . . 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 3568	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑_m (0..^𝑁))(𝑎 finSupp (0_g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σ_g (𝑎 ∘_f ( ·_𝑠 ‘𝑃)𝐹))))
277	102, 8	fmptd 7064	. . . . . . . 8 ⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝑃))
278	156, 33, 39, 37, 224, 38, 277, 23, 239	ellspd 21798	. . . . . . 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 6033	. . . . . . . 8 ⊢ (𝐹 “ dom 𝐹) = ran 𝐹
282	154	fdmd 6676	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = (0..^𝑁))
283	282	imaeq2d 6023	. . . . . . . 8 ⊢ (𝜑 → (𝐹 “ dom 𝐹) = (𝐹 “ (0..^𝑁)))
284	281, 283	eqtr3id 2786	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 = (𝐹 “ (0..^𝑁)))
285	284	fveq2d 6842	. . . . . 6 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
286	285	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))))
287	280, 286	eleqtrrd 2840	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘ran 𝐹))
288	158, 287	eqelssd 3944	. . 3 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = 𝑆)
289		eqid 2737	. . . . . 6 ⊢ (LSpan‘𝐸) = (LSpan‘𝐸)
290	44, 156, 289, 27	lsslsp 21007	. . . . 5 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝐸)‘ran 𝐹) = ((LSpan‘𝑃)‘ran 𝐹))
291	290	eqcomd 2743	. . . 4 ⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
292	23, 26, 155, 291	syl3anc 1374	. . 3 ⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹))
293	288, 292, 46	3eqtr3d 2780	. 2 ⊢ (𝜑 → ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸))
294		eqid 2737	. . 3 ⊢ (Base‘𝐸) = (Base‘𝐸)
295	24	fvexi 6852	. . . . . . 7 ⊢ 𝐷 ∈ V
296		cnvexg 7872	. . . . . . 7 ⊢ (𝐷 ∈ V → ^◡𝐷 ∈ V)
297		imaexg 7861	. . . . . . 7 ⊢ (^◡𝐷 ∈ V → (^◡𝐷 “ (-∞[,)𝑁)) ∈ V)
298	295, 296, 297	mp2b 10	. . . . . 6 ⊢ (^◡𝐷 “ (-∞[,)𝑁)) ∈ V
299	25, 298	eqeltri 2833	. . . . 5 ⊢ 𝑆 ∈ V
300	44, 37	resssca 17303	. . . . 5 ⊢ (𝑆 ∈ V → (Scalar‘𝑃) = (Scalar‘𝐸))
301	299, 300	ax-mp 5	. . . 4 ⊢ (Scalar‘𝑃) = (Scalar‘𝐸)
302	301	fveq2i 6841	. . 3 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝐸))
303		eqid 2737	. . 3 ⊢ (Scalar‘𝐸) = (Scalar‘𝐸)
304	44, 38	ressvsca 17304	. . . 4 ⊢ (𝑆 ∈ V → ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝐸))
305	299, 304	ax-mp 5	. . 3 ⊢ ( ·_𝑠 ‘𝑃) = ( ·_𝑠 ‘𝐸)
306		eqid 2737	. . 3 ⊢ (0_g‘𝐸) = (0_g‘𝐸)
307	301	fveq2i 6841	. . 3 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝐸))
308		eqid 2737	. . 3 ⊢ (LBasis‘𝐸) = (LBasis‘𝐸)
309	44, 27	lsslvec 21102	. . . . 5 ⊢ ((𝑃 ∈ LVec ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝐸 ∈ LVec)
310	22, 26, 309	syl2anc 585	. . . 4 ⊢ (𝜑 → 𝐸 ∈ LVec)
311	310	lveclmodd 21100	. . 3 ⊢ (𝜑 → 𝐸 ∈ LMod)
312	14, 5	eqeltrrd 2838	. . . . 5 ⊢ (𝜑 → (Scalar‘𝑃) ∈ DivRing)
313		drngnzr 20722	. . . . 5 ⊢ ((Scalar‘𝑃) ∈ DivRing → (Scalar‘𝑃) ∈ NzRing)
314	312, 313	syl 17	. . . 4 ⊢ (𝜑 → (Scalar‘𝑃) ∈ NzRing)
315	301, 314	eqeltrrid 2842	. . 3 ⊢ (𝜑 → (Scalar‘𝐸) ∈ NzRing)
316	120	ralrimiva 3130	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸))
317		drngnzr 20722	. . . . . . . . . 10 ⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing)
318	5, 317	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ NzRing)
319	318	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑅 ∈ NzRing)
320	97	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ₀)
321		elfzonn0 13659	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℕ₀)
322	321	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ ℕ₀)
323	1, 98, 91, 319, 320, 322	ply1moneq 33669	. . . . . . 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 3181	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖))
327		oveq1 7371	. . . . 5 ⊢ (𝑛 = 𝑖 → (𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)))
328	8, 327	f1mpt 7213	. . . 4 ⊢ (𝐹:(0..^𝑁)–1-1→(Base‘𝐸) ↔ (∀𝑛 ∈ (0..^𝑁)(𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) ∈ (Base‘𝐸) ∧ ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) = (𝑖(._g‘(mulGrp‘𝑃))(var₁‘𝑅)) → 𝑛 = 𝑖)))
329	316, 326, 328	sylanbrc 584	. . 3 ⊢ (𝜑 → 𝐹:(0..^𝑁)–1-1→(Base‘𝐸))
330	294, 302, 303, 305, 306, 307, 308, 289, 311, 315, 239, 329	islbs5 33461	. 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 714	1 ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 Vcvv 3430 ∩ cin 3889 ⊆ wss 3890 {csn 4568 class class class wbr 5086 ↦ cmpt 5167 × cxp 5626 ^◡ccnv 5627 dom cdm 5628 ran crn 5629 ↾ cres 5630 “ cima 5631 Fun wfun 6490 Fn wfn 6491 ⟶wf 6492 –1-1→wf1 6493 ‘cfv 6496 (class class class)co 7364 ∘_f cof 7626 supp csupp 8107 ↑_m cmap 8770 Fincfn 8890 finSupp cfsupp 9271 0cc0 11035 -∞cmnf 11174 ℝ^*cxr 11175 < clt 11176 ≤ cle 11177 ℕ₀cn0 12434 ℤcz 12521 [,)cico 13297 ..^cfzo 13605 Basecbs 17176 ↾_s cress 17197 Scalarcsca 17220 ·_𝑠 cvsca 17221 0_gc0g 17399 Σ_g cgsu 17400 Mndcmnd 18699 SubMndcsubmnd 18747 ._gcmg 19040 SubGrpcsubg 19093 CMndccmn 19752 mulGrpcmgp 20118 Ringcrg 20211 NzRingcnzr 20486 DivRingcdr 20703 LModclmod 20852 LSubSpclss 20923 LSpanclspn 20963 LBasisclbs 21067 LVecclvec 21095 var₁cv1 22155 Poly₁cpl1 22156 coe₁cco1 22157 deg₁cdg1 26035

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5306 ax-pr 5374 ax-un 7686 ax-cnex 11091 ax-resscn 11092 ax-1cn 11093 ax-icn 11094 ax-addcl 11095 ax-addrcl 11096 ax-mulcl 11097 ax-mulrcl 11098 ax-mulcom 11099 ax-addass 11100 ax-mulass 11101 ax-distr 11102 ax-i2m1 11103 ax-1ne0 11104 ax-1rid 11105 ax-rnegex 11106 ax-rrecex 11107 ax-cnre 11108 ax-pre-lttri 11109 ax-pre-lttrn 11110 ax-pre-ltadd 11111 ax-pre-mulgt0 11112 ax-pre-sup 11113 ax-addf 11114

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5523 df-eprel 5528 df-po 5536 df-so 5537 df-fr 5581 df-se 5582 df-we 5583 df-xp 5634 df-rel 5635 df-cnv 5636 df-co 5637 df-dm 5638 df-rn 5639 df-res 5640 df-ima 5641 df-pred 6263 df-ord 6324 df-on 6325 df-lim 6326 df-suc 6327 df-iota 6452 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7321 df-ov 7367 df-oprab 7368 df-mpo 7369 df-of 7628 df-ofr 7629 df-om 7815 df-1st 7939 df-2nd 7940 df-supp 8108 df-tpos 8173 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-2o 8403 df-er 8640 df-map 8772 df-pm 8773 df-ixp 8843 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-fsupp 9272 df-sup 9352 df-oi 9422 df-card 9860 df-pnf 11178 df-mnf 11179 df-xr 11180 df-ltxr 11181 df-le 11182 df-sub 11376 df-neg 11377 df-nn 12172 df-2 12241 df-3 12242 df-4 12243 df-5 12244 df-6 12245 df-7 12246 df-8 12247 df-9 12248 df-n0 12435 df-z 12522 df-dec 12642 df-uz 12786 df-ico 13301 df-fz 13459 df-fzo 13606 df-seq 13961 df-hash 14290 df-struct 17114 df-sets 17131 df-slot 17149 df-ndx 17161 df-base 17177 df-ress 17198 df-plusg 17230 df-mulr 17231 df-starv 17232 df-sca 17233 df-vsca 17234 df-ip 17235 df-tset 17236 df-ple 17237 df-ds 17239 df-unif 17240 df-hom 17241 df-cco 17242 df-0g 17401 df-gsum 17402 df-prds 17407 df-pws 17409 df-mre 17545 df-mrc 17546 df-acs 17548 df-mgm 18605 df-sgrp 18684 df-mnd 18700 df-mhm 18748 df-submnd 18749 df-grp 18909 df-minusg 18910 df-sbg 18911 df-mulg 19041 df-subg 19096 df-ghm 19185 df-cntz 19289 df-cmn 19754 df-abl 19755 df-mgp 20119 df-rng 20131 df-ur 20160 df-srg 20165 df-ring 20213 df-cring 20214 df-oppr 20314 df-dvdsr 20334 df-unit 20335 df-nzr 20487 df-subrng 20520 df-subrg 20544 df-drng 20705 df-lmod 20854 df-lss 20924 df-lsp 20964 df-lmhm 21015 df-lbs 21068 df-lvec 21096 df-sra 21166 df-rgmod 21167 df-cnfld 21351 df-dsmm 21728 df-frlm 21743 df-uvc 21779 df-lindf 21802 df-linds 21803 df-psr 21905 df-mvr 21906 df-mpl 21907 df-opsr 21909 df-psr1 22159 df-vr1 22160 df-ply1 22161 df-coe1 22162 df-mdeg 26036 df-deg1 26037

This theorem is referenced by: ply1degltdim 33789

W3C validator