This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efgi1

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

Ref Expression
Hypotheses efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
Assertion efgi1 ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝐽 ∈ 𝐼 ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ ⟩ ) )

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
3 1oex ⊢ 1o ∈ V
4 3 prid2 ⊢ 1o ∈ { ∅ , 1o }
5 df2o3 ⊢ 2o = { ∅ , 1o }
6 4 5 eleqtrri ⊢ 1o ∈ 2o
7 1 2 efgi ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽 ∈ 𝐼 ∧ 1o ∈ 2o ) ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ ) )
8 6 7 mpanr2 ⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝐽 ∈ 𝐼 ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ ) )
9 8 3impa ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝐽 ∈ 𝐼 ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ ) )
10 tru ⊢ ⊤
11 eqidd ⊢ ( ⊤ → ⟨ 𝐽 , 1o ⟩ = ⟨ 𝐽 , 1o ⟩ )
12 difid ⊢ ( 1o ∖ 1o ) = ∅
13 12 opeq2i ⊢ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ = ⟨ 𝐽 , ∅ ⟩
14 13 a1i ⊢ ( ⊤ → ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ = ⟨ 𝐽 , ∅ ⟩ )
15 11 14 s2eqd ⊢ ( ⊤ → ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ = ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ )
16 oteq3 ⊢ ( ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ = ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ → ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ ⟩ )
17 10 15 16 mp2b ⊢ ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ ⟩
18 17 oveq2i ⊢ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ ) = ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ ⟩ )
19 9 18 breqtrdi ⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝐽 ∈ 𝐼 ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ ⟩ ) )