Metamath Proof Explorer

Theorem efgtf

Description: Value of the free group construction. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypotheses efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
Assertion efgtf ( 𝑋 ∈ 𝑊 → ( ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ 𝑋 ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
3 efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
4 efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
6 1 5 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
7 simpl ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑋 ∈ 𝑊 )
8 6 7 sseldi ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑋 ∈ Word ( 𝐼 × 2o ) )
9 simprr ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑏 ∈ ( 𝐼 × 2o ) )
10 3 efgmf ⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
11 10 ffvelrni ⊢ ( 𝑏 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ 𝑏 ) ∈ ( 𝐼 × 2o ) )
12 11 ad2antll ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ‘ 𝑏 ) ∈ ( 𝐼 × 2o ) )
13 9 12 s2cld ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
14 splcl ⊢ ( ( 𝑋 ∈ Word ( 𝐼 × 2o ) ∧ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) ) → ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ∈ Word ( 𝐼 × 2o ) )
15 8 13 14 syl2anc ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ∈ Word ( 𝐼 × 2o ) )
16 1 efgrcl ⊢ ( 𝑋 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) )
17 16 simprd ⊢ ( 𝑋 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) )
18 17 adantr ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑊 = Word ( 𝐼 × 2o ) )
19 15 18 eleqtrrd ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ∈ 𝑊 )
20 19 ralrimivva ⊢ ( 𝑋 ∈ 𝑊 → ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∀ 𝑏 ∈ ( 𝐼 × 2o ) ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ∈ 𝑊 )
21 eqid ⊢ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
22 21 fmpo ⊢ ( ∀ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∀ 𝑏 ∈ ( 𝐼 × 2o ) ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ∈ 𝑊 ↔ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
23 20 22 sylib ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
24 ovex ⊢ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∈ V
25 16 simpld ⊢ ( 𝑋 ∈ 𝑊 → 𝐼 ∈ V )
26 2on ⊢ 2o ∈ On
27 xpexg ⊢ ( ( 𝐼 ∈ V ∧ 2o ∈ On ) → ( 𝐼 × 2o ) ∈ V )
28 25 26 27 sylancl ⊢ ( 𝑋 ∈ 𝑊 → ( 𝐼 × 2o ) ∈ V )
29 xpexg ⊢ ( ( ( 0 ... ( ♯ ‘ 𝑋 ) ) ∈ V ∧ ( 𝐼 × 2o ) ∈ V ) → ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ∈ V )
30 24 28 29 sylancr ⊢ ( 𝑋 ∈ 𝑊 → ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ∈ V )
31 1 fvexi ⊢ 𝑊 ∈ V
32 31 a1i ⊢ ( 𝑋 ∈ 𝑊 → 𝑊 ∈ V )
33 fex2 ⊢ ( ( ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ∧ ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ∈ V ∧ 𝑊 ∈ V ) → ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∈ V )
34 23 30 32 33 syl3anc ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∈ V )
35 fveq2 ⊢ ( 𝑢 = 𝑋 → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ 𝑋 ) )
36 35 oveq2d ⊢ ( 𝑢 = 𝑋 → ( 0 ... ( ♯ ‘ 𝑢 ) ) = ( 0 ... ( ♯ ‘ 𝑋 ) ) )
37 eqidd ⊢ ( 𝑢 = 𝑋 → ( 𝐼 × 2o ) = ( 𝐼 × 2o ) )
38 oveq1 ⊢ ( 𝑢 = 𝑋 → ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) = ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
39 36 37 38 mpoeq123dv ⊢ ( 𝑢 = 𝑋 → ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
40 oteq1 ⊢ ( 𝑛 = 𝑎 → ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ = ⟨ 𝑎 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ )
41 oteq2 ⊢ ( 𝑛 = 𝑎 → ⟨ 𝑎 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ = ⟨ 𝑎 , 𝑎 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ )
42 40 41 eqtrd ⊢ ( 𝑛 = 𝑎 → ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ = ⟨ 𝑎 , 𝑎 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ )
43 42 oveq2d ⊢ ( 𝑛 = 𝑎 → ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) = ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) )
44 id ⊢ ( 𝑤 = 𝑏 → 𝑤 = 𝑏 )
45 fveq2 ⊢ ( 𝑤 = 𝑏 → ( 𝑀 ‘ 𝑤 ) = ( 𝑀 ‘ 𝑏 ) )
46 44 45 s2eqd ⊢ ( 𝑤 = 𝑏 → ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ )
47 46 oteq3d ⊢ ( 𝑤 = 𝑏 → ⟨ 𝑎 , 𝑎 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ = ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ )
48 47 oveq2d ⊢ ( 𝑤 = 𝑏 → ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) = ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
49 43 48 cbvmpov ⊢ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
50 fveq2 ⊢ ( 𝑣 = 𝑢 → ( ♯ ‘ 𝑣 ) = ( ♯ ‘ 𝑢 ) )
51 50 oveq2d ⊢ ( 𝑣 = 𝑢 → ( 0 ... ( ♯ ‘ 𝑣 ) ) = ( 0 ... ( ♯ ‘ 𝑢 ) ) )
52 eqidd ⊢ ( 𝑣 = 𝑢 → ( 𝐼 × 2o ) = ( 𝐼 × 2o ) )
53 oveq1 ⊢ ( 𝑣 = 𝑢 → ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) = ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
54 51 52 53 mpoeq123dv ⊢ ( 𝑣 = 𝑢 → ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
55 49 54 syl5eq ⊢ ( 𝑣 = 𝑢 → ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
56 55 cbvmptv ⊢ ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) ) = ( 𝑢 ∈ 𝑊 ↦ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
57 4 56 eqtri ⊢ 𝑇 = ( 𝑢 ∈ 𝑊 ↦ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
58 39 57 fvmptg ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∈ V ) → ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
59 34 58 mpdan ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
60 59 feq1d ⊢ ( 𝑋 ∈ 𝑊 → ( ( 𝑇 ‘ 𝑋 ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ↔ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
61 23 60 mpbird ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑇 ‘ 𝑋 ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
62 59 61 jca ⊢ ( 𝑋 ∈ 𝑊 → ( ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ 𝑋 ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )