Metamath Proof Explorer

Theorem ccatalpha

Description: A concatenation of two arbitrary words is a word over an alphabet iff the symbols of both words belong to the alphabet. (Contributed by AV, 28-Feb-2021)

Ref Expression
Assertion ccatalpha 
|- ( ( A e. Word _V /\ B e. Word _V ) -> ( ( A ++ B ) e. Word S <-> ( A e. Word S /\ B e. Word S ) ) )

Proof

Step Hyp Ref Expression
1 ccatfval 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( A ++ B ) = ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) )
2 1 eleq1d 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( A ++ B ) e. Word S <-> ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) e. Word S ) )
3 wrdf 
 |-  ( ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) e. Word S -> ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) : ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) ) --> S )
4 funmpt 
 |-  Fun ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) )
5 fzofi 
 |-  ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) e. Fin
6 mptfi 
 |-  ( ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) e. Fin -> ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) e. Fin )
7 5 6 ax-mp 
 |-  ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) e. Fin
8 hashfun 
 |-  ( ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) e. Fin -> ( Fun ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) <-> ( # ` ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) = ( # ` dom ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) ) )
9 7 8 mp1i 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( Fun ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) <-> ( # ` ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) = ( # ` dom ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) ) )
10 4 9 mpbii 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( # ` ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) = ( # ` dom ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) )
11 dmmptg 
 |-  ( A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. _V -> dom ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) = ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) )
12 fvex 
 |-  ( A ` x ) e. _V
13 fvex 
 |-  ( B ` ( x - ( # ` A ) ) ) e. _V
14 12 13 ifex 
 |-  if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. _V
15 14 a1i 
 |-  ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) -> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. _V )
16 11 15 mprg 
 |-  dom ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) = ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) )
17 16 fveq2i 
 |-  ( # ` dom ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) = ( # ` ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) )
18 lencl 
 |-  ( A e. Word _V -> ( # ` A ) e. NN0 )
19 lencl 
 |-  ( B e. Word _V -> ( # ` B ) e. NN0 )
20 nn0addcl 
 |-  ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 ) -> ( ( # ` A ) + ( # ` B ) ) e. NN0 )
21 18 19 20 syl2an 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( # ` A ) + ( # ` B ) ) e. NN0 )
22 hashfzo0 
 |-  ( ( ( # ` A ) + ( # ` B ) ) e. NN0 -> ( # ` ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) = ( ( # ` A ) + ( # ` B ) ) )
23 21 22 syl 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( # ` ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) = ( ( # ` A ) + ( # ` B ) ) )
24 17 23 eqtrid 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( # ` dom ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) = ( ( # ` A ) + ( # ` B ) ) )
25 10 24 eqtrd 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( # ` ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) = ( ( # ` A ) + ( # ` B ) ) )
26 25 oveq2d 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) ) = ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) )
27 26 feq2d 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) : ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) ) --> S <-> ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) : ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) --> S ) )
28 eqid 
 |-  ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) = ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) )
29 28 fmpt 
 |-  ( A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S <-> ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) : ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) --> S )
30 simpl 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> A e. Word _V )
31 nn0cn 
 |-  ( ( # ` A ) e. NN0 -> ( # ` A ) e. CC )
32 nn0cn 
 |-  ( ( # ` B ) e. NN0 -> ( # ` B ) e. CC )
33 addcom 
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC ) -> ( ( # ` A ) + ( # ` B ) ) = ( ( # ` B ) + ( # ` A ) ) )
34 31 32 33 syl2an 
 |-  ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 ) -> ( ( # ` A ) + ( # ` B ) ) = ( ( # ` B ) + ( # ` A ) ) )
35 nn0z 
 |-  ( ( # ` A ) e. NN0 -> ( # ` A ) e. ZZ )
36 35 anim1ci 
 |-  ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 ) -> ( ( # ` B ) e. NN0 /\ ( # ` A ) e. ZZ ) )
37 nn0pzuz 
 |-  ( ( ( # ` B ) e. NN0 /\ ( # ` A ) e. ZZ ) -> ( ( # ` B ) + ( # ` A ) ) e. ( ZZ>= ` ( # ` A ) ) )
38 36 37 syl 
 |-  ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 ) -> ( ( # ` B ) + ( # ` A ) ) e. ( ZZ>= ` ( # ` A ) ) )
39 34 38 eqeltrd 
 |-  ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 ) -> ( ( # ` A ) + ( # ` B ) ) e. ( ZZ>= ` ( # ` A ) ) )
40 18 19 39 syl2an 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( # ` A ) + ( # ` B ) ) e. ( ZZ>= ` ( # ` A ) ) )
41 fzoss2 
 |-  ( ( ( # ` A ) + ( # ` B ) ) e. ( ZZ>= ` ( # ` A ) ) -> ( 0 ..^ ( # ` A ) ) C_ ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) )
42 40 41 syl 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( 0 ..^ ( # ` A ) ) C_ ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) )
43 42 sselda 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` A ) ) ) -> y e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) )
44 eleq1 
 |-  ( x = y -> ( x e. ( 0 ..^ ( # ` A ) ) <-> y e. ( 0 ..^ ( # ` A ) ) ) )
45 fveq2 
 |-  ( x = y -> ( A ` x ) = ( A ` y ) )
46 fvoveq1 
 |-  ( x = y -> ( B ` ( x - ( # ` A ) ) ) = ( B ` ( y - ( # ` A ) ) ) )
47 44 45 46 ifbieq12d 
 |-  ( x = y -> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) = if ( y e. ( 0 ..^ ( # ` A ) ) , ( A ` y ) , ( B ` ( y - ( # ` A ) ) ) ) )
48 47 eleq1d 
 |-  ( x = y -> ( if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S <-> if ( y e. ( 0 ..^ ( # ` A ) ) , ( A ` y ) , ( B ` ( y - ( # ` A ) ) ) ) e. S ) )
49 48 rspcv 
 |-  ( y e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) -> ( A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S -> if ( y e. ( 0 ..^ ( # ` A ) ) , ( A ` y ) , ( B ` ( y - ( # ` A ) ) ) ) e. S ) )
50 43 49 syl 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` A ) ) ) -> ( A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S -> if ( y e. ( 0 ..^ ( # ` A ) ) , ( A ` y ) , ( B ` ( y - ( # ` A ) ) ) ) e. S ) )
51 iftrue 
 |-  ( y e. ( 0 ..^ ( # ` A ) ) -> if ( y e. ( 0 ..^ ( # ` A ) ) , ( A ` y ) , ( B ` ( y - ( # ` A ) ) ) ) = ( A ` y ) )
52 51 adantl 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` A ) ) ) -> if ( y e. ( 0 ..^ ( # ` A ) ) , ( A ` y ) , ( B ` ( y - ( # ` A ) ) ) ) = ( A ` y ) )
53 52 eleq1d 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` A ) ) ) -> ( if ( y e. ( 0 ..^ ( # ` A ) ) , ( A ` y ) , ( B ` ( y - ( # ` A ) ) ) ) e. S <-> ( A ` y ) e. S ) )
54 50 53 sylibd 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` A ) ) ) -> ( A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S -> ( A ` y ) e. S ) )
55 54 impancom 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S ) -> ( y e. ( 0 ..^ ( # ` A ) ) -> ( A ` y ) e. S ) )
56 55 ralrimiv 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S ) -> A. y e. ( 0 ..^ ( # ` A ) ) ( A ` y ) e. S )
57 iswrdsymb 
 |-  ( ( A e. Word _V /\ A. y e. ( 0 ..^ ( # ` A ) ) ( A ` y ) e. S ) -> A e. Word S )
58 30 56 57 syl2an2r 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S ) -> A e. Word S )
59 simpr 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> B e. Word _V )
60 simpr 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> y e. ( 0 ..^ ( # ` B ) ) )
61 18 adantr 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( # ` A ) e. NN0 )
62 61 adantr 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( # ` A ) e. NN0 )
63 elincfzoext 
 |-  ( ( y e. ( 0 ..^ ( # ` B ) ) /\ ( # ` A ) e. NN0 ) -> ( y + ( # ` A ) ) e. ( 0 ..^ ( ( # ` B ) + ( # ` A ) ) ) )
64 60 62 63 syl2anc 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( y + ( # ` A ) ) e. ( 0 ..^ ( ( # ` B ) + ( # ` A ) ) ) )
65 18 nn0cnd 
 |-  ( A e. Word _V -> ( # ` A ) e. CC )
66 19 nn0cnd 
 |-  ( B e. Word _V -> ( # ` B ) e. CC )
67 65 66 33 syl2an 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( # ` A ) + ( # ` B ) ) = ( ( # ` B ) + ( # ` A ) ) )
68 67 oveq2d 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) = ( 0 ..^ ( ( # ` B ) + ( # ` A ) ) ) )
69 68 eleq2d 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( y + ( # ` A ) ) e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( y + ( # ` A ) ) e. ( 0 ..^ ( ( # ` B ) + ( # ` A ) ) ) ) )
70 69 adantr 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( ( y + ( # ` A ) ) e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( y + ( # ` A ) ) e. ( 0 ..^ ( ( # ` B ) + ( # ` A ) ) ) ) )
71 64 70 mpbird 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( y + ( # ` A ) ) e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) )
72 eleq1 
 |-  ( x = ( y + ( # ` A ) ) -> ( x e. ( 0 ..^ ( # ` A ) ) <-> ( y + ( # ` A ) ) e. ( 0 ..^ ( # ` A ) ) ) )
73 fveq2 
 |-  ( x = ( y + ( # ` A ) ) -> ( A ` x ) = ( A ` ( y + ( # ` A ) ) ) )
74 fvoveq1 
 |-  ( x = ( y + ( # ` A ) ) -> ( B ` ( x - ( # ` A ) ) ) = ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) )
75 72 73 74 ifbieq12d 
 |-  ( x = ( y + ( # ` A ) ) -> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) = if ( ( y + ( # ` A ) ) e. ( 0 ..^ ( # ` A ) ) , ( A ` ( y + ( # ` A ) ) ) , ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) ) )
76 75 eleq1d 
 |-  ( x = ( y + ( # ` A ) ) -> ( if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S <-> if ( ( y + ( # ` A ) ) e. ( 0 ..^ ( # ` A ) ) , ( A ` ( y + ( # ` A ) ) ) , ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) ) e. S ) )
77 76 rspcv 
 |-  ( ( y + ( # ` A ) ) e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) -> ( A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S -> if ( ( y + ( # ` A ) ) e. ( 0 ..^ ( # ` A ) ) , ( A ` ( y + ( # ` A ) ) ) , ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) ) e. S ) )
78 71 77 syl 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S -> if ( ( y + ( # ` A ) ) e. ( 0 ..^ ( # ` A ) ) , ( A ` ( y + ( # ` A ) ) ) , ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) ) e. S ) )
79 18 nn0red 
 |-  ( A e. Word _V -> ( # ` A ) e. RR )
80 79 adantr 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( # ` A ) e. RR )
81 80 adantr 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( # ` A ) e. RR )
82 elfzoelz 
 |-  ( y e. ( 0 ..^ ( # ` B ) ) -> y e. ZZ )
83 82 zred 
 |-  ( y e. ( 0 ..^ ( # ` B ) ) -> y e. RR )
84 83 adantr 
 |-  ( ( y e. ( 0 ..^ ( # ` B ) ) /\ ( A e. Word _V /\ B e. Word _V ) ) -> y e. RR )
85 80 adantl 
 |-  ( ( y e. ( 0 ..^ ( # ` B ) ) /\ ( A e. Word _V /\ B e. Word _V ) ) -> ( # ` A ) e. RR )
86 84 85 readdcld 
 |-  ( ( y e. ( 0 ..^ ( # ` B ) ) /\ ( A e. Word _V /\ B e. Word _V ) ) -> ( y + ( # ` A ) ) e. RR )
87 86 ancoms 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( y + ( # ` A ) ) e. RR )
88 elfzole1 
 |-  ( y e. ( 0 ..^ ( # ` B ) ) -> 0 <_ y )
89 88 adantl 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> 0 <_ y )
90 addge02 
 |-  ( ( ( # ` A ) e. RR /\ y e. RR ) -> ( 0 <_ y <-> ( # ` A ) <_ ( y + ( # ` A ) ) ) )
91 80 83 90 syl2an 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( 0 <_ y <-> ( # ` A ) <_ ( y + ( # ` A ) ) ) )
92 89 91 mpbid 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( # ` A ) <_ ( y + ( # ` A ) ) )
93 81 87 92 lensymd 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> -. ( y + ( # ` A ) ) < ( # ` A ) )
94 93 intn3an3d 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> -. ( ( y + ( # ` A ) ) e. NN0 /\ ( # ` A ) e. NN /\ ( y + ( # ` A ) ) < ( # ` A ) ) )
95 elfzo0 
 |-  ( ( y + ( # ` A ) ) e. ( 0 ..^ ( # ` A ) ) <-> ( ( y + ( # ` A ) ) e. NN0 /\ ( # ` A ) e. NN /\ ( y + ( # ` A ) ) < ( # ` A ) ) )
96 94 95 sylnibr 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> -. ( y + ( # ` A ) ) e. ( 0 ..^ ( # ` A ) ) )
97 96 iffalsed 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> if ( ( y + ( # ` A ) ) e. ( 0 ..^ ( # ` A ) ) , ( A ` ( y + ( # ` A ) ) ) , ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) ) = ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) )
98 97 eleq1d 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( if ( ( y + ( # ` A ) ) e. ( 0 ..^ ( # ` A ) ) , ( A ` ( y + ( # ` A ) ) ) , ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) ) e. S <-> ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) e. S ) )
99 82 zcnd 
 |-  ( y e. ( 0 ..^ ( # ` B ) ) -> y e. CC )
100 65 adantr 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( # ` A ) e. CC )
101 pncan 
 |-  ( ( y e. CC /\ ( # ` A ) e. CC ) -> ( ( y + ( # ` A ) ) - ( # ` A ) ) = y )
102 99 100 101 syl2anr 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( ( y + ( # ` A ) ) - ( # ` A ) ) = y )
103 102 fveq2d 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) = ( B ` y ) )
104 103 eleq1d 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) e. S <-> ( B ` y ) e. S ) )
105 104 biimpd 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) e. S -> ( B ` y ) e. S ) )
106 98 105 sylbid 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( if ( ( y + ( # ` A ) ) e. ( 0 ..^ ( # ` A ) ) , ( A ` ( y + ( # ` A ) ) ) , ( B ` ( ( y + ( # ` A ) ) - ( # ` A ) ) ) ) e. S -> ( B ` y ) e. S ) )
107 78 106 syld 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ y e. ( 0 ..^ ( # ` B ) ) ) -> ( A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S -> ( B ` y ) e. S ) )
108 107 impancom 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S ) -> ( y e. ( 0 ..^ ( # ` B ) ) -> ( B ` y ) e. S ) )
109 108 ralrimiv 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S ) -> A. y e. ( 0 ..^ ( # ` B ) ) ( B ` y ) e. S )
110 iswrdsymb 
 |-  ( ( B e. Word _V /\ A. y e. ( 0 ..^ ( # ` B ) ) ( B ` y ) e. S ) -> B e. Word S )
111 59 109 110 syl2an2r 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S ) -> B e. Word S )
112 58 111 jca 
 |-  ( ( ( A e. Word _V /\ B e. Word _V ) /\ A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S ) -> ( A e. Word S /\ B e. Word S ) )
113 112 ex 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( A. x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. S -> ( A e. Word S /\ B e. Word S ) ) )
114 29 113 syl5bir 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) : ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) --> S -> ( A e. Word S /\ B e. Word S ) ) )
115 27 114 sylbid 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) : ( 0 ..^ ( # ` ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) ) ) --> S -> ( A e. Word S /\ B e. Word S ) ) )
116 3 115 syl5 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) e. Word S -> ( A e. Word S /\ B e. Word S ) ) )
117 2 116 sylbid 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( A ++ B ) e. Word S -> ( A e. Word S /\ B e. Word S ) ) )
118 ccatcl 
 |-  ( ( A e. Word S /\ B e. Word S ) -> ( A ++ B ) e. Word S )
119 117 118 impbid1 
 |-  ( ( A e. Word _V /\ B e. Word _V ) -> ( ( A ++ B ) e. Word S <-> ( A e. Word S /\ B e. Word S ) ) )