Metamath Proof Explorer

Theorem efgtlen

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 efgtlen ( ( 𝑋 ∈ 𝑊 ∧ 𝐴 ∈ ran ( 𝑇 ‘ 𝑋 ) ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ 𝑋 ) + 2 ) )

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 1 2 3 4 efgtf ⊢ ( 𝑋 ∈ 𝑊 → ( ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ 𝑋 ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
6 5 simpld ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
7 6 rneqd ⊢ ( 𝑋 ∈ 𝑊 → ran ( 𝑇 ‘ 𝑋 ) = ran ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
8 7 eleq2d ⊢ ( 𝑋 ∈ 𝑊 → ( 𝐴 ∈ ran ( 𝑇 ‘ 𝑋 ) ↔ 𝐴 ∈ ran ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ) )
9 eqid ⊢ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
10 ovex ⊢ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ∈ V
11 9 10 elrnmpo ⊢ ( 𝐴 ∈ ran ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ↔ ∃ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∃ 𝑏 ∈ ( 𝐼 × 2o ) 𝐴 = ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
12 8 11 bitrdi ⊢ ( 𝑋 ∈ 𝑊 → ( 𝐴 ∈ ran ( 𝑇 ‘ 𝑋 ) ↔ ∃ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∃ 𝑏 ∈ ( 𝐼 × 2o ) 𝐴 = ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
13 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
14 1 13 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
15 simpl ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑋 ∈ 𝑊 )
16 14 15 sseldi ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑋 ∈ Word ( 𝐼 × 2o ) )
17 elfzuz ⊢ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) → 𝑎 ∈ ( ℤ≥ ‘ 0 ) )
18 17 ad2antrl ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 ∈ ( ℤ≥ ‘ 0 ) )
19 eluzfz2b ⊢ ( 𝑎 ∈ ( ℤ≥ ‘ 0 ) ↔ 𝑎 ∈ ( 0 ... 𝑎 ) )
20 18 19 sylib ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 ∈ ( 0 ... 𝑎 ) )
21 simprl ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) )
22 simprr ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑏 ∈ ( 𝐼 × 2o ) )
23 3 efgmf ⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o )
24 23 ffvelrni ⊢ ( 𝑏 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ 𝑏 ) ∈ ( 𝐼 × 2o ) )
25 22 24 syl ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ‘ 𝑏 ) ∈ ( 𝐼 × 2o ) )
26 22 25 s2cld ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ∈ Word ( 𝐼 × 2o ) )
27 16 20 21 26 spllen ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( ( ♯ ‘ 𝑋 ) + ( ( ♯ ‘ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) − ( 𝑎 − 𝑎 ) ) ) )
28 s2len ⊢ ( ♯ ‘ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) = 2
29 28 a1i ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) = 2 )
30 eluzelcn ⊢ ( 𝑎 ∈ ( ℤ≥ ‘ 0 ) → 𝑎 ∈ ℂ )
31 18 30 syl ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → 𝑎 ∈ ℂ )
32 31 subidd ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑎 − 𝑎 ) = 0 )
33 29 32 oveq12d ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) − ( 𝑎 − 𝑎 ) ) = ( 2 − 0 ) )
34 2cn ⊢ 2 ∈ ℂ
35 34 subid1i ⊢ ( 2 − 0 ) = 2
36 33 35 eqtrdi ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) − ( 𝑎 − 𝑎 ) ) = 2 )
37 36 oveq2d ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝑋 ) + ( ( ♯ ‘ ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ) − ( 𝑎 − 𝑎 ) ) ) = ( ( ♯ ‘ 𝑋 ) + 2 ) )
38 27 37 eqtrd ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( ( ♯ ‘ 𝑋 ) + 2 ) )
39 fveqeq2 ⊢ ( 𝐴 = ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) → ( ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ 𝑋 ) + 2 ) ↔ ( ♯ ‘ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( ( ♯ ‘ 𝑋 ) + 2 ) ) )
40 38 39 syl5ibrcom ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝑏 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 = ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ 𝑋 ) + 2 ) ) )
41 40 rexlimdvva ⊢ ( 𝑋 ∈ 𝑊 → ( ∃ 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∃ 𝑏 ∈ ( 𝐼 × 2o ) 𝐴 = ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ 𝑋 ) + 2 ) ) )
42 12 41 sylbid ⊢ ( 𝑋 ∈ 𝑊 → ( 𝐴 ∈ ran ( 𝑇 ‘ 𝑋 ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ 𝑋 ) + 2 ) ) )
43 42 imp ⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝐴 ∈ ran ( 𝑇 ‘ 𝑋 ) ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ 𝑋 ) + 2 ) )