Step | Hyp | Ref
| Expression |
1 | | ply1degltdim.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | eqid 2727 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
3 | | ply1degltdim.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
4 | 3 | ad3antrrr 729 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑁 ∈
ℕ0) |
5 | | ply1degltdim.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ DivRing) |
6 | 5 | drngringd 20621 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
7 | 6 | ad3antrrr 729 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑅 ∈ Ring) |
8 | | ply1degltdimlem.f |
. . . . . 6
⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
9 | | eqid 2727 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
10 | | eqid 2727 |
. . . . . 6
⊢
(0g‘𝑃) = (0g‘𝑃) |
11 | | elmapi 8859 |
. . . . . . . . 9
⊢ (𝑎 ∈
((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃))) |
12 | 11 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃))) |
13 | 1 | ply1sca 22158 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ DivRing → 𝑅 = (Scalar‘𝑃)) |
14 | 5, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) |
15 | 14 | fveq2d 6895 |
. . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
16 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) → (Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
17 | 16 | feq3d 6703 |
. . . . . . . 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 725 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑎:(0..^𝑁)⟶(Base‘𝑅)) |
20 | | simpr 484 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) |
21 | | ovexd 7449 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → (0..^𝑁) ∈ V) |
22 | 1, 5 | ply1lvec 33170 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ LVec) |
23 | 22 | lveclmodd 20981 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ LMod) |
24 | | ply1degltdim.d |
. . . . . . . . . . . 12
⊢ 𝐷 = ( deg1
‘𝑅) |
25 | | ply1degltdim.s |
. . . . . . . . . . . 12
⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁)) |
26 | 1, 24, 25, 3, 6 | ply1degltlss 33199 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃)) |
27 | | eqid 2727 |
. . . . . . . . . . . 12
⊢
(LSubSp‘𝑃) =
(LSubSp‘𝑃) |
28 | 27 | lsssubg 20830 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝑆 ∈ (SubGrp‘𝑃)) |
29 | 23, 26, 28 | syl2anc 583 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑃)) |
30 | | subgsubm 19094 |
. . . . . . . . . 10
⊢ (𝑆 ∈ (SubGrp‘𝑃) → 𝑆 ∈ (SubMnd‘𝑃)) |
31 | 29, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑃)) |
32 | 31 | ad3antrrr 729 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑆 ∈ (SubMnd‘𝑃)) |
33 | | eqid 2727 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑃) =
(Base‘𝑃) |
34 | 24, 1, 33 | deg1xrf 26004 |
. . . . . . . . . . . . . 14
⊢ 𝐷:(Base‘𝑃)⟶ℝ* |
35 | | ffn 6716 |
. . . . . . . . . . . . . 14
⊢ (𝐷:(Base‘𝑃)⟶ℝ* → 𝐷 Fn (Base‘𝑃)) |
36 | 34, 35 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷 Fn (Base‘𝑃)) |
37 | | eqid 2727 |
. . . . . . . . . . . . . 14
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
38 | | eqid 2727 |
. . . . . . . . . . . . . 14
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
39 | | eqid 2727 |
. . . . . . . . . . . . . 14
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
40 | 23 | ad2antrr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑃 ∈ LMod) |
41 | | simplr 768 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘(Scalar‘𝑃))) |
42 | 33, 27 | lssss 20809 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈ (LSubSp‘𝑃) → 𝑆 ⊆ (Base‘𝑃)) |
43 | 26, 42 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑃)) |
44 | | ply1degltdim.e |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐸 = (𝑃 ↾s 𝑆) |
45 | 44, 33 | ressbas2 17209 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ⊆ (Base‘𝑃) → 𝑆 = (Base‘𝐸)) |
46 | 43, 45 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 = (Base‘𝐸)) |
47 | 46, 43 | eqsstrrd 4017 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Base‘𝐸) ⊆ (Base‘𝑃)) |
48 | 47 | sselda 3978 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃)) |
49 | 48 | adantlr 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃)) |
50 | 33, 37, 38, 39, 40, 41, 49 | lmodvscld 20751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·𝑠
‘𝑃)𝑥) ∈ (Base‘𝑃)) |
51 | | mnfxr 11293 |
. . . . . . . . . . . . . . 15
⊢ -∞
∈ ℝ* |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ∈
ℝ*) |
53 | 3 | nn0red 12555 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℝ) |
54 | 53 | rexrd 11286 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
55 | 54 | ad2antrr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑁 ∈
ℝ*) |
56 | 34 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷:(Base‘𝑃)⟶ℝ*) |
57 | 56, 50 | ffvelcdmd 7089 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠
‘𝑃)𝑥)) ∈
ℝ*) |
58 | 57 | mnfled 13139 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ≤ (𝐷‘(𝑘( ·𝑠
‘𝑃)𝑥))) |
59 | 56, 49 | ffvelcdmd 7089 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) ∈
ℝ*) |
60 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑅 ∈ Ring) |
61 | 15 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 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 26027 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠
‘𝑃)𝑥)) ≤ (𝐷‘𝑥)) |
64 | | simpll 766 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝜑) |
65 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝐸)) |
66 | 46 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 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 7061 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 Fn (Base‘𝑃) → (𝑥 ∈ (◡𝐷 “ (-∞[,)𝑁)) ↔ (𝑥 ∈ (Base‘𝑃) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)))) |
74 | 73 | simplbda 499 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 Fn (Base‘𝑃) ∧ 𝑥 ∈ (◡𝐷 “ (-∞[,)𝑁))) → (𝐷‘𝑥) ∈ (-∞[,)𝑁)) |
75 | 70, 72, 74 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ (-∞[,)𝑁)) |
76 | | elico1 13391 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-∞ ∈ ℝ* ∧ 𝑁 ∈ ℝ*) → ((𝐷‘𝑥) ∈ (-∞[,)𝑁) ↔ ((𝐷‘𝑥) ∈ ℝ* ∧ -∞
≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁))) |
77 | 76 | biimpa 476 |
. . . . . . . . . . . . . . . . . 18
⊢
(((-∞ ∈ ℝ* ∧ 𝑁 ∈ ℝ*) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → ((𝐷‘𝑥) ∈ ℝ* ∧ -∞
≤ (𝐷‘𝑥) ∧ (𝐷‘𝑥) < 𝑁)) |
78 | 77 | simp3d 1142 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞ ∈ ℝ* ∧ 𝑁 ∈ ℝ*) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)) → (𝐷‘𝑥) < 𝑁) |
79 | 68, 69, 75, 78 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) < 𝑁) |
80 | 64, 67, 79 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘𝑥) < 𝑁) |
81 | 57, 59, 55, 63, 80 | xrlelttrd 13163 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠
‘𝑃)𝑥)) < 𝑁) |
82 | 52, 55, 57, 58, 81 | elicod 13398 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠
‘𝑃)𝑥)) ∈ (-∞[,)𝑁)) |
83 | 36, 50, 82 | elpreimad 7062 |
. . . . . . . . . . . 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
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑥 ∈ (Base‘𝐸))) → (𝑘( ·𝑠
‘𝑃)𝑥) ∈ 𝑆) |
87 | 12 | ad2antrr 725 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃))) |
88 | 34, 35 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝐷 Fn (Base‘𝑃)) |
89 | | eqid 2727 |
. . . . . . . . . . . . . . . 16
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
90 | 89, 33 | mgpbas 20071 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) |
91 | | eqid 2727 |
. . . . . . . . . . . . . . 15
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
92 | 1 | ply1ring 22153 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
93 | 89 | ringmgp 20170 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) |
94 | 6, 92, 93 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (mulGrp‘𝑃) ∈ Mnd) |
96 | | elfzonn0 13701 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℕ0) |
97 | 96 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ0) |
98 | | eqid 2727 |
. . . . . . . . . . . . . . . . . 18
⊢
(var1‘𝑅) = (var1‘𝑅) |
99 | 98, 1, 33 | vr1cl 22123 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ (Base‘𝑃)) |
100 | 6, 99 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(var1‘𝑅)
∈ (Base‘𝑃)) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (var1‘𝑅) ∈ (Base‘𝑃)) |
102 | 90, 91, 95, 97, 101 | mulgnn0cld 19041 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) |
103 | 51 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ∈
ℝ*) |
104 | 54 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑁 ∈
ℝ*) |
105 | 24, 1, 33 | deg1xrcl 26005 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈
ℝ*) |
106 | 102, 105 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈
ℝ*) |
107 | 106 | mnfled 13139 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ≤ (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
108 | 96 | nn0red 12555 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ) |
109 | 108 | rexrd 11286 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ*) |
110 | 109 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℝ*) |
111 | 24, 1, 98, 89, 91 | deg1pwle 26042 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0)
→ (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ≤ 𝑛) |
112 | 6, 96, 111 | syl2an 595 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ≤ 𝑛) |
113 | | elfzolt2 13665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 < 𝑁) |
114 | 113 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 < 𝑁) |
115 | 106, 110,
104, 112, 114 | xrlelttrd 13163 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) < 𝑁) |
116 | 103, 104,
106, 107, 115 | elicod 13398 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ (-∞[,)𝑁)) |
117 | 88, 102, 116 | elpreimad 7062 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (◡𝐷 “ (-∞[,)𝑁))) |
118 | 117, 25 | eleqtrrdi 2839 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ 𝑆) |
119 | 46 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑆 = (Base‘𝐸)) |
120 | 118, 119 | eleqtrd 2830 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝐸)) |
121 | 120, 8 | fmptd 7118 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝐸)) |
122 | 121 | ad3antrrr 729 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝐹:(0..^𝑁)⟶(Base‘𝐸)) |
123 | | inidm 4214 |
. . . . . . . . 9
⊢
((0..^𝑁) ∩
(0..^𝑁)) = (0..^𝑁) |
124 | 86, 87, 122, 21, 21, 123 | off 7697 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹):(0..^𝑁)⟶𝑆) |
125 | 21, 32, 124, 44 | gsumsubm 18778 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹))) |
126 | | ringmnd 20174 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd) |
127 | 6, 92, 126 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ Mnd) |
128 | 34, 35 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 Fn (Base‘𝑃)) |
129 | 33, 10 | mndidcl 18700 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Mnd →
(0g‘𝑃)
∈ (Base‘𝑃)) |
130 | 127, 129 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0g‘𝑃) ∈ (Base‘𝑃)) |
131 | 51 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → -∞ ∈
ℝ*) |
132 | 24, 1, 33 | deg1xrcl 26005 |
. . . . . . . . . . . . 13
⊢
((0g‘𝑃) ∈ (Base‘𝑃) → (𝐷‘(0g‘𝑃)) ∈
ℝ*) |
133 | 130, 132 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) ∈
ℝ*) |
134 | 133 | mnfled 13139 |
. . . . . . . . . . . 12
⊢ (𝜑 → -∞ ≤ (𝐷‘(0g‘𝑃))) |
135 | 24, 1, 10 | deg1z 26010 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → (𝐷‘(0g‘𝑃)) = -∞) |
136 | 6, 135 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) = -∞) |
137 | 53 | mnfltd 13128 |
. . . . . . . . . . . . 13
⊢ (𝜑 → -∞ < 𝑁) |
138 | 136, 137 | eqbrtrd 5164 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) < 𝑁) |
139 | 131, 54, 133, 134, 138 | elicod 13398 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) ∈ (-∞[,)𝑁)) |
140 | 128, 130,
139 | elpreimad 7062 |
. . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑃) ∈ (◡𝐷 “ (-∞[,)𝑁))) |
141 | 140, 25 | eleqtrrdi 2839 |
. . . . . . . . 9
⊢ (𝜑 → (0g‘𝑃) ∈ 𝑆) |
142 | 44, 33, 10 | ress0g 18713 |
. . . . . . . . 9
⊢ ((𝑃 ∈ Mnd ∧
(0g‘𝑃)
∈ 𝑆 ∧ 𝑆 ⊆ (Base‘𝑃)) →
(0g‘𝑃) =
(0g‘𝐸)) |
143 | 127, 141,
43, 142 | syl3anc 1369 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑃) = (0g‘𝐸)) |
144 | 143 | ad3antrrr 729 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → (0g‘𝑃) = (0g‘𝐸)) |
145 | 20, 125, 144 | 3eqtr4d 2777 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝑃)) |
146 | 1, 2, 4, 7, 8, 9, 10, 19, 145 | ply1gsumz 33201 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0g‘𝑅)})) |
147 | 14 | fveq2d 6895 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
148 | 147 | sneqd 4636 |
. . . . . . 7
⊢ (𝜑 →
{(0g‘𝑅)} =
{(0g‘(Scalar‘𝑃))}) |
149 | 148 | xpeq2d 5702 |
. . . . . 6
⊢ (𝜑 → ((0..^𝑁) × {(0g‘𝑅)}) = ((0..^𝑁) ×
{(0g‘(Scalar‘𝑃))})) |
150 | 149 | ad3antrrr 729 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → ((0..^𝑁) × {(0g‘𝑅)}) = ((0..^𝑁) ×
{(0g‘(Scalar‘𝑃))})) |
151 | 146, 150 | eqtrd 2767 |
. . . 4
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑎 = ((0..^𝑁) ×
{(0g‘(Scalar‘𝑃))})) |
152 | 151 | expl 457 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) → ((𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑎 = ((0..^𝑁) ×
{(0g‘(Scalar‘𝑃))}))) |
153 | 152 | ralrimiva 3141 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))((𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑎 = ((0..^𝑁) ×
{(0g‘(Scalar‘𝑃))}))) |
154 | 118, 8 | fmptd 7118 |
. . . . . 6
⊢ (𝜑 → 𝐹:(0..^𝑁)⟶𝑆) |
155 | 154 | frnd 6724 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ 𝑆) |
156 | | eqid 2727 |
. . . . . 6
⊢
(LSpan‘𝑃) =
(LSpan‘𝑃) |
157 | 27, 156 | lspssp 20861 |
. . . . 5
⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆) |
158 | 23, 26, 155, 157 | syl3anc 1369 |
. . . 4
⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆) |
159 | | breq1 5145 |
. . . . . . . 8
⊢ (𝑎 = ((coe1‘𝑥) ↾ (0..^𝑁)) → (𝑎 finSupp
(0g‘(Scalar‘𝑃)) ↔ ((coe1‘𝑥) ↾ (0..^𝑁)) finSupp
(0g‘(Scalar‘𝑃)))) |
160 | | oveq1 7421 |
. . . . . . . . . 10
⊢ (𝑎 = ((coe1‘𝑥) ↾ (0..^𝑁)) → (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹) = (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)𝐹)) |
161 | 160 | oveq2d 7430 |
. . . . . . . . 9
⊢ (𝑎 = ((coe1‘𝑥) ↾ (0..^𝑁)) → (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (𝑃 Σg
(((coe1‘𝑥)
↾ (0..^𝑁))
∘f ( ·𝑠 ‘𝑃)𝐹))) |
162 | 161 | eqeq2d 2738 |
. . . . . . . 8
⊢ (𝑎 = ((coe1‘𝑥) ↾ (0..^𝑁)) → (𝑥 = (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) ↔ 𝑥 = (𝑃 Σg
(((coe1‘𝑥)
↾ (0..^𝑁))
∘f ( ·𝑠 ‘𝑃)𝐹)))) |
163 | 159, 162 | anbi12d 630 |
. . . . . . 7
⊢ (𝑎 = ((coe1‘𝑥) ↾ (0..^𝑁)) → ((𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹))) ↔ (((coe1‘𝑥) ↾ (0..^𝑁)) finSupp
(0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg
(((coe1‘𝑥)
↾ (0..^𝑁))
∘f ( ·𝑠 ‘𝑃)𝐹))))) |
164 | | fvexd 6906 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘(Scalar‘𝑃)) ∈ V) |
165 | | ovexd 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ V) |
166 | 43 | sselda 3978 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑃)) |
167 | | eqid 2727 |
. . . . . . . . . . . 12
⊢
(coe1‘𝑥) = (coe1‘𝑥) |
168 | 167, 33, 1, 2 | coe1f 22117 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (Base‘𝑃) →
(coe1‘𝑥):ℕ0⟶(Base‘𝑅)) |
169 | 166, 168 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe1‘𝑥):ℕ0⟶(Base‘𝑅)) |
170 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘𝑅) = (Base‘(Scalar‘𝑃))) |
171 | 170 | feq3d 6703 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe1‘𝑥):ℕ0⟶(Base‘𝑅) ↔
(coe1‘𝑥):ℕ0⟶(Base‘(Scalar‘𝑃)))) |
172 | 169, 171 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe1‘𝑥):ℕ0⟶(Base‘(Scalar‘𝑃))) |
173 | | fzo0ssnn0 13737 |
. . . . . . . . . 10
⊢
(0..^𝑁) ⊆
ℕ0 |
174 | 173 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆
ℕ0) |
175 | 172, 174 | fssresd 6758 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe1‘𝑥) ↾ (0..^𝑁)):(0..^𝑁)⟶(Base‘(Scalar‘𝑃))) |
176 | 164, 165,
175 | elmapdd 8851 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe1‘𝑥) ↾ (0..^𝑁)) ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) |
177 | 169 | ffund 6720 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (coe1‘𝑥)) |
178 | | fzofi 13963 |
. . . . . . . . . 10
⊢
(0..^𝑁) ∈
Fin |
179 | 178 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ Fin) |
180 | | fvexd 6906 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) →
(0g‘(Scalar‘𝑃)) ∈ V) |
181 | 177, 179,
180 | resfifsupp 9412 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe1‘𝑥) ↾ (0..^𝑁)) finSupp
(0g‘(Scalar‘𝑃))) |
182 | | ringcmn 20207 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) |
183 | 6, 92, 182 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ CMnd) |
184 | 183 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑃 ∈ CMnd) |
185 | | nn0ex 12500 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
186 | 185 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ℕ0 ∈
V) |
187 | 23 | ad2antrr 725 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑃 ∈ LMod) |
188 | 172 | ffvelcdmda 7088 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) →
((coe1‘𝑥)‘𝑖) ∈ (Base‘(Scalar‘𝑃))) |
189 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑅 ∈ Ring) |
190 | 189, 92, 93 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) →
(mulGrp‘𝑃) ∈
Mnd) |
191 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) |
192 | 189, 99 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) →
(var1‘𝑅)
∈ (Base‘𝑃)) |
193 | 90, 91, 190, 191, 192 | mulgnn0cld 19041 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) |
194 | 33, 37, 38, 39, 187, 188, 193 | lmodvscld 20751 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) →
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ (Base‘𝑃)) |
195 | | eqid 2727 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
196 | 194, 195 | fmptd 7118 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))):ℕ0⟶(Base‘𝑃)) |
197 | | nfv 1910 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝜑 ∧ 𝑥 ∈ 𝑆) |
198 | 197, 194,
195 | fnmptd 6690 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) Fn
ℕ0) |
199 | | fveq2 6891 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → ((coe1‘𝑥)‘𝑖) = ((coe1‘𝑥)‘𝑗)) |
200 | | oveq1 7421 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
201 | 199, 200 | oveq12d 7432 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
(((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
202 | | simplr 768 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℕ0) |
203 | | ovexd 7449 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ V) |
204 | 195, 201,
202, 203 | fvmptd3 7022 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗) = (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
205 | 166 | ad2antrr 725 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑥 ∈ (Base‘𝑃)) |
206 | | icossxr 13433 |
. . . . . . . . . . . . . . . . 17
⊢
(-∞[,)𝑁)
⊆ ℝ* |
207 | 206, 75 | sselid 3976 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈
ℝ*) |
208 | 207 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) ∈
ℝ*) |
209 | 54 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑁 ∈
ℝ*) |
210 | 202 | nn0red 12555 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ) |
211 | 210 | rexrd 11286 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ*) |
212 | 79 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑁) |
213 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑁 ≤ 𝑗) |
214 | 208, 209,
211, 212, 213 | xrltletrd 13164 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑗) |
215 | 24, 1, 33, 9, 167 | deg1lt 26020 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (Base‘𝑃) ∧ 𝑗 ∈ ℕ0 ∧ (𝐷‘𝑥) < 𝑗) → ((coe1‘𝑥)‘𝑗) = (0g‘𝑅)) |
216 | 205, 202,
214, 215 | syl3anc 1369 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → ((coe1‘𝑥)‘𝑗) = (0g‘𝑅)) |
217 | 216 | oveq1d 7429 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
((0g‘𝑅)(
·𝑠 ‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
218 | 147 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) |
219 | 218 | oveq1d 7429 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → ((0g‘𝑅)(
·𝑠 ‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
220 | 23 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑃 ∈ LMod) |
221 | 94 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (mulGrp‘𝑃) ∈ Mnd) |
222 | 100 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (var1‘𝑅) ∈ (Base‘𝑃)) |
223 | 90, 91, 221, 202, 222 | mulgnn0cld 19041 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) |
224 | | eqid 2727 |
. . . . . . . . . . . . . . 15
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) |
225 | 33, 37, 38, 224, 10 | lmod0vs 20767 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ LMod ∧ (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃)) |
226 | 220, 223,
225 | syl2anc 583 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃)) |
227 | 219, 226 | eqtrd 2767 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → ((0g‘𝑅)(
·𝑠 ‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃)) |
228 | 204, 217,
227 | 3eqtrd 2771 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗) = (0g‘𝑃)) |
229 | 3 | nn0zd 12606 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
230 | 229 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℤ) |
231 | 198, 228,
230 | suppssnn0 32558 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) supp
(0g‘𝑃))
⊆ (0..^𝑁)) |
232 | 186 | mptexd 7230 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ V) |
233 | 198 | fnfund 6649 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) |
234 | | fvexd 6906 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0g‘𝑃) ∈ V) |
235 | | suppssfifsupp 9395 |
. . . . . . . . . . 11
⊢ ((((𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ V ∧ Fun (𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∧
(0g‘𝑃)
∈ V) ∧ ((0..^𝑁)
∈ Fin ∧ ((𝑖 ∈
ℕ0 ↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) supp
(0g‘𝑃))
⊆ (0..^𝑁))) →
(𝑖 ∈
ℕ0 ↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) finSupp
(0g‘𝑃)) |
236 | 232, 233,
234, 179, 231, 235 | syl32anc 1376 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) finSupp
(0g‘𝑃)) |
237 | 33, 10, 184, 186, 196, 231, 236 | gsumres 19859 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σg ((𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ↾ (0..^𝑁))) = (𝑃 Σg (𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) |
238 | | fvexd 6906 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe1‘𝑥) ∈ V) |
239 | | ovexd 7449 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0..^𝑁) ∈ V) |
240 | 154, 239 | fexd 7233 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ V) |
241 | 240 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 ∈ V) |
242 | | offres 7981 |
. . . . . . . . . . . 12
⊢
(((coe1‘𝑥) ∈ V ∧ 𝐹 ∈ V) →
(((coe1‘𝑥)
∘f ( ·𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁)))) |
243 | 238, 241,
242 | syl2anc 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁)))) |
244 | 169 | ffnd 6717 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe1‘𝑥) Fn
ℕ0) |
245 | 154 | ffnd 6717 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 Fn (0..^𝑁)) |
246 | 245 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 Fn (0..^𝑁)) |
247 | | sseqin2 4211 |
. . . . . . . . . . . . . . . 16
⊢
((0..^𝑁) ⊆
ℕ0 ↔ (ℕ0 ∩ (0..^𝑁)) = (0..^𝑁)) |
248 | 173, 247 | mpbi 229 |
. . . . . . . . . . . . . . 15
⊢
(ℕ0 ∩ (0..^𝑁)) = (0..^𝑁) |
249 | | eqidd 2728 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) →
((coe1‘𝑥)‘𝑗) = ((coe1‘𝑥)‘𝑗)) |
250 | | oveq1 7421 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
251 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁)) |
252 | | ovexd 7449 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ V) |
253 | 8, 250, 251, 252 | fvmptd3 7022 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹‘𝑗) = (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
254 | 244, 246,
186, 165, 248, 249, 253 | ofval 7690 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹)‘𝑗) = (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
255 | 173, 251 | sselid 3976 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0) |
256 | | ovexd 7449 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ V) |
257 | 195, 201,
255, 256 | fvmptd3 7022 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗) = (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) |
258 | 254, 257 | eqtr4d 2770 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗)) |
259 | 258 | ralrimiva 3141 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑗 ∈ (0..^𝑁)(((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗)) |
260 | 244, 246,
186, 165, 248 | offn 7692 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹) Fn (0..^𝑁)) |
261 | | ssidd 4001 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ (0..^𝑁)) |
262 | | fvreseq0 7041 |
. . . . . . . . . . . . 13
⊢
(((((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹) Fn (0..^𝑁) ∧ (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) Fn ℕ0)
∧ ((0..^𝑁) ⊆
(0..^𝑁) ∧ (0..^𝑁) ⊆ ℕ0))
→ ((((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ↾ (0..^𝑁)) ↔ ∀𝑗 ∈ (0..^𝑁)(((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗))) |
263 | 260, 198,
261, 174, 262 | syl22anc 838 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ↾ (0..^𝑁)) ↔ ∀𝑗 ∈ (0..^𝑁)(((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗))) |
264 | 259, 263 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ↾ (0..^𝑁))) |
265 | | fnresdm 6668 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn (0..^𝑁) → (𝐹 ↾ (0..^𝑁)) = 𝐹) |
266 | 245, 265 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) = 𝐹) |
267 | 266 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐹 ↾ (0..^𝑁)) = 𝐹) |
268 | 267 | oveq2d 7430 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))) = (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)𝐹)) |
269 | 243, 264,
268 | 3eqtr3rd 2776 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)𝐹) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ↾ (0..^𝑁))) |
270 | 269 | oveq2d 7430 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σg
(((coe1‘𝑥)
↾ (0..^𝑁))
∘f ( ·𝑠 ‘𝑃)𝐹)) = (𝑃 Σg ((𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ↾ (0..^𝑁)))) |
271 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ Ring) |
272 | 1, 98, 33, 38, 89, 91, 167 | ply1coe 22204 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σg (𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) |
273 | 271, 166,
272 | syl2anc 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σg (𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) |
274 | 237, 270,
273 | 3eqtr4rd 2778 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σg
(((coe1‘𝑥)
↾ (0..^𝑁))
∘f ( ·𝑠 ‘𝑃)𝐹))) |
275 | 181, 274 | jca 511 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe1‘𝑥) ↾ (0..^𝑁)) finSupp
(0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg
(((coe1‘𝑥)
↾ (0..^𝑁))
∘f ( ·𝑠 ‘𝑃)𝐹)))) |
276 | 163, 176,
275 | rspcedvdw 3610 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))(𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)))) |
277 | 102, 8 | fmptd 7118 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝑃)) |
278 | 156, 33, 39, 37, 224, 38, 277, 23, 239 | ellspd 21723 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))(𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹))))) |
279 | 278 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁))) ↔ ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))(𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹))))) |
280 | 276, 279 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁)))) |
281 | | imadmrn 6067 |
. . . . . . . 8
⊢ (𝐹 “ dom 𝐹) = ran 𝐹 |
282 | 154 | fdmd 6727 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = (0..^𝑁)) |
283 | 282 | imaeq2d 6057 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ dom 𝐹) = (𝐹 “ (0..^𝑁))) |
284 | 281, 283 | eqtr3id 2781 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 = (𝐹 “ (0..^𝑁))) |
285 | 284 | fveq2d 6895 |
. . . . . 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 3999 |
. . 3
⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = 𝑆) |
289 | | eqid 2727 |
. . . . . 6
⊢
(LSpan‘𝐸) =
(LSpan‘𝐸) |
290 | 44, 156, 289, 27 | lsslsp 20888 |
. . . . 5
⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝐸)‘ran 𝐹) = ((LSpan‘𝑃)‘ran 𝐹)) |
291 | 290 | eqcomd 2733 |
. . . 4
⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹)) |
292 | 23, 26, 155, 291 | syl3anc 1369 |
. . 3
⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹)) |
293 | 288, 292,
46 | 3eqtr3d 2775 |
. 2
⊢ (𝜑 → ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸)) |
294 | | eqid 2727 |
. . 3
⊢
(Base‘𝐸) =
(Base‘𝐸) |
295 | 24 | fvexi 6905 |
. . . . . . 7
⊢ 𝐷 ∈ V |
296 | | cnvexg 7926 |
. . . . . . 7
⊢ (𝐷 ∈ V → ◡𝐷 ∈ V) |
297 | | imaexg 7915 |
. . . . . . 7
⊢ (◡𝐷 ∈ V → (◡𝐷 “ (-∞[,)𝑁)) ∈ V) |
298 | 295, 296,
297 | mp2b 10 |
. . . . . 6
⊢ (◡𝐷 “ (-∞[,)𝑁)) ∈ V |
299 | 25, 298 | eqeltri 2824 |
. . . . 5
⊢ 𝑆 ∈ V |
300 | 44, 37 | resssca 17315 |
. . . . 5
⊢ (𝑆 ∈ V →
(Scalar‘𝑃) =
(Scalar‘𝐸)) |
301 | 299, 300 | ax-mp 5 |
. . . 4
⊢
(Scalar‘𝑃) =
(Scalar‘𝐸) |
302 | 301 | fveq2i 6894 |
. . 3
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝐸)) |
303 | | eqid 2727 |
. . 3
⊢
(Scalar‘𝐸) =
(Scalar‘𝐸) |
304 | 44, 38 | ressvsca 17316 |
. . . 4
⊢ (𝑆 ∈ V → (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝐸)) |
305 | 299, 304 | ax-mp 5 |
. . 3
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝐸) |
306 | | eqid 2727 |
. . 3
⊢
(0g‘𝐸) = (0g‘𝐸) |
307 | 301 | fveq2i 6894 |
. . 3
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝐸)) |
308 | | eqid 2727 |
. . 3
⊢
(LBasis‘𝐸) =
(LBasis‘𝐸) |
309 | 44, 27 | lsslvec 20983 |
. . . . 5
⊢ ((𝑃 ∈ LVec ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝐸 ∈ LVec) |
310 | 22, 26, 309 | syl2anc 583 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ LVec) |
311 | 310 | lveclmodd 20981 |
. . 3
⊢ (𝜑 → 𝐸 ∈ LMod) |
312 | 14, 5 | eqeltrrd 2829 |
. . . . 5
⊢ (𝜑 → (Scalar‘𝑃) ∈
DivRing) |
313 | | drngnzr 20633 |
. . . . 5
⊢
((Scalar‘𝑃)
∈ DivRing → (Scalar‘𝑃) ∈ NzRing) |
314 | 312, 313 | syl 17 |
. . . 4
⊢ (𝜑 → (Scalar‘𝑃) ∈
NzRing) |
315 | 301, 314 | eqeltrrid 2833 |
. . 3
⊢ (𝜑 → (Scalar‘𝐸) ∈
NzRing) |
316 | 120 | ralrimiva 3141 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝐸)) |
317 | | drngnzr 20633 |
. . . . . . . . . 10
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ NzRing) |
318 | 5, 317 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ NzRing) |
319 | 318 | ad2antrr 725 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑅 ∈ NzRing) |
320 | 97 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ0) |
321 | | elfzonn0 13701 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℕ0) |
322 | 321 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ ℕ0) |
323 | 1, 98, 91, 319, 320, 322 | ply1moneq 33196 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ↔ 𝑛 = 𝑖)) |
324 | 323 | biimpd 228 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) → 𝑛 = 𝑖)) |
325 | 324 | anasss 466 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (0..^𝑁) ∧ 𝑖 ∈ (0..^𝑁))) → ((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) → 𝑛 = 𝑖)) |
326 | 325 | ralrimivva 3195 |
. . . 4
⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) → 𝑛 = 𝑖)) |
327 | | oveq1 7421 |
. . . . 5
⊢ (𝑛 = 𝑖 → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))) |
328 | 8, 327 | f1mpt 7265 |
. . . 4
⊢ (𝐹:(0..^𝑁)–1-1→(Base‘𝐸) ↔ (∀𝑛 ∈ (0..^𝑁)(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝐸) ∧ ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) → 𝑛 = 𝑖))) |
329 | 316, 326,
328 | sylanbrc 582 |
. . 3
⊢ (𝜑 → 𝐹:(0..^𝑁)–1-1→(Base‘𝐸)) |
330 | 294, 302,
303, 305, 306, 307, 308, 289, 311, 315, 239, 329 | islbs5 33035 |
. 2
⊢ (𝜑 → (ran 𝐹 ∈ (LBasis‘𝐸) ↔ (∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))((𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑎 = ((0..^𝑁) ×
{(0g‘(Scalar‘𝑃))})) ∧ ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸)))) |
331 | 153, 293,
330 | mpbir2and 712 |
1
⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸)) |