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 X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
Assertion efgi 
|- ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ ( J e. I /\ K e. 2o ) ) -> A .~ ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) )

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
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 , ( 1o \ b ) >. "> >. ) = ( A splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
7 5 6 breq12d 
 |-  ( u = A -> ( u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) <-> A r ( A splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
8 7 2ralbidv 
 |-  ( u = A -> ( A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) <-> A. a e. I A. b e. 2o A r ( A splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
9 4 8 raleqbidv 
 |-  ( u = A -> ( A. i e. ( 0 ... ( # ` u ) ) A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) <-> A. i e. ( 0 ... ( # ` A ) ) A. a e. I A. b e. 2o A r ( A splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
10 9 rspcv 
 |-  ( A e. W -> ( A. u e. W A. i e. ( 0 ... ( # ` u ) ) A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) -> A. i e. ( 0 ... ( # ` A ) ) A. a e. I A. b e. 2o A r ( A splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
11 oteq1 
 |-  ( i = N -> <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. = <. N , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. )
12 oteq2 
 |-  ( i = N -> <. N , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. = <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. )
13 11 12 eqtrd 
 |-  ( i = N -> <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. = <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. )
14 13 oveq2d 
 |-  ( i = N -> ( A splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) = ( A splice <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
15 14 breq2d 
 |-  ( i = N -> ( A r ( A splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) <-> A r ( A splice <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
16 15 2ralbidv 
 |-  ( i = N -> ( A. a e. I A. b e. 2o A r ( A splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) <-> A. a e. I A. b e. 2o A r ( A splice <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
17 16 rspcv 
 |-  ( N e. ( 0 ... ( # ` A ) ) -> ( A. i e. ( 0 ... ( # ` A ) ) A. a e. I A. b e. 2o A r ( A splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) -> A. a e. I A. b e. 2o A r ( A splice <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
18 10 17 sylan9 
 |-  ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) -> ( A. u e. W A. i e. ( 0 ... ( # ` u ) ) A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) -> A. a e. I A. b e. 2o A r ( A splice <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
19 opeq1 
 |-  ( a = J -> <. a , b >. = <. J , b >. )
20 opeq1 
 |-  ( a = J -> <. a , ( 1o \ b ) >. = <. J , ( 1o \ b ) >. )
21 19 20 s2eqd 
 |-  ( a = J -> <" <. a , b >. <. a , ( 1o \ b ) >. "> = <" <. J , b >. <. J , ( 1o \ b ) >. "> )
22 21 oteq3d 
 |-  ( a = J -> <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. = <. N , N , <" <. J , b >. <. J , ( 1o \ b ) >. "> >. )
23 22 oveq2d 
 |-  ( a = J -> ( A splice <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) = ( A splice <. N , N , <" <. J , b >. <. J , ( 1o \ b ) >. "> >. ) )
24 23 breq2d 
 |-  ( a = J -> ( A r ( A splice <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) <-> A r ( A splice <. N , N , <" <. J , b >. <. J , ( 1o \ b ) >. "> >. ) ) )
25 opeq2 
 |-  ( b = K -> <. J , b >. = <. J , K >. )
26 difeq2 
 |-  ( b = K -> ( 1o \ b ) = ( 1o \ K ) )
27 26 opeq2d 
 |-  ( b = K -> <. J , ( 1o \ b ) >. = <. J , ( 1o \ K ) >. )
28 25 27 s2eqd 
 |-  ( b = K -> <" <. J , b >. <. J , ( 1o \ b ) >. "> = <" <. J , K >. <. J , ( 1o \ K ) >. "> )
29 28 oteq3d 
 |-  ( b = K -> <. N , N , <" <. J , b >. <. J , ( 1o \ b ) >. "> >. = <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. )
30 29 oveq2d 
 |-  ( b = K -> ( A splice <. N , N , <" <. J , b >. <. J , ( 1o \ b ) >. "> >. ) = ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) )
31 30 breq2d 
 |-  ( b = K -> ( A r ( A splice <. N , N , <" <. J , b >. <. J , ( 1o \ b ) >. "> >. ) <-> A r ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) ) )
32 df-br 
 |-  ( A r ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) <-> <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. r )
33 31 32 bitrdi 
 |-  ( b = K -> ( A r ( A splice <. N , N , <" <. J , b >. <. J , ( 1o \ b ) >. "> >. ) <-> <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. r ) )
34 24 33 rspc2v 
 |-  ( ( J e. I /\ K e. 2o ) -> ( A. a e. I A. b e. 2o A r ( A splice <. N , N , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) -> <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. r ) )
35 18 34 sylan9 
 |-  ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ ( J e. I /\ K e. 2o ) ) -> ( A. u e. W A. i e. ( 0 ... ( # ` u ) ) A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) -> <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. r ) )
36 35 adantld 
 |-  ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ ( J e. I /\ K e. 2o ) ) -> ( ( r Er W /\ A. u e. W A. i e. ( 0 ... ( # ` u ) ) A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) -> <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. r ) )
37 36 alrimiv 
 |-  ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ ( J e. I /\ K e. 2o ) ) -> A. r ( ( r Er W /\ A. u e. W A. i e. ( 0 ... ( # ` u ) ) A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) -> <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. r ) )
38 opex 
 |-  <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. _V
39 38 elintab 
 |-  ( <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. |^| { r | ( r Er W /\ A. u e. W A. i e. ( 0 ... ( # ` u ) ) A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } <-> A. r ( ( r Er W /\ A. u e. W A. i e. ( 0 ... ( # ` u ) ) A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) -> <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. r ) )
40 37 39 sylibr 
 |-  ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ ( J e. I /\ K e. 2o ) ) -> <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. |^| { r | ( r Er W /\ A. u e. W A. i e. ( 0 ... ( # ` u ) ) A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } )
41 1 2 efgval 
 |-  .~ = |^| { r | ( r Er W /\ A. u e. W A. i e. ( 0 ... ( # ` u ) ) A. a e. I A. b e. 2o u r ( u splice <. i , i , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) }
42 40 41 eleqtrrdi 
 |-  ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ ( J e. I /\ K e. 2o ) ) -> <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. .~ )
43 df-br 
 |-  ( A .~ ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) <-> <. A , ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) >. e. .~ )
44 42 43 sylibr 
 |-  ( ( ( A e. W /\ N e. ( 0 ... ( # ` A ) ) ) /\ ( J e. I /\ K e. 2o ) ) -> A .~ ( A splice <. N , N , <" <. J , K >. <. J , ( 1o \ K ) >. "> >. ) )