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 ) }