Metamath Proof Explorer


Theorem efgi

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 efgi A W N 0 A J I K 2 𝑜 A ˙ A splice N N ⟨“ J K J 1 𝑜 K ”⟩

Proof

Step Hyp Ref Expression
1 efgval.w W = I Word I × 2 𝑜
2 efgval.r ˙ = ~ FG I
3 fveq2 u = A u = A
4 3 oveq2d u = A 0 u = 0 A
5 id u = A u = A
6 oveq1 u = A u splice i i ⟨“ a b a 1 𝑜 b ”⟩ = A splice i i ⟨“ a b a 1 𝑜 b ”⟩
7 5 6 breq12d u = A u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩ A r A splice i i ⟨“ a b a 1 𝑜 b ”⟩
8 7 2ralbidv u = A a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩ a I b 2 𝑜 A r A splice i i ⟨“ a b a 1 𝑜 b ”⟩
9 4 8 raleqbidv u = A i 0 u a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩ i 0 A a I b 2 𝑜 A r A splice i i ⟨“ a b a 1 𝑜 b ”⟩
10 9 rspcv A W u W i 0 u a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩ i 0 A a I b 2 𝑜 A r A splice i i ⟨“ a b a 1 𝑜 b ”⟩
11 oteq1 i = N i i ⟨“ a b a 1 𝑜 b ”⟩ = N i ⟨“ a b a 1 𝑜 b ”⟩
12 oteq2 i = N N i ⟨“ a b a 1 𝑜 b ”⟩ = N N ⟨“ a b a 1 𝑜 b ”⟩
13 11 12 eqtrd i = N i i ⟨“ a b a 1 𝑜 b ”⟩ = N N ⟨“ a b a 1 𝑜 b ”⟩
14 13 oveq2d i = N A splice i i ⟨“ a b a 1 𝑜 b ”⟩ = A splice N N ⟨“ a b a 1 𝑜 b ”⟩
15 14 breq2d i = N A r A splice i i ⟨“ a b a 1 𝑜 b ”⟩ A r A splice N N ⟨“ a b a 1 𝑜 b ”⟩
16 15 2ralbidv i = N a I b 2 𝑜 A r A splice i i ⟨“ a b a 1 𝑜 b ”⟩ a I b 2 𝑜 A r A splice N N ⟨“ a b a 1 𝑜 b ”⟩
17 16 rspcv N 0 A i 0 A a I b 2 𝑜 A r A splice i i ⟨“ a b a 1 𝑜 b ”⟩ a I b 2 𝑜 A r A splice N N ⟨“ a b a 1 𝑜 b ”⟩
18 10 17 sylan9 A W N 0 A u W i 0 u a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩ a I b 2 𝑜 A r A splice N N ⟨“ a b a 1 𝑜 b ”⟩
19 opeq1 a = J a b = J b
20 opeq1 a = J a 1 𝑜 b = J 1 𝑜 b
21 19 20 s2eqd a = J ⟨“ a b a 1 𝑜 b ”⟩ = ⟨“ J b J 1 𝑜 b ”⟩
22 21 oteq3d a = J N N ⟨“ a b a 1 𝑜 b ”⟩ = N N ⟨“ J b J 1 𝑜 b ”⟩
23 22 oveq2d a = J A splice N N ⟨“ a b a 1 𝑜 b ”⟩ = A splice N N ⟨“ J b J 1 𝑜 b ”⟩
24 23 breq2d a = J A r A splice N N ⟨“ a b a 1 𝑜 b ”⟩ A r A splice N N ⟨“ J b J 1 𝑜 b ”⟩
25 opeq2 b = K J b = J K
26 difeq2 b = K 1 𝑜 b = 1 𝑜 K
27 26 opeq2d b = K J 1 𝑜 b = J 1 𝑜 K
28 25 27 s2eqd b = K ⟨“ J b J 1 𝑜 b ”⟩ = ⟨“ J K J 1 𝑜 K ”⟩
29 28 oteq3d b = K N N ⟨“ J b J 1 𝑜 b ”⟩ = N N ⟨“ J K J 1 𝑜 K ”⟩
30 29 oveq2d b = K A splice N N ⟨“ J b J 1 𝑜 b ”⟩ = A splice N N ⟨“ J K J 1 𝑜 K ”⟩
31 30 breq2d b = K A r A splice N N ⟨“ J b J 1 𝑜 b ”⟩ A r A splice N N ⟨“ J K J 1 𝑜 K ”⟩
32 df-br A r A splice N N ⟨“ J K J 1 𝑜 K ”⟩ A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ r
33 31 32 bitrdi b = K A r A splice N N ⟨“ J b J 1 𝑜 b ”⟩ A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ r
34 24 33 rspc2v J I K 2 𝑜 a I b 2 𝑜 A r A splice N N ⟨“ a b a 1 𝑜 b ”⟩ A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ r
35 18 34 sylan9 A W N 0 A J I K 2 𝑜 u W i 0 u a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩ A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ r
36 35 adantld A W N 0 A J I K 2 𝑜 r Er W u W i 0 u a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩ A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ r
37 36 alrimiv A W N 0 A J I K 2 𝑜 r r Er W u W i 0 u a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩ A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ r
38 opex A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ V
39 38 elintab A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ r | r Er W u W i 0 u a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩ r r Er W u W i 0 u a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩ A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ r
40 37 39 sylibr A W N 0 A J I K 2 𝑜 A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ r | r Er W u W i 0 u a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩
41 1 2 efgval ˙ = r | r Er W u W i 0 u a I b 2 𝑜 u r u splice i i ⟨“ a b a 1 𝑜 b ”⟩
42 40 41 eleqtrrdi A W N 0 A J I K 2 𝑜 A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ ˙
43 df-br A ˙ A splice N N ⟨“ J K J 1 𝑜 K ”⟩ A A splice N N ⟨“ J K J 1 𝑜 K ”⟩ ˙
44 42 43 sylibr A W N 0 A J I K 2 𝑜 A ˙ A splice N N ⟨“ J K J 1 𝑜 K ”⟩