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 X. 2o ) )
efgval.r
|- .~ = ( ~FG ` I )
efgval2.m
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
Assertion efgval2
|- .~ = |^| { r | ( r Er W /\ A. x e. W ran ( T ` x ) C_ [ x ] r ) }

Proof

Step Hyp Ref Expression
1 efgval.w
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r
 |-  .~ = ( ~FG ` I )
3 efgval2.m
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4 efgval2.t
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5 1 2 efgval
 |-  .~ = |^| { r | ( r Er W /\ A. x e. W A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) }
6 1 2 3 4 efgtf
 |-  ( x e. W -> ( ( T ` x ) = ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) /\ ( T ` x ) : ( ( 0 ... ( # ` x ) ) X. ( I X. 2o ) ) --> W ) )
7 6 simpld
 |-  ( x e. W -> ( T ` x ) = ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) )
8 7 rneqd
 |-  ( x e. W -> ran ( T ` x ) = ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) )
9 8 sseq1d
 |-  ( x e. W -> ( ran ( T ` x ) C_ [ x ] r <-> ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) C_ [ x ] r ) )
10 dfss3
 |-  ( ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) C_ [ x ] r <-> A. a e. ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) a e. [ x ] r )
11 ovex
 |-  ( x splice <. m , m , <" u ( M ` u ) "> >. ) e. _V
12 11 rgen2w
 |-  A. m e. ( 0 ... ( # ` x ) ) A. u e. ( I X. 2o ) ( x splice <. m , m , <" u ( M ` u ) "> >. ) e. _V
13 eqid
 |-  ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) = ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) )
14 vex
 |-  a e. _V
15 vex
 |-  x e. _V
16 14 15 elec
 |-  ( a e. [ 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 e. [ x ] r <-> x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) )
19 13 18 ralrnmpo
 |-  ( A. m e. ( 0 ... ( # ` x ) ) A. u e. ( I X. 2o ) ( x splice <. m , m , <" u ( M ` u ) "> >. ) e. _V -> ( A. a e. ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) a e. [ x ] r <-> A. m e. ( 0 ... ( # ` x ) ) A. u e. ( I X. 2o ) x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) )
20 12 19 ax-mp
 |-  ( A. a e. ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) a e. [ x ] r <-> A. m e. ( 0 ... ( # ` x ) ) A. u e. ( I X. 2o ) 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
 |-  ( A. u e. ( I X. 2o ) x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) <-> A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) )
30 eqidd
 |-  ( ( a e. I /\ b e. 2o ) -> <. a , b >. = <. a , b >. )
31 3 efgmval
 |-  ( ( a e. I /\ b e. 2o ) -> ( a M b ) = <. a , ( 1o \ b ) >. )
32 30 31 s2eqd
 |-  ( ( a e. I /\ b e. 2o ) -> <" <. a , b >. ( a M b ) "> = <" <. a , b >. <. a , ( 1o \ b ) >. "> )
33 32 oteq3d
 |-  ( ( a e. I /\ b e. 2o ) -> <. m , m , <" <. a , b >. ( a M b ) "> >. = <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. )
34 33 oveq2d
 |-  ( ( a e. I /\ b e. 2o ) -> ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) = ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
35 34 breq2d
 |-  ( ( a e. I /\ b e. 2o ) -> ( x r ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) <-> x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
36 35 ralbidva
 |-  ( a e. I -> ( A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) <-> A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
37 36 ralbiia
 |-  ( A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. ( a M b ) "> >. ) <-> A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
38 29 37 bitri
 |-  ( A. u e. ( I X. 2o ) x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) <-> A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
39 38 ralbii
 |-  ( A. m e. ( 0 ... ( # ` x ) ) A. u e. ( I X. 2o ) x r ( x splice <. m , m , <" u ( M ` u ) "> >. ) <-> A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
40 20 39 bitri
 |-  ( A. a e. ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) a e. [ x ] r <-> A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
41 10 40 bitri
 |-  ( ran ( m e. ( 0 ... ( # ` x ) ) , u e. ( I X. 2o ) |-> ( x splice <. m , m , <" u ( M ` u ) "> >. ) ) C_ [ x ] r <-> A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
42 9 41 bitrdi
 |-  ( x e. W -> ( ran ( T ` x ) C_ [ x ] r <-> A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
43 42 ralbiia
 |-  ( A. x e. W ran ( T ` x ) C_ [ x ] r <-> A. x e. W A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
44 43 anbi2i
 |-  ( ( r Er W /\ A. x e. W ran ( T ` x ) C_ [ x ] r ) <-> ( r Er W /\ A. x e. W A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
45 44 abbii
 |-  { r | ( r Er W /\ A. x e. W ran ( T ` x ) C_ [ x ] r ) } = { r | ( r Er W /\ A. x e. W A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) }
46 45 inteqi
 |-  |^| { r | ( r Er W /\ A. x e. W ran ( T ` x ) C_ [ x ] r ) } = |^| { r | ( r Er W /\ A. x e. W A. m e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. m , m , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) }
47 5 46 eqtr4i
 |-  .~ = |^| { r | ( r Er W /\ A. x e. W ran ( T ` x ) C_ [ x ] r ) }