Metamath Proof Explorer

Theorem isubgr3stgrlem8

Description: Lemma 8 for isubgr3stgr . (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 ‘ 𝐺 )
isubgr3stgr.i ⊢ 𝐼 = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) )
isubgr3stgr.h ⊢ 𝐻 = ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) )
Assertion isubgr3stgrlem8 ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐻 : 𝐼 –1-1-onto→ ( Edg ‘ ( 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 isubgr3stgr.i ⊢ 𝐼 = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) )
9 isubgr3stgr.h ⊢ 𝐻 = ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) )
10 imaeq2 ⊢ ( 𝑖 = 𝑘 → ( 𝐹 “ 𝑖 ) = ( 𝐹 “ 𝑘 ) )
11 10 cbvmptv ⊢ ( 𝑖 ∈ 𝐼 ↦ ( 𝐹 “ 𝑖 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 “ 𝑘 ) )
12 9 11 eqtri ⊢ 𝐻 = ( 𝑘 ∈ 𝐼 ↦ ( 𝐹 “ 𝑘 ) )
13 f1of ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → 𝐹 : 𝐶 ⟶ 𝑊 )
14 13 ad2antrl ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐹 : 𝐶 ⟶ 𝑊 )
15 1 2 3 4 5 6 7 8 9 isubgr3stgrlem5 ⊢ ( ( 𝐹 : 𝐶 ⟶ 𝑊 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 “ 𝑘 ) )
16 14 15 sylan ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑘 ) = ( 𝐹 “ 𝑘 ) )
17 1 2 3 4 5 6 7 8 9 isubgr3stgrlem6 ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐻 : 𝐼 ⟶ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )
18 17 ffvelcdmda ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐻 ‘ 𝑘 ) ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )
19 16 18 eqeltrrd ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 “ 𝑘 ) ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )
20 1 2 3 4 5 6 7 8 9 isubgr3stgrlem7 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( ◡ 𝐹 “ 𝑗 ) ∈ 𝐼 )
21 20 ad4ant134 ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( ◡ 𝐹 “ 𝑗 ) ∈ 𝐼 )
22 f1ofo ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → 𝐹 : 𝐶 –onto→ 𝑊 )
23 22 ad2antrl ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐹 : 𝐶 –onto→ 𝑊 )
24 stgrusgra ⊢ ( 𝑁 ∈ ℕ0 → ( StarGr ‘ 𝑁 ) ∈ USGraph )
25 4 24 mp1i ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( StarGr ‘ 𝑁 ) ∈ USGraph )
26 simpr ⊢ ( ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )
27 5 fveq2i ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
28 6 27 eqtri ⊢ 𝑊 = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
29 eqid ⊢ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = ( Edg ‘ ( StarGr ‘ 𝑁 ) )
30 28 29 edgssv2 ⊢ ( ( ( StarGr ‘ 𝑁 ) ∈ USGraph ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( 𝑗 ⊆ 𝑊 ∧ ( ♯ ‘ 𝑗 ) = 2 ) )
31 30 simpld ⊢ ( ( ( StarGr ‘ 𝑁 ) ∈ USGraph ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → 𝑗 ⊆ 𝑊 )
32 25 26 31 syl2an ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → 𝑗 ⊆ 𝑊 )
33 foimacnv ⊢ ( ( 𝐹 : 𝐶 –onto→ 𝑊 ∧ 𝑗 ⊆ 𝑊 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑗 ) ) = 𝑗 )
34 23 32 33 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑗 ) ) = 𝑗 )
35 imaeq2 ⊢ ( 𝑘 = ( ◡ 𝐹 “ 𝑗 ) → ( 𝐹 “ 𝑘 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑗 ) ) )
36 35 eqcomd ⊢ ( 𝑘 = ( ◡ 𝐹 “ 𝑗 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑗 ) ) = ( 𝐹 “ 𝑘 ) )
37 34 36 sylan9req ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) ∧ 𝑘 = ( ◡ 𝐹 “ 𝑗 ) ) → 𝑗 = ( 𝐹 “ 𝑘 ) )
38 imaeq2 ⊢ ( 𝑗 = ( 𝐹 “ 𝑘 ) → ( ◡ 𝐹 “ 𝑗 ) = ( ◡ 𝐹 “ ( 𝐹 “ 𝑘 ) ) )
39 f1of1 ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 → 𝐹 : 𝐶 –1-1→ 𝑊 )
40 39 ad2antrl ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐹 : 𝐶 –1-1→ 𝑊 )
41 usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
42 41 ad2antrr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → 𝐺 ∈ UHGraph )
43 1 clnbgrssvtx ⊢ ( 𝐺 ClNeighbVtx 𝑋 ) ⊆ 𝑉
44 3 43 eqsstri ⊢ 𝐶 ⊆ 𝑉
45 44 a1i ⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) → 𝐶 ⊆ 𝑉 )
46 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
47 eqid ⊢ ( 𝐺 ISubGr 𝐶 ) = ( 𝐺 ISubGr 𝐶 )
48 1 46 47 8 isubgredg ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐶 ⊆ 𝑉 ) → ( 𝑘 ∈ 𝐼 ↔ ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘 ⊆ 𝐶 ) ) )
49 42 45 48 syl2an ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( 𝑘 ∈ 𝐼 ↔ ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘 ⊆ 𝐶 ) ) )
50 simpr ⊢ ( ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘 ⊆ 𝐶 ) → 𝑘 ⊆ 𝐶 )
51 50 a1d ⊢ ( ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘 ⊆ 𝐶 ) → ( 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) → 𝑘 ⊆ 𝐶 ) )
52 49 51 biimtrdi ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → ( 𝑘 ∈ 𝐼 → ( 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) → 𝑘 ⊆ 𝐶 ) ) )
53 52 imp32 ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → 𝑘 ⊆ 𝐶 )
54 f1imacnv ⊢ ( ( 𝐹 : 𝐶 –1-1→ 𝑊 ∧ 𝑘 ⊆ 𝐶 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑘 ) ) = 𝑘 )
55 40 53 54 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑘 ) ) = 𝑘 )
56 38 55 sylan9eqr ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) ∧ 𝑗 = ( 𝐹 “ 𝑘 ) ) → ( ◡ 𝐹 “ 𝑗 ) = 𝑘 )
57 56 eqcomd ⊢ ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) ∧ 𝑗 = ( 𝐹 “ 𝑘 ) ) → 𝑘 = ( ◡ 𝐹 “ 𝑗 ) )
58 37 57 impbida ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) ∧ ( 𝑘 ∈ 𝐼 ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → ( 𝑘 = ( ◡ 𝐹 “ 𝑗 ) ↔ 𝑗 = ( 𝐹 “ 𝑘 ) ) )
59 12 19 21 58 f1o2d ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝐹 ‘ 𝑋 ) = 0 ) ) → 𝐻 : 𝐼 –1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )