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 W = I Word I × 2 𝑜
efgval.r ˙ = ~ FG I
Assertion efgi1 A W N 0 A J I A ˙ A splice N N ⟨“ J 1 𝑜 J ”⟩

Proof

Step Hyp Ref Expression
1 efgval.w W = I Word I × 2 𝑜
2 efgval.r ˙ = ~ FG I
3 1oex 1 𝑜 V
4 3 prid2 1 𝑜 1 𝑜
5 df2o3 2 𝑜 = 1 𝑜
6 4 5 eleqtrri 1 𝑜 2 𝑜
7 1 2 efgi A W N 0 A J I 1 𝑜 2 𝑜 A ˙ A splice N N ⟨“ J 1 𝑜 J 1 𝑜 1 𝑜 ”⟩
8 6 7 mpanr2 A W N 0 A J I A ˙ A splice N N ⟨“ J 1 𝑜 J 1 𝑜 1 𝑜 ”⟩
9 8 3impa A W N 0 A J I A ˙ A splice N N ⟨“ J 1 𝑜 J 1 𝑜 1 𝑜 ”⟩
10 tru
11 eqidd J 1 𝑜 = J 1 𝑜
12 difid 1 𝑜 1 𝑜 =
13 12 opeq2i J 1 𝑜 1 𝑜 = J
14 13 a1i J 1 𝑜 1 𝑜 = J
15 11 14 s2eqd ⟨“ J 1 𝑜 J 1 𝑜 1 𝑜 ”⟩ = ⟨“ J 1 𝑜 J ”⟩
16 oteq3 ⟨“ J 1 𝑜 J 1 𝑜 1 𝑜 ”⟩ = ⟨“ J 1 𝑜 J ”⟩ N N ⟨“ J 1 𝑜 J 1 𝑜 1 𝑜 ”⟩ = N N ⟨“ J 1 𝑜 J ”⟩
17 10 15 16 mp2b N N ⟨“ J 1 𝑜 J 1 𝑜 1 𝑜 ”⟩ = N N ⟨“ J 1 𝑜 J ”⟩
18 17 oveq2i A splice N N ⟨“ J 1 𝑜 J 1 𝑜 1 𝑜 ”⟩ = A splice N N ⟨“ J 1 𝑜 J ”⟩
19 9 18 breqtrdi A W N 0 A J I A ˙ A splice N N ⟨“ J 1 𝑜 J ”⟩