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 sselid ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 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 23 30 fexd ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∈ V )
32 fveq2 ⊢ ( 𝑢 = 𝑋 → ( ♯ ‘ 𝑢 ) = ( ♯ ‘ 𝑋 ) )
33 32 oveq2d ⊢ ( 𝑢 = 𝑋 → ( 0 ... ( ♯ ‘ 𝑢 ) ) = ( 0 ... ( ♯ ‘ 𝑋 ) ) )
34 eqidd ⊢ ( 𝑢 = 𝑋 → ( 𝐼 × 2o ) = ( 𝐼 × 2o ) )
35 oveq1 ⊢ ( 𝑢 = 𝑋 → ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) = ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
36 33 34 35 mpoeq123dv ⊢ ( 𝑢 = 𝑋 → ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
37 oteq1 ⊢ ( 𝑛 = 𝑎 → ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ = ⟨ 𝑎 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ )
38 oteq2 ⊢ ( 𝑛 = 𝑎 → ⟨ 𝑎 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ = ⟨ 𝑎 , 𝑎 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ )
39 37 38 eqtrd ⊢ ( 𝑛 = 𝑎 → ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ = ⟨ 𝑎 , 𝑎 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ )
40 39 oveq2d ⊢ ( 𝑛 = 𝑎 → ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) = ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) )
41 id ⊢ ( 𝑤 = 𝑏 → 𝑤 = 𝑏 )
42 fveq2 ⊢ ( 𝑤 = 𝑏 → ( 𝑀 ‘ 𝑤 ) = ( 𝑀 ‘ 𝑏 ) )
43 41 42 s2eqd ⊢ ( 𝑤 = 𝑏 → ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ = ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ )
44 43 oteq3d ⊢ ( 𝑤 = 𝑏 → ⟨ 𝑎 , 𝑎 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ = ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ )
45 44 oveq2d ⊢ ( 𝑤 = 𝑏 → ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) = ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
46 40 45 cbvmpov ⊢ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
47 fveq2 ⊢ ( 𝑣 = 𝑢 → ( ♯ ‘ 𝑣 ) = ( ♯ ‘ 𝑢 ) )
48 47 oveq2d ⊢ ( 𝑣 = 𝑢 → ( 0 ... ( ♯ ‘ 𝑣 ) ) = ( 0 ... ( ♯ ‘ 𝑢 ) ) )
49 eqidd ⊢ ( 𝑣 = 𝑢 → ( 𝐼 × 2o ) = ( 𝐼 × 2o ) )
50 oveq1 ⊢ ( 𝑣 = 𝑢 → ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) = ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
51 48 49 50 mpoeq123dv ⊢ ( 𝑣 = 𝑢 → ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
52 46 51 syl5eq ⊢ ( 𝑣 = 𝑢 → ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
53 52 cbvmptv ⊢ ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) ) = ( 𝑢 ∈ 𝑊 ↦ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
54 4 53 eqtri ⊢ 𝑇 = ( 𝑢 ∈ 𝑊 ↦ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑢 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑢 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
55 36 54 fvmptg ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∈ V ) → ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
56 31 55 mpdan ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
57 56 feq1d ⊢ ( 𝑋 ∈ 𝑊 → ( ( 𝑇 ‘ 𝑋 ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ↔ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
58 23 57 mpbird ⊢ ( 𝑋 ∈ 𝑊 → ( 𝑇 ‘ 𝑋 ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 )
59 56 58 jca ⊢ ( 𝑋 ∈ 𝑊 → ( ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ 𝑋 ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )