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		1oelpr	⊢ 1o ∈ { ∅ , 1o }
4		df2o3	⊢ 2o = { ∅ , 1o }
5	3 4	eleqtrri	⊢ 1o ∈ 2o
6	1 2	efgi	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ ( 𝐽 ∈ 𝐼 ∧ 1o ∈ 2o ) ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ ) )
7	5 6	mpanr2	⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝐽 ∈ 𝐼 ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ ) )
8	7	3impa	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝐽 ∈ 𝐼 ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ ) )
9		tru	⊢ ⊤
10		eqidd	⊢ ( ⊤ → ⟨ 𝐽 , 1o ⟩ = ⟨ 𝐽 , 1o ⟩ )
11		difid	⊢ ( 1o ∖ 1o ) = ∅
12	11	opeq2i	⊢ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ = ⟨ 𝐽 , ∅ ⟩
13	12	a1i	⊢ ( ⊤ → ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ = ⟨ 𝐽 , ∅ ⟩ )
14	10 13	s2eqd	⊢ ( ⊤ → ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ = ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ )
15		oteq3	⊢ ( ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ = ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ → ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ ⟩ )
16	9 14 15	mp2b	⊢ ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ ⟩
17	16	oveq2i	⊢ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ( 1o ∖ 1o ) ⟩ ”⟩ ⟩ ) = ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ ⟩ )
18	8 17	breqtrdi	⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ∧ 𝐽 ∈ 𝐼 ) → 𝐴 ∼ ( 𝐴 splice ⟨ 𝑁 , 𝑁 , ⟨“ ⟨ 𝐽 , 1o ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ ⟩ ) )