Metamath Proof Explorer


Theorem efgval2

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

Ref Expression
Hypotheses efgval.w W = I Word I × 2 𝑜
efgval.r ˙ = ~ FG I
efgval2.m M = y I , z 2 𝑜 y 1 𝑜 z
efgval2.t T = v W n 0 v , w I × 2 𝑜 v splice n n ⟨“ w M w ”⟩
Assertion efgval2 ˙ = r | r Er W x W ran T x x r

Proof

Step Hyp Ref Expression
1 efgval.w W = I Word I × 2 𝑜
2 efgval.r ˙ = ~ FG I
3 efgval2.m M = y I , z 2 𝑜 y 1 𝑜 z
4 efgval2.t T = v W n 0 v , w I × 2 𝑜 v splice n n ⟨“ w M w ”⟩
5 1 2 efgval ˙ = r | r Er W x W m 0 x a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
6 1 2 3 4 efgtf x W T x = m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ T x : 0 x × I × 2 𝑜 W
7 6 simpld x W T x = m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩
8 7 rneqd x W ran T x = ran m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩
9 8 sseq1d x W ran T x x r ran m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ x r
10 dfss3 ran m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ x r a ran m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ a x r
11 ovex x splice m m ⟨“ u M u ”⟩ V
12 11 rgen2w m 0 x u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ V
13 eqid m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ = m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩
14 vex a V
15 vex x V
16 14 15 elec a x r x r a
17 breq2 a = x splice m m ⟨“ u M u ”⟩ x r a x r x splice m m ⟨“ u M u ”⟩
18 16 17 syl5bb a = x splice m m ⟨“ u M u ”⟩ a x r x r x splice m m ⟨“ u M u ”⟩
19 13 18 ralrnmpo m 0 x u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ V a ran m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ a x r m 0 x u I × 2 𝑜 x r x splice m m ⟨“ u M u ”⟩
20 12 19 ax-mp a ran m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ a x r m 0 x u I × 2 𝑜 x r x splice m m ⟨“ u M u ”⟩
21 id u = a b u = a b
22 fveq2 u = a b M u = M a b
23 df-ov a M b = M a b
24 22 23 eqtr4di u = a b M u = a M b
25 21 24 s2eqd u = a b ⟨“ u M u ”⟩ = ⟨“ a b a M b ”⟩
26 25 oteq3d u = a b m m ⟨“ u M u ”⟩ = m m ⟨“ a b a M b ”⟩
27 26 oveq2d u = a b x splice m m ⟨“ u M u ”⟩ = x splice m m ⟨“ a b a M b ”⟩
28 27 breq2d u = a b x r x splice m m ⟨“ u M u ”⟩ x r x splice m m ⟨“ a b a M b ”⟩
29 28 ralxp u I × 2 𝑜 x r x splice m m ⟨“ u M u ”⟩ a I b 2 𝑜 x r x splice m m ⟨“ a b a M b ”⟩
30 eqidd a I b 2 𝑜 a b = a b
31 3 efgmval a I b 2 𝑜 a M b = a 1 𝑜 b
32 30 31 s2eqd a I b 2 𝑜 ⟨“ a b a M b ”⟩ = ⟨“ a b a 1 𝑜 b ”⟩
33 32 oteq3d a I b 2 𝑜 m m ⟨“ a b a M b ”⟩ = m m ⟨“ a b a 1 𝑜 b ”⟩
34 33 oveq2d a I b 2 𝑜 x splice m m ⟨“ a b a M b ”⟩ = x splice m m ⟨“ a b a 1 𝑜 b ”⟩
35 34 breq2d a I b 2 𝑜 x r x splice m m ⟨“ a b a M b ”⟩ x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
36 35 ralbidva a I b 2 𝑜 x r x splice m m ⟨“ a b a M b ”⟩ b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
37 36 ralbiia a I b 2 𝑜 x r x splice m m ⟨“ a b a M b ”⟩ a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
38 29 37 bitri u I × 2 𝑜 x r x splice m m ⟨“ u M u ”⟩ a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
39 38 ralbii m 0 x u I × 2 𝑜 x r x splice m m ⟨“ u M u ”⟩ m 0 x a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
40 20 39 bitri a ran m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ a x r m 0 x a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
41 10 40 bitri ran m 0 x , u I × 2 𝑜 x splice m m ⟨“ u M u ”⟩ x r m 0 x a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
42 9 41 bitrdi x W ran T x x r m 0 x a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
43 42 ralbiia x W ran T x x r x W m 0 x a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
44 43 anbi2i r Er W x W ran T x x r r Er W x W m 0 x a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
45 44 abbii r | r Er W x W ran T x x r = r | r Er W x W m 0 x a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
46 45 inteqi r | r Er W x W ran T x x r = r | r Er W x W m 0 x a I b 2 𝑜 x r x splice m m ⟨“ a b a 1 𝑜 b ”⟩
47 5 46 eqtr4i ˙ = r | r Er W x W ran T x x r