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 ⟩ ⟨ 𝐽 , ∅ ⟩ ”⟩ ⟩ ) )