| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ply1degltdim.p | . . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) | 
| 2 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 3 |  | ply1degltdim.n | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 4 | 3 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑁 ∈
ℕ0) | 
| 5 |  | ply1degltdim.r | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ DivRing) | 
| 6 | 5 | drngringd 20738 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 7 | 6 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑅 ∈ Ring) | 
| 8 |  | ply1degltdimlem.f | . . . . . 6
⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) | 
| 9 |  | eqid 2736 | . . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 10 |  | eqid 2736 | . . . . . 6
⊢
(0g‘𝑃) = (0g‘𝑃) | 
| 11 |  | elmapi 8890 | . . . . . . . . 9
⊢ (𝑎 ∈
((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁)) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃))) | 
| 12 | 11 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) → 𝑎:(0..^𝑁)⟶(Base‘(Scalar‘𝑃))) | 
| 13 | 1 | ply1sca 22255 | . . . . . . . . . . . 12
⊢ (𝑅 ∈ DivRing → 𝑅 = (Scalar‘𝑃)) | 
| 14 | 5, 13 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑅 = (Scalar‘𝑃)) | 
| 15 | 14 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑃))) | 
| 16 | 15 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) → (Base‘𝑅) =
(Base‘(Scalar‘𝑃))) | 
| 17 | 16 | feq3d 6722 | . . . . . . . 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
(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 7467 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → (0..^𝑁) ∈ V) | 
| 22 | 1, 5 | ply1lvec 33586 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ LVec) | 
| 23 | 22 | lveclmodd 21107 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ LMod) | 
| 24 |  | ply1degltdim.d | . . . . . . . . . . . 12
⊢ 𝐷 = (deg1‘𝑅) | 
| 25 |  | ply1degltdim.s | . . . . . . . . . . . 12
⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁)) | 
| 26 | 1, 24, 25, 3, 6 | ply1degltlss 33618 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑃)) | 
| 27 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(LSubSp‘𝑃) =
(LSubSp‘𝑃) | 
| 28 | 27 | lsssubg 20956 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝑆 ∈ (SubGrp‘𝑃)) | 
| 29 | 23, 26, 28 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑃)) | 
| 30 |  | subgsubm 19167 | . . . . . . . . . 10
⊢ (𝑆 ∈ (SubGrp‘𝑃) → 𝑆 ∈ (SubMnd‘𝑃)) | 
| 31 | 29, 30 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑃)) | 
| 32 | 31 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑆 ∈ (SubMnd‘𝑃)) | 
| 33 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(Base‘𝑃) =
(Base‘𝑃) | 
| 34 | 24, 1, 33 | deg1xrf 26121 | . . . . . . . . . . . . . 14
⊢ 𝐷:(Base‘𝑃)⟶ℝ* | 
| 35 |  | ffn 6735 | . . . . . . . . . . . . . 14
⊢ (𝐷:(Base‘𝑃)⟶ℝ* → 𝐷 Fn (Base‘𝑃)) | 
| 36 | 34, 35 | mp1i 13 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷 Fn (Base‘𝑃)) | 
| 37 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) | 
| 38 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) | 
| 39 |  | eqid 2736 | . . . . . . . . . . . . . 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 20935 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈ (LSubSp‘𝑃) → 𝑆 ⊆ (Base‘𝑃)) | 
| 43 | 26, 42 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑃)) | 
| 44 |  | ply1degltdim.e | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐸 = (𝑃 ↾s 𝑆) | 
| 45 | 44, 33 | ressbas2 17284 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ⊆ (Base‘𝑃) → 𝑆 = (Base‘𝐸)) | 
| 46 | 43, 45 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 = (Base‘𝐸)) | 
| 47 | 46, 43 | eqsstrrd 4018 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Base‘𝐸) ⊆ (Base‘𝑃)) | 
| 48 | 47 | sselda 3982 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃)) | 
| 49 | 48 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑥 ∈ (Base‘𝑃)) | 
| 50 | 33, 37, 38, 39, 40, 41, 49 | lmodvscld 20878 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·𝑠
‘𝑃)𝑥) ∈ (Base‘𝑃)) | 
| 51 |  | mnfxr 11319 | . . . . . . . . . . . . . . 15
⊢ -∞
∈ ℝ* | 
| 52 | 51 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ∈
ℝ*) | 
| 53 | 3 | nn0red 12590 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 54 | 53 | rexrd 11312 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℝ*) | 
| 55 | 54 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑁 ∈
ℝ*) | 
| 56 | 34 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝐷:(Base‘𝑃)⟶ℝ*) | 
| 57 | 56, 50 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠
‘𝑃)𝑥)) ∈
ℝ*) | 
| 58 | 57 | mnfled 13179 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → -∞ ≤ (𝐷‘(𝑘( ·𝑠
‘𝑃)𝑥))) | 
| 59 | 56, 49 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 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 2843 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → 𝑘 ∈ (Base‘𝑅)) | 
| 63 | 1, 24, 60, 33, 2, 38, 62, 49 | deg1vscale 26144 | . . . . . . . . . . . . . . 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 2843 | . . . . . . . . . . . . . . . 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 2850 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (◡𝐷 “ (-∞[,)𝑁))) | 
| 73 |  | elpreima 7077 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 Fn (Base‘𝑃) → (𝑥 ∈ (◡𝐷 “ (-∞[,)𝑁)) ↔ (𝑥 ∈ (Base‘𝑃) ∧ (𝐷‘𝑥) ∈ (-∞[,)𝑁)))) | 
| 74 | 73 | simplbda 499 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 Fn (Base‘𝑃) ∧ 𝑥 ∈ (◡𝐷 “ (-∞[,)𝑁))) → (𝐷‘𝑥) ∈ (-∞[,)𝑁)) | 
| 75 | 70, 72, 74 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈ (-∞[,)𝑁)) | 
| 76 |  | elico1 13431 | . . . . . . . . . . . . . . . . . . 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 13203 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠
‘𝑃)𝑥)) < 𝑁) | 
| 82 | 52, 55, 57, 58, 81 | elicod 13438 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝐷‘(𝑘( ·𝑠
‘𝑃)𝑥)) ∈ (-∞[,)𝑁)) | 
| 83 | 36, 50, 82 | elpreimad 7078 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑃))) ∧ 𝑥 ∈ (Base‘𝐸)) → (𝑘( ·𝑠
‘𝑃)𝑥) ∈ (◡𝐷 “ (-∞[,)𝑁))) | 
| 84 | 83, 25 | eleqtrrdi 2851 | . . . . . . . . . . 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 726 | . . . . . . . . 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 2736 | . . . . . . . . . . . . . . . 16
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) | 
| 90 | 89, 33 | mgpbas 20143 | . . . . . . . . . . . . . . 15
⊢
(Base‘𝑃) =
(Base‘(mulGrp‘𝑃)) | 
| 91 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) | 
| 92 | 1 | ply1ring 22250 | . . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) | 
| 93 | 89 | ringmgp 20237 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Ring →
(mulGrp‘𝑃) ∈
Mnd) | 
| 94 | 6, 92, 93 | 3syl 18 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd) | 
| 95 | 94 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (mulGrp‘𝑃) ∈ Mnd) | 
| 96 |  | elfzonn0 13748 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℕ0) | 
| 97 | 96 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℕ0) | 
| 98 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(var1‘𝑅) = (var1‘𝑅) | 
| 99 | 98, 1, 33 | vr1cl 22220 | . . . . . . . . . . . . . . . . 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 19114 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) | 
| 103 | 51 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ∈
ℝ*) | 
| 104 | 54 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑁 ∈
ℝ*) | 
| 105 | 24, 1, 33 | deg1xrcl 26122 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈
ℝ*) | 
| 106 | 102, 105 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈
ℝ*) | 
| 107 | 106 | mnfled 13179 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → -∞ ≤ (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) | 
| 108 | 96 | nn0red 12590 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ) | 
| 109 | 108 | rexrd 11312 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 ∈ ℝ*) | 
| 110 | 109 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 ∈ ℝ*) | 
| 111 | 24, 1, 98, 89, 91 | deg1pwle 26160 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0)
→ (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ≤ 𝑛) | 
| 112 | 6, 96, 111 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ≤ 𝑛) | 
| 113 |  | elfzolt2 13709 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (0..^𝑁) → 𝑛 < 𝑁) | 
| 114 | 113 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑛 < 𝑁) | 
| 115 | 106, 110,
104, 112, 114 | xrlelttrd 13203 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) < 𝑁) | 
| 116 | 103, 104,
106, 107, 115 | elicod 13438 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝐷‘(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ (-∞[,)𝑁)) | 
| 117 | 88, 102, 116 | elpreimad 7078 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (◡𝐷 “ (-∞[,)𝑁))) | 
| 118 | 117, 25 | eleqtrrdi 2851 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ 𝑆) | 
| 119 | 46 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → 𝑆 = (Base‘𝐸)) | 
| 120 | 118, 119 | eleqtrd 2842 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝐸)) | 
| 121 | 120, 8 | fmptd 7133 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝐸)) | 
| 122 | 121 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝐹:(0..^𝑁)⟶(Base‘𝐸)) | 
| 123 |  | inidm 4226 | . . . . . . . . 9
⊢
((0..^𝑁) ∩
(0..^𝑁)) = (0..^𝑁) | 
| 124 | 86, 87, 122, 21, 21, 123 | off 7716 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹):(0..^𝑁)⟶𝑆) | 
| 125 | 21, 32, 124, 44 | gsumsubm 18849 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹))) | 
| 126 |  | ringmnd 20241 | . . . . . . . . . 10
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd) | 
| 127 | 6, 92, 126 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ Mnd) | 
| 128 | 34, 35 | mp1i 13 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 Fn (Base‘𝑃)) | 
| 129 | 33, 10 | mndidcl 18763 | . . . . . . . . . . . 12
⊢ (𝑃 ∈ Mnd →
(0g‘𝑃)
∈ (Base‘𝑃)) | 
| 130 | 127, 129 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (0g‘𝑃) ∈ (Base‘𝑃)) | 
| 131 | 51 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → -∞ ∈
ℝ*) | 
| 132 | 24, 1, 33 | deg1xrcl 26122 | . . . . . . . . . . . . 13
⊢
((0g‘𝑃) ∈ (Base‘𝑃) → (𝐷‘(0g‘𝑃)) ∈
ℝ*) | 
| 133 | 130, 132 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) ∈
ℝ*) | 
| 134 | 133 | mnfled 13179 | . . . . . . . . . . . 12
⊢ (𝜑 → -∞ ≤ (𝐷‘(0g‘𝑃))) | 
| 135 | 24, 1, 10 | deg1z 26127 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → (𝐷‘(0g‘𝑃)) = -∞) | 
| 136 | 6, 135 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) = -∞) | 
| 137 | 53 | mnfltd 13167 | . . . . . . . . . . . . 13
⊢ (𝜑 → -∞ < 𝑁) | 
| 138 | 136, 137 | eqbrtrd 5164 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) < 𝑁) | 
| 139 | 131, 54, 133, 134, 138 | elicod 13438 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐷‘(0g‘𝑃)) ∈ (-∞[,)𝑁)) | 
| 140 | 128, 130,
139 | elpreimad 7078 | . . . . . . . . . 10
⊢ (𝜑 → (0g‘𝑃) ∈ (◡𝐷 “ (-∞[,)𝑁))) | 
| 141 | 140, 25 | eleqtrrdi 2851 | . . . . . . . . 9
⊢ (𝜑 → (0g‘𝑃) ∈ 𝑆) | 
| 142 | 44, 33, 10 | ress0g 18776 | . . . . . . . . 9
⊢ ((𝑃 ∈ Mnd ∧
(0g‘𝑃)
∈ 𝑆 ∧ 𝑆 ⊆ (Base‘𝑃)) →
(0g‘𝑃) =
(0g‘𝐸)) | 
| 143 | 127, 141,
43, 142 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (0g‘𝑃) = (0g‘𝐸)) | 
| 144 | 143 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → (0g‘𝑃) = (0g‘𝐸)) | 
| 145 | 20, 125, 144 | 3eqtr4d 2786 | . . . . . 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 33620 | . . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑎 = ((0..^𝑁) × {(0g‘𝑅)})) | 
| 147 | 14 | fveq2d 6909 | . . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) | 
| 148 | 147 | sneqd 4637 | . . . . . . 7
⊢ (𝜑 →
{(0g‘𝑅)} =
{(0g‘(Scalar‘𝑃))}) | 
| 149 | 148 | xpeq2d 5714 | . . . . . 6
⊢ (𝜑 → ((0..^𝑁) × {(0g‘𝑅)}) = ((0..^𝑁) ×
{(0g‘(Scalar‘𝑃))})) | 
| 150 | 149 | ad3antrrr 730 | . . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) ∧ 𝑎 finSupp
(0g‘(Scalar‘𝑃))) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → ((0..^𝑁) × {(0g‘𝑅)}) = ((0..^𝑁) ×
{(0g‘(Scalar‘𝑃))})) | 
| 151 | 146, 150 | eqtrd 2776 | . . . 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 3145 | . 2
⊢ (𝜑 → ∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))((𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑎 = ((0..^𝑁) ×
{(0g‘(Scalar‘𝑃))}))) | 
| 154 | 118, 8 | fmptd 7133 | . . . . . 6
⊢ (𝜑 → 𝐹:(0..^𝑁)⟶𝑆) | 
| 155 | 154 | frnd 6743 | . . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ 𝑆) | 
| 156 |  | eqid 2736 | . . . . . 6
⊢
(LSpan‘𝑃) =
(LSpan‘𝑃) | 
| 157 | 27, 156 | lspssp 20987 | . . . . 5
⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆) | 
| 158 | 23, 26, 155, 157 | syl3anc 1372 | . . . 4
⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) ⊆ 𝑆) | 
| 159 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑎 = ((coe1‘𝑥) ↾ (0..^𝑁)) → (𝑎 finSupp
(0g‘(Scalar‘𝑃)) ↔ ((coe1‘𝑥) ↾ (0..^𝑁)) finSupp
(0g‘(Scalar‘𝑃)))) | 
| 160 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑎 = ((coe1‘𝑥) ↾ (0..^𝑁)) → (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹) = (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)𝐹)) | 
| 161 | 160 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑎 = ((coe1‘𝑥) ↾ (0..^𝑁)) → (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (𝑃 Σg
(((coe1‘𝑥)
↾ (0..^𝑁))
∘f ( ·𝑠 ‘𝑃)𝐹))) | 
| 162 | 161 | eqeq2d 2747 | . . . . . . . 8
⊢ (𝑎 = ((coe1‘𝑥) ↾ (0..^𝑁)) → (𝑥 = (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) ↔ 𝑥 = (𝑃 Σg
(((coe1‘𝑥)
↾ (0..^𝑁))
∘f ( ·𝑠 ‘𝑃)𝐹)))) | 
| 163 | 159, 162 | anbi12d 632 | . . . . . . 7
⊢ (𝑎 = ((coe1‘𝑥) ↾ (0..^𝑁)) → ((𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹))) ↔ (((coe1‘𝑥) ↾ (0..^𝑁)) finSupp
(0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg
(((coe1‘𝑥)
↾ (0..^𝑁))
∘f ( ·𝑠 ‘𝑃)𝐹))))) | 
| 164 |  | fvexd 6920 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Base‘(Scalar‘𝑃)) ∈ V) | 
| 165 |  | ovexd 7467 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ V) | 
| 166 | 43 | sselda 3982 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝑃)) | 
| 167 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(coe1‘𝑥) = (coe1‘𝑥) | 
| 168 | 167, 33, 1, 2 | coe1f 22214 | . . . . . . . . . . 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 6722 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe1‘𝑥):ℕ0⟶(Base‘𝑅) ↔
(coe1‘𝑥):ℕ0⟶(Base‘(Scalar‘𝑃)))) | 
| 172 | 169, 171 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe1‘𝑥):ℕ0⟶(Base‘(Scalar‘𝑃))) | 
| 173 |  | fzo0ssnn0 13786 | . . . . . . . . . 10
⊢
(0..^𝑁) ⊆
ℕ0 | 
| 174 | 173 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆
ℕ0) | 
| 175 | 172, 174 | fssresd 6774 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe1‘𝑥) ↾ (0..^𝑁)):(0..^𝑁)⟶(Base‘(Scalar‘𝑃))) | 
| 176 | 164, 165,
175 | elmapdd 8882 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe1‘𝑥) ↾ (0..^𝑁)) ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))) | 
| 177 | 169 | ffund 6739 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (coe1‘𝑥)) | 
| 178 |  | fzofi 14016 | . . . . . . . . . 10
⊢
(0..^𝑁) ∈
Fin | 
| 179 | 178 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ∈ Fin) | 
| 180 |  | fvexd 6920 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) →
(0g‘(Scalar‘𝑃)) ∈ V) | 
| 181 | 177, 179,
180 | resfifsupp 9438 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe1‘𝑥) ↾ (0..^𝑁)) finSupp
(0g‘(Scalar‘𝑃))) | 
| 182 |  | ringcmn 20280 | . . . . . . . . . . . 12
⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd) | 
| 183 | 6, 92, 182 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ CMnd) | 
| 184 | 183 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑃 ∈ CMnd) | 
| 185 |  | nn0ex 12534 | . . . . . . . . . . 11
⊢
ℕ0 ∈ V | 
| 186 | 185 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ℕ0 ∈
V) | 
| 187 | 23 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → 𝑃 ∈ LMod) | 
| 188 | 172 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) →
((coe1‘𝑥)‘𝑖) ∈ (Base‘(Scalar‘𝑃))) | 
| 189 | 6 | ad2antrr 726 | . . . . . . . . . . . . . 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 19114 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) → (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) | 
| 194 | 33, 37, 38, 39, 187, 188, 193 | lmodvscld 20878 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑖 ∈ ℕ0) →
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ (Base‘𝑃)) | 
| 195 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) = (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) | 
| 196 | 194, 195 | fmptd 7133 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))):ℕ0⟶(Base‘𝑃)) | 
| 197 |  | nfv 1913 | . . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝜑 ∧ 𝑥 ∈ 𝑆) | 
| 198 | 197, 194,
195 | fnmptd 6708 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) Fn
ℕ0) | 
| 199 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → ((coe1‘𝑥)‘𝑖) = ((coe1‘𝑥)‘𝑗)) | 
| 200 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑗 → (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) | 
| 201 | 199, 200 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
(((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) | 
| 202 |  | simplr 768 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℕ0) | 
| 203 |  | ovexd 7467 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ V) | 
| 204 | 195, 201,
202, 203 | fvmptd3 7038 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗) = (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) | 
| 205 | 166 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑥 ∈ (Base‘𝑃)) | 
| 206 |  | icossxr 13473 | . . . . . . . . . . . . . . . . 17
⊢
(-∞[,)𝑁)
⊆ ℝ* | 
| 207 | 206, 75 | sselid 3980 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐷‘𝑥) ∈
ℝ*) | 
| 208 | 207 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) ∈
ℝ*) | 
| 209 | 54 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑁 ∈
ℝ*) | 
| 210 | 202 | nn0red 12590 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ) | 
| 211 | 210 | rexrd 11312 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑗 ∈ ℝ*) | 
| 212 | 79 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑁) | 
| 213 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑁 ≤ 𝑗) | 
| 214 | 208, 209,
211, 212, 213 | xrltletrd 13204 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (𝐷‘𝑥) < 𝑗) | 
| 215 | 24, 1, 33, 9, 167 | deg1lt 26137 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (Base‘𝑃) ∧ 𝑗 ∈ ℕ0 ∧ (𝐷‘𝑥) < 𝑗) → ((coe1‘𝑥)‘𝑗) = (0g‘𝑅)) | 
| 216 | 205, 202,
214, 215 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → ((coe1‘𝑥)‘𝑗) = (0g‘𝑅)) | 
| 217 | 216 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
((0g‘𝑅)(
·𝑠 ‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) | 
| 218 | 147 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (0g‘𝑅) =
(0g‘(Scalar‘𝑃))) | 
| 219 | 218 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → ((0g‘𝑅)(
·𝑠 ‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) =
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) | 
| 220 | 23 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → 𝑃 ∈ LMod) | 
| 221 | 94 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (mulGrp‘𝑃) ∈ Mnd) | 
| 222 | 100 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (var1‘𝑅) ∈ (Base‘𝑃)) | 
| 223 | 90, 91, 221, 202, 222 | mulgnn0cld 19114 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) | 
| 224 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝑃)) | 
| 225 | 33, 37, 38, 224, 10 | lmod0vs 20894 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ LMod ∧ (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝑃)) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃)) | 
| 226 | 220, 223,
225 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) →
((0g‘(Scalar‘𝑃))( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃)) | 
| 227 | 219, 226 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → ((0g‘𝑅)(
·𝑠 ‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = (0g‘𝑃)) | 
| 228 | 204, 217,
227 | 3eqtrd 2780 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑁 ≤ 𝑗) → ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗) = (0g‘𝑃)) | 
| 229 | 3 | nn0zd 12641 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 230 | 229 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ ℤ) | 
| 231 | 198, 228,
230 | suppssnn0 32810 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) supp
(0g‘𝑃))
⊆ (0..^𝑁)) | 
| 232 | 186 | mptexd 7245 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ V) | 
| 233 | 198 | fnfund 6668 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → Fun (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) | 
| 234 |  | fvexd 6920 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0g‘𝑃) ∈ V) | 
| 235 |  | suppssfifsupp 9421 | . . . . . . . . . . 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 1379 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) finSupp
(0g‘𝑃)) | 
| 237 | 33, 10, 184, 186, 196, 231, 236 | gsumres 19932 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑃 Σg ((𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ↾ (0..^𝑁))) = (𝑃 Σg (𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) | 
| 238 |  | fvexd 6920 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe1‘𝑥) ∈ V) | 
| 239 |  | ovexd 7467 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (0..^𝑁) ∈ V) | 
| 240 | 154, 239 | fexd 7248 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ V) | 
| 241 | 240 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 ∈ V) | 
| 242 |  | offres 8009 | . . . . . . . . . . . 12
⊢
(((coe1‘𝑥) ∈ V ∧ 𝐹 ∈ V) →
(((coe1‘𝑥)
∘f ( ·𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁)))) | 
| 243 | 238, 241,
242 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹) ↾ (0..^𝑁)) = (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁)))) | 
| 244 | 169 | ffnd 6736 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (coe1‘𝑥) Fn
ℕ0) | 
| 245 | 154 | ffnd 6736 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 Fn (0..^𝑁)) | 
| 246 | 245 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐹 Fn (0..^𝑁)) | 
| 247 |  | sseqin2 4222 | . . . . . . . . . . . . . . . 16
⊢
((0..^𝑁) ⊆
ℕ0 ↔ (ℕ0 ∩ (0..^𝑁)) = (0..^𝑁)) | 
| 248 | 173, 247 | mpbi 230 | . . . . . . . . . . . . . . 15
⊢
(ℕ0 ∩ (0..^𝑁)) = (0..^𝑁) | 
| 249 |  | eqidd 2737 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) →
((coe1‘𝑥)‘𝑗) = ((coe1‘𝑥)‘𝑗)) | 
| 250 |  | oveq1 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) | 
| 251 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁)) | 
| 252 |  | ovexd 7467 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ V) | 
| 253 | 8, 250, 251, 252 | fvmptd3 7038 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (𝐹‘𝑗) = (𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) | 
| 254 | 244, 246,
186, 165, 248, 249, 253 | ofval 7709 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹)‘𝑗) = (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) | 
| 255 | 173, 251 | sselid 3980 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ ℕ0) | 
| 256 |  | ovexd 7467 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ V) | 
| 257 | 195, 201,
255, 256 | fvmptd3 7038 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗) = (((coe1‘𝑥)‘𝑗)( ·𝑠
‘𝑃)(𝑗(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) | 
| 258 | 254, 257 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑗 ∈ (0..^𝑁)) → (((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗)) | 
| 259 | 258 | ralrimiva 3145 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∀𝑗 ∈ (0..^𝑁)(((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹)‘𝑗) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))))‘𝑗)) | 
| 260 | 244, 246,
186, 165, 248 | offn 7711 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((coe1‘𝑥) ∘f (
·𝑠 ‘𝑃)𝐹) Fn (0..^𝑁)) | 
| 261 |  | ssidd 4006 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (0..^𝑁) ⊆ (0..^𝑁)) | 
| 262 |  | fvreseq0 7057 | . . . . . . . . . . . . 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 6686 | . . . . . . . . . . . . . 14
⊢ (𝐹 Fn (0..^𝑁) → (𝐹 ↾ (0..^𝑁)) = 𝐹) | 
| 266 | 245, 265 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) = 𝐹) | 
| 267 | 266 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐹 ↾ (0..^𝑁)) = 𝐹) | 
| 268 | 267 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)(𝐹 ↾ (0..^𝑁))) = (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)𝐹)) | 
| 269 | 243, 264,
268 | 3eqtr3rd 2785 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((coe1‘𝑥) ↾ (0..^𝑁)) ∘f (
·𝑠 ‘𝑃)𝐹) = ((𝑖 ∈ ℕ0 ↦
(((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ↾ (0..^𝑁))) | 
| 270 | 269 | oveq2d 7448 | . . . . . . . . 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 22303 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑃)) → 𝑥 = (𝑃 Σg (𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) | 
| 273 | 271, 166,
272 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 = (𝑃 Σg (𝑖 ∈ ℕ0
↦ (((coe1‘𝑥)‘𝑖)( ·𝑠
‘𝑃)(𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) | 
| 274 | 237, 270,
273 | 3eqtr4rd 2787 | . . . . . . . 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 3624 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))(𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ 𝑥 = (𝑃 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)))) | 
| 277 | 102, 8 | fmptd 7133 | . . . . . . . 8
⊢ (𝜑 → 𝐹:(0..^𝑁)⟶(Base‘𝑃)) | 
| 278 | 156, 33, 39, 37, 224, 38, 277, 23, 239 | ellspd 21823 | . . . . . . 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 6087 | . . . . . . . 8
⊢ (𝐹 “ dom 𝐹) = ran 𝐹 | 
| 282 | 154 | fdmd 6745 | . . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = (0..^𝑁)) | 
| 283 | 282 | imaeq2d 6077 | . . . . . . . 8
⊢ (𝜑 → (𝐹 “ dom 𝐹) = (𝐹 “ (0..^𝑁))) | 
| 284 | 281, 283 | eqtr3id 2790 | . . . . . . 7
⊢ (𝜑 → ran 𝐹 = (𝐹 “ (0..^𝑁))) | 
| 285 | 284 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁)))) | 
| 286 | 285 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝑃)‘(𝐹 “ (0..^𝑁)))) | 
| 287 | 280, 286 | eleqtrrd 2843 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ((LSpan‘𝑃)‘ran 𝐹)) | 
| 288 | 158, 287 | eqelssd 4004 | . . 3
⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = 𝑆) | 
| 289 |  | eqid 2736 | . . . . . 6
⊢
(LSpan‘𝐸) =
(LSpan‘𝐸) | 
| 290 | 44, 156, 289, 27 | lsslsp 21014 | . . . . 5
⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝐸)‘ran 𝐹) = ((LSpan‘𝑃)‘ran 𝐹)) | 
| 291 | 290 | eqcomd 2742 | . . . 4
⊢ ((𝑃 ∈ LMod ∧ 𝑆 ∈ (LSubSp‘𝑃) ∧ ran 𝐹 ⊆ 𝑆) → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹)) | 
| 292 | 23, 26, 155, 291 | syl3anc 1372 | . . 3
⊢ (𝜑 → ((LSpan‘𝑃)‘ran 𝐹) = ((LSpan‘𝐸)‘ran 𝐹)) | 
| 293 | 288, 292,
46 | 3eqtr3d 2784 | . 2
⊢ (𝜑 → ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸)) | 
| 294 |  | eqid 2736 | . . 3
⊢
(Base‘𝐸) =
(Base‘𝐸) | 
| 295 | 24 | fvexi 6919 | . . . . . . 7
⊢ 𝐷 ∈ V | 
| 296 |  | cnvexg 7947 | . . . . . . 7
⊢ (𝐷 ∈ V → ◡𝐷 ∈ V) | 
| 297 |  | imaexg 7936 | . . . . . . 7
⊢ (◡𝐷 ∈ V → (◡𝐷 “ (-∞[,)𝑁)) ∈ V) | 
| 298 | 295, 296,
297 | mp2b 10 | . . . . . 6
⊢ (◡𝐷 “ (-∞[,)𝑁)) ∈ V | 
| 299 | 25, 298 | eqeltri 2836 | . . . . 5
⊢ 𝑆 ∈ V | 
| 300 | 44, 37 | resssca 17388 | . . . . 5
⊢ (𝑆 ∈ V →
(Scalar‘𝑃) =
(Scalar‘𝐸)) | 
| 301 | 299, 300 | ax-mp 5 | . . . 4
⊢
(Scalar‘𝑃) =
(Scalar‘𝐸) | 
| 302 | 301 | fveq2i 6908 | . . 3
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝐸)) | 
| 303 |  | eqid 2736 | . . 3
⊢
(Scalar‘𝐸) =
(Scalar‘𝐸) | 
| 304 | 44, 38 | ressvsca 17389 | . . . 4
⊢ (𝑆 ∈ V → (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝐸)) | 
| 305 | 299, 304 | ax-mp 5 | . . 3
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝐸) | 
| 306 |  | eqid 2736 | . . 3
⊢
(0g‘𝐸) = (0g‘𝐸) | 
| 307 | 301 | fveq2i 6908 | . . 3
⊢
(0g‘(Scalar‘𝑃)) =
(0g‘(Scalar‘𝐸)) | 
| 308 |  | eqid 2736 | . . 3
⊢
(LBasis‘𝐸) =
(LBasis‘𝐸) | 
| 309 | 44, 27 | lsslvec 21109 | . . . . 5
⊢ ((𝑃 ∈ LVec ∧ 𝑆 ∈ (LSubSp‘𝑃)) → 𝐸 ∈ LVec) | 
| 310 | 22, 26, 309 | syl2anc 584 | . . . 4
⊢ (𝜑 → 𝐸 ∈ LVec) | 
| 311 | 310 | lveclmodd 21107 | . . 3
⊢ (𝜑 → 𝐸 ∈ LMod) | 
| 312 | 14, 5 | eqeltrrd 2841 | . . . . 5
⊢ (𝜑 → (Scalar‘𝑃) ∈
DivRing) | 
| 313 |  | drngnzr 20749 | . . . . 5
⊢
((Scalar‘𝑃)
∈ DivRing → (Scalar‘𝑃) ∈ NzRing) | 
| 314 | 312, 313 | syl 17 | . . . 4
⊢ (𝜑 → (Scalar‘𝑃) ∈
NzRing) | 
| 315 | 301, 314 | eqeltrrid 2845 | . . 3
⊢ (𝜑 → (Scalar‘𝐸) ∈
NzRing) | 
| 316 | 120 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝐸)) | 
| 317 |  | drngnzr 20749 | . . . . . . . . . 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..^𝑁)) → 𝑛 ∈ ℕ0) | 
| 321 |  | elfzonn0 13748 | . . . . . . . . 9
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ ℕ0) | 
| 322 | 321 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ ℕ0) | 
| 323 | 1, 98, 91, 319, 320, 322 | ply1moneq 33612 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ↔ 𝑛 = 𝑖)) | 
| 324 | 323 | biimpd 229 | . . . . . 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 3201 | . . . 4
⊢ (𝜑 → ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) → 𝑛 = 𝑖)) | 
| 327 |  | oveq1 7439 | . . . . 5
⊢ (𝑛 = 𝑖 → (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅))) | 
| 328 | 8, 327 | f1mpt 7282 | . . . 4
⊢ (𝐹:(0..^𝑁)–1-1→(Base‘𝐸) ↔ (∀𝑛 ∈ (0..^𝑁)(𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) ∈ (Base‘𝐸) ∧ ∀𝑛 ∈ (0..^𝑁)∀𝑖 ∈ (0..^𝑁)((𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅)) = (𝑖(.g‘(mulGrp‘𝑃))(var1‘𝑅)) → 𝑛 = 𝑖))) | 
| 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 33409 | . 2
⊢ (𝜑 → (ran 𝐹 ∈ (LBasis‘𝐸) ↔ (∀𝑎 ∈ ((Base‘(Scalar‘𝑃)) ↑m (0..^𝑁))((𝑎 finSupp
(0g‘(Scalar‘𝑃)) ∧ (𝐸 Σg (𝑎 ∘f (
·𝑠 ‘𝑃)𝐹)) = (0g‘𝐸)) → 𝑎 = ((0..^𝑁) ×
{(0g‘(Scalar‘𝑃))})) ∧ ((LSpan‘𝐸)‘ran 𝐹) = (Base‘𝐸)))) | 
| 331 | 153, 293,
330 | mpbir2and 713 | 1
⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸)) |