Metamath Proof Explorer

Theorem efglem

Description: Lemma for efgval . (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Hypothesis efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
Assertion efglem 
|- E. r ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) )

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 xpider 
 |-  ( W X. W ) Er W
3 simpll 
 |-  ( ( ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) /\ ( y e. I /\ z e. 2o ) ) -> x e. W )
4 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
5 1 4 eqsstri 
 |-  W C_ Word ( I X. 2o )
6 5 3 sseldi 
 |-  ( ( ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) /\ ( y e. I /\ z e. 2o ) ) -> x e. Word ( I X. 2o ) )
7 opelxpi 
 |-  ( ( y e. I /\ z e. 2o ) -> <. y , z >. e. ( I X. 2o ) )
8 7 adantl 
 |-  ( ( ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) /\ ( y e. I /\ z e. 2o ) ) -> <. y , z >. e. ( I X. 2o ) )
9 2oconcl 
 |-  ( z e. 2o -> ( 1o \ z ) e. 2o )
10 opelxpi 
 |-  ( ( y e. I /\ ( 1o \ z ) e. 2o ) -> <. y , ( 1o \ z ) >. e. ( I X. 2o ) )
11 9 10 sylan2 
 |-  ( ( y e. I /\ z e. 2o ) -> <. y , ( 1o \ z ) >. e. ( I X. 2o ) )
12 11 adantl 
 |-  ( ( ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) /\ ( y e. I /\ z e. 2o ) ) -> <. y , ( 1o \ z ) >. e. ( I X. 2o ) )
13 8 12 s2cld 
 |-  ( ( ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) /\ ( y e. I /\ z e. 2o ) ) -> <" <. y , z >. <. y , ( 1o \ z ) >. "> e. Word ( I X. 2o ) )
14 splcl 
 |-  ( ( x e. Word ( I X. 2o ) /\ <" <. y , z >. <. y , ( 1o \ z ) >. "> e. Word ( I X. 2o ) ) -> ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) e. Word ( I X. 2o ) )
15 6 13 14 syl2anc 
 |-  ( ( ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) /\ ( y e. I /\ z e. 2o ) ) -> ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) e. Word ( I X. 2o ) )
16 1 efgrcl 
 |-  ( x e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
17 16 simprd 
 |-  ( x e. W -> W = Word ( I X. 2o ) )
18 17 ad2antrr 
 |-  ( ( ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) /\ ( y e. I /\ z e. 2o ) ) -> W = Word ( I X. 2o ) )
19 15 18 eleqtrrd 
 |-  ( ( ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) /\ ( y e. I /\ z e. 2o ) ) -> ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) e. W )
20 brxp 
 |-  ( x ( W X. W ) ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) <-> ( x e. W /\ ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) e. W ) )
21 3 19 20 sylanbrc 
 |-  ( ( ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) /\ ( y e. I /\ z e. 2o ) ) -> x ( W X. W ) ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) )
22 21 ralrimivva 
 |-  ( ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) -> A. y e. I A. z e. 2o x ( W X. W ) ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) )
23 22 rgen2 
 |-  A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x ( W X. W ) ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. )
24 1 fvexi 
 |-  W e. _V
25 24 24 xpex 
 |-  ( W X. W ) e. _V
26 ereq1 
 |-  ( r = ( W X. W ) -> ( r Er W <-> ( W X. W ) Er W ) )
27 breq 
 |-  ( r = ( W X. W ) -> ( x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) <-> x ( W X. W ) ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) )
28 27 2ralbidv 
 |-  ( r = ( W X. W ) -> ( A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) <-> A. y e. I A. z e. 2o x ( W X. W ) ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) )
29 28 2ralbidv 
 |-  ( r = ( W X. W ) -> ( A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) <-> A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x ( W X. W ) ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) )
30 26 29 anbi12d 
 |-  ( r = ( W X. W ) -> ( ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) <-> ( ( W X. W ) Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x ( W X. W ) ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) ) )
31 25 30 spcev 
 |-  ( ( ( W X. W ) Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x ( W X. W ) ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) -> E. r ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) ) )
32 2 23 31 mp2an 
 |-  E. r ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. y e. I A. z e. 2o x r ( x splice <. n , n , <" <. y , z >. <. y , ( 1o \ z ) >. "> >. ) )