Metamath Proof Explorer


Theorem isubgr3stgr

Description: If a vertex of a simple graph has exactly N (different) neighbors, and none of these neighbors are connected by an edge, then the (closed) neighborhood of this vertex induces a subgraph which is isomorphic to an N-star. (Contributed by AV, 29-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v 𝑉 = ( Vtx ‘ 𝐺 )
isubgr3stgr.u 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
isubgr3stgr.c 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
isubgr3stgr.n 𝑁 ∈ ℕ0
isubgr3stgr.s 𝑆 = ( StarGr ‘ 𝑁 )
isubgr3stgr.w 𝑊 = ( Vtx ‘ 𝑆 )
isubgr3stgr.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion isubgr3stgr ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) → ( ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) → ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 isubgr3stgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgr3stgr.u 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
3 isubgr3stgr.c 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
4 isubgr3stgr.n 𝑁 ∈ ℕ0
5 isubgr3stgr.s 𝑆 = ( StarGr ‘ 𝑁 )
6 isubgr3stgr.w 𝑊 = ( Vtx ‘ 𝑆 )
7 isubgr3stgr.e 𝐸 = ( Edg ‘ 𝐺 )
8 simpl ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) → 𝐺 ∈ USGraph )
9 simpr ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) → 𝑋𝑉 )
10 simpl ( ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) → ( ♯ ‘ 𝑈 ) = 𝑁 )
11 1 2 3 4 5 6 isubgr3stgrlem3 ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ∃ 𝑓 ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) )
12 8 9 10 11 syl2an3an ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ∃ 𝑓 ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) )
13 1 clnbgrssvtx ( 𝐺 ClNeighbVtx 𝑋 ) ⊆ 𝑉
14 3 13 eqsstri 𝐶𝑉
15 14 a1i ( 𝑋𝑉𝐶𝑉 )
16 15 anim2i ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) → ( 𝐺 ∈ USGraph ∧ 𝐶𝑉 ) )
17 16 adantr ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( 𝐺 ∈ USGraph ∧ 𝐶𝑉 ) )
18 1 isubgrvtx ( ( 𝐺 ∈ USGraph ∧ 𝐶𝑉 ) → ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) = 𝐶 )
19 17 18 syl ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) = 𝐶 )
20 19 eqcomd ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → 𝐶 = ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) )
21 20 f1oeq2d ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( 𝑓 : 𝐶1-1-onto𝑊𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 ) )
22 21 biimpd ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( 𝑓 : 𝐶1-1-onto𝑊𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 ) )
23 22 adantrd ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) → 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 ) )
24 23 imp ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) ) → 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 )
25 fvexd ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) ) → ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ∈ V )
26 25 mptexd ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) ) → ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) ∈ V )
27 eqid ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) )
28 eqid ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) )
29 1 2 3 4 5 6 7 27 28 isubgr3stgrlem9 ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) ) → ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) ‘ 𝑒 ) ) )
30 f1oeq1 ( 𝑔 = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) → ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ↔ ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) )
31 fveq1 ( 𝑔 = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) → ( 𝑔𝑒 ) = ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) ‘ 𝑒 ) )
32 31 eqeq2d ( 𝑔 = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) → ( ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ↔ ( 𝑓𝑒 ) = ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) ‘ 𝑒 ) ) )
33 32 ralbidv ( 𝑔 = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) → ( ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ↔ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) ‘ 𝑒 ) ) )
34 30 33 anbi12d ( 𝑔 = ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) → ( ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ↔ ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( ( 𝑖 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ↦ ( 𝑓𝑖 ) ) ‘ 𝑒 ) ) ) )
35 26 29 34 spcedv ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) ) → ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) )
36 24 35 jca ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) ) → ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) )
37 36 ex ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) → ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ) )
38 37 eximdv ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( ∃ 𝑓 ( 𝑓 : 𝐶1-1-onto𝑊 ∧ ( 𝑓𝑋 ) = 0 ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ) )
39 12 38 mpd ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) )
40 1 isubgrusgr ( ( 𝐺 ∈ USGraph ∧ 𝐶𝑉 ) → ( 𝐺 ISubGr 𝐶 ) ∈ USGraph )
41 16 40 syl ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) → ( 𝐺 ISubGr 𝐶 ) ∈ USGraph )
42 usgruspgr ( ( 𝐺 ISubGr 𝐶 ) ∈ USGraph → ( 𝐺 ISubGr 𝐶 ) ∈ USPGraph )
43 uspgrushgr ( ( 𝐺 ISubGr 𝐶 ) ∈ USPGraph → ( 𝐺 ISubGr 𝐶 ) ∈ USHGraph )
44 41 42 43 3syl ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) → ( 𝐺 ISubGr 𝐶 ) ∈ USHGraph )
45 stgrusgra ( 𝑁 ∈ ℕ0 → ( StarGr ‘ 𝑁 ) ∈ USGraph )
46 usgruspgr ( ( StarGr ‘ 𝑁 ) ∈ USGraph → ( StarGr ‘ 𝑁 ) ∈ USPGraph )
47 uspgrushgr ( ( StarGr ‘ 𝑁 ) ∈ USPGraph → ( StarGr ‘ 𝑁 ) ∈ USHGraph )
48 45 46 47 3syl ( 𝑁 ∈ ℕ0 → ( StarGr ‘ 𝑁 ) ∈ USHGraph )
49 4 48 ax-mp ( StarGr ‘ 𝑁 ) ∈ USHGraph
50 eqid ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) = ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) )
51 5 fveq2i ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
52 6 51 eqtri 𝑊 = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
53 eqid ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = ( Edg ‘ ( StarGr ‘ 𝑁 ) )
54 50 52 27 53 gricushgr ( ( ( 𝐺 ISubGr 𝐶 ) ∈ USHGraph ∧ ( StarGr ‘ 𝑁 ) ∈ USHGraph ) → ( ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ) )
55 44 49 54 sylancl ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) → ( ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ) )
56 55 adantr ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) ) ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ) )
57 39 56 mpbird ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) )
58 57 ex ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) → ( ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) → ( 𝐺 ISubGr 𝐶 ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )