This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1degltdim

Description: The space S of the univariate polynomials of degree less than N has dimension N . (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses ply1degltdim.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1degltdim.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
ply1degltdim.s ⊢ 𝑆 = ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) )
ply1degltdim.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
ply1degltdim.r ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
ply1degltdim.e ⊢ 𝐸 = ( 𝑃 ↾s 𝑆 )
Assertion ply1degltdim ( 𝜑 → ( dim ‘ 𝐸 ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 ply1degltdim.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1degltdim.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3 ply1degltdim.s ⊢ 𝑆 = ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) )
4 ply1degltdim.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 ply1degltdim.r ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
6 ply1degltdim.e ⊢ 𝐸 = ( 𝑃 ↾s 𝑆 )
7 1 5 ply1lvec ⊢ ( 𝜑 → 𝑃 ∈ LVec )
8 5 drngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
9 1 2 3 4 8 ply1degltlss ⊢ ( 𝜑 → 𝑆 ∈ ( LSubSp ‘ 𝑃 ) )
10 eqid ⊢ ( LSubSp ‘ 𝑃 ) = ( LSubSp ‘ 𝑃 )
11 6 10 lsslvec ⊢ ( ( 𝑃 ∈ LVec ∧ 𝑆 ∈ ( LSubSp ‘ 𝑃 ) ) → 𝐸 ∈ LVec )
12 7 9 11 syl2anc ⊢ ( 𝜑 → 𝐸 ∈ LVec )
13 oveq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
14 13 cbvmptv ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
15 1 2 3 4 5 6 14 ply1degltdimlem ⊢ ( 𝜑 → ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ( LBasis ‘ 𝐸 ) )
16 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
17 2 1 16 deg1xrf ⊢ 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ*
18 ffn ⊢ ( 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ* → 𝐷 Fn ( Base ‘ 𝑃 ) )
19 17 18 mp1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝐷 Fn ( Base ‘ 𝑃 ) )
20 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
21 20 16 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
22 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
23 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
24 20 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
25 8 23 24 3syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
27 elfzonn0 ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 ∈ ℕ0 )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℕ0 )
29 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
30 29 1 16 vr1cl ⊢ ( 𝑅 ∈ Ring → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
31 8 30 syl ⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ 𝑃 ) )
33 21 22 26 28 32 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
34 mnfxr ⊢ -∞ ∈ ℝ*
35 34 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → -∞ ∈ ℝ* )
36 4 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
37 36 rexrd ⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ* )
39 2 1 16 deg1xrcl ⊢ ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ℝ* )
40 33 39 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ℝ* )
41 40 mnfled ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → -∞ ≤ ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
42 27 nn0red ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 ∈ ℝ )
43 42 rexrd ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 ∈ ℝ* )
44 43 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℝ* )
45 2 1 29 20 22 deg1pwle ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑛 ∈ ℕ0 ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ≤ 𝑛 )
46 8 27 45 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ≤ 𝑛 )
47 elfzolt2 ⊢ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) → 𝑛 < 𝑁 )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 < 𝑁 )
49 40 44 38 46 48 xrlelttrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) < 𝑁 )
50 35 38 40 41 49 elicod ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ( -∞ [,) 𝑁 ) )
51 19 33 50 elpreimad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
52 51 3 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ 𝑆 )
53 16 10 lssss ⊢ ( 𝑆 ∈ ( LSubSp ‘ 𝑃 ) → 𝑆 ⊆ ( Base ‘ 𝑃 ) )
54 6 16 ressbas2 ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑃 ) → 𝑆 = ( Base ‘ 𝐸 ) )
55 9 53 54 3syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐸 ) )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → 𝑆 = ( Base ‘ 𝐸 ) )
57 52 56 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐸 ) )
58 57 14 fmptd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) : ( 0 ..^ 𝑁 ) ⟶ ( Base ‘ 𝐸 ) )
59 58 ffnd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) Fn ( 0 ..^ 𝑁 ) )
60 hashfn ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) Fn ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
61 59 60 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
62 ovexd ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ V )
63 57 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐸 ) )
64 drngnzr ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
65 5 64 syl ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
66 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑅 ∈ NzRing )
67 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑛 ∈ ℕ0 )
68 elfzonn0 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑁 ) → 𝑖 ∈ ℕ0 )
69 68 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ℕ0 )
70 1 29 22 66 67 69 ply1moneq ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ↔ 𝑛 = 𝑖 ) )
71 70 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) )
72 71 anasss ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) ) → ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) )
73 72 ralrimivva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) )
74 oveq1 ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
75 14 74 f1mpt ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) : ( 0 ..^ 𝑁 ) –1-1→ ( Base ‘ 𝐸 ) ↔ ( ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐸 ) ∧ ∀ 𝑛 ∈ ( 0 ..^ 𝑁 ) ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) → 𝑛 = 𝑖 ) ) )
76 63 73 75 sylanbrc ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) : ( 0 ..^ 𝑁 ) –1-1→ ( Base ‘ 𝐸 ) )
77 hashf1rn ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ V ∧ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) : ( 0 ..^ 𝑁 ) –1-1→ ( Base ‘ 𝐸 ) ) → ( ♯ ‘ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( ♯ ‘ ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
78 62 76 77 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = ( ♯ ‘ ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
79 hashfzo0 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
80 4 79 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
81 61 78 80 3eqtr3d ⊢ ( 𝜑 → ( ♯ ‘ ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = 𝑁 )
82 hashvnfin ⊢ ( ( ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ( LBasis ‘ 𝐸 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = 𝑁 → ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ Fin ) )
83 82 imp ⊢ ( ( ( ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ( LBasis ‘ 𝐸 ) ∧ 𝑁 ∈ ℕ0 ) ∧ ( ♯ ‘ ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) = 𝑁 ) → ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ Fin )
84 15 4 81 83 syl21anc ⊢ ( 𝜑 → ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ Fin )
85 eqid ⊢ ( LBasis ‘ 𝐸 ) = ( LBasis ‘ 𝐸 )
86 85 dimvalfi ⊢ ( ( 𝐸 ∈ LVec ∧ ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ( LBasis ‘ 𝐸 ) ∧ ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ Fin ) → ( dim ‘ 𝐸 ) = ( ♯ ‘ ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
87 12 15 84 86 syl3anc ⊢ ( 𝜑 → ( dim ‘ 𝐸 ) = ( ♯ ‘ ran ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
88 87 81 eqtrd ⊢ ( 𝜑 → ( dim ‘ 𝐸 ) = 𝑁 )