Metamath Proof Explorer

Theorem ccatws1f1o

Description: Conditions for the concatenation of a word and a singleton word to be bijective. (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Hypotheses ccatws1f1o.1 
|- N = ( # ` T )
ccatws1f1o.2 
|- J = ( 0 ..^ ( N + 1 ) )
ccatws1f1o.3 
|- ( ph -> T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) )
Assertion ccatws1f1o 
|- ( ph -> ( T ++ <" N "> ) : J -1-1-onto-> J )

Proof

Step Hyp Ref Expression
1 ccatws1f1o.1 
 |-  N = ( # ` T )
2 ccatws1f1o.2 
 |-  J = ( 0 ..^ ( N + 1 ) )
3 ccatws1f1o.3 
 |-  ( ph -> T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) )
4 f1of 
 |-  ( T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) -> T : ( 0 ..^ N ) --> ( 0 ..^ N ) )
5 3 4 syl 
 |-  ( ph -> T : ( 0 ..^ N ) --> ( 0 ..^ N ) )
6 iswrdi 
 |-  ( T : ( 0 ..^ N ) --> ( 0 ..^ N ) -> T e. Word ( 0 ..^ N ) )
7 lencl 
 |-  ( T e. Word ( 0 ..^ N ) -> ( # ` T ) e. NN0 )
8 5 6 7 3syl 
 |-  ( ph -> ( # ` T ) e. NN0 )
9 1 8 eqeltrid 
 |-  ( ph -> N e. NN0 )
10 fzossfzop1 
 |-  ( N e. NN0 -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
11 9 10 syl 
 |-  ( ph -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
12 11 2 sseqtrrdi 
 |-  ( ph -> ( 0 ..^ N ) C_ J )
13 12 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` T ) ) ) -> ( 0 ..^ N ) C_ J )
14 5 adantr 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` T ) ) ) -> T : ( 0 ..^ N ) --> ( 0 ..^ N ) )
15 1 eqcomi 
 |-  ( # ` T ) = N
16 15 a1i 
 |-  ( ph -> ( # ` T ) = N )
17 16 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` T ) ) = ( 0 ..^ N ) )
18 17 eleq2d 
 |-  ( ph -> ( x e. ( 0 ..^ ( # ` T ) ) <-> x e. ( 0 ..^ N ) ) )
19 18 biimpa 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` T ) ) ) -> x e. ( 0 ..^ N ) )
20 14 19 ffvelcdmd 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` T ) ) ) -> ( T ` x ) e. ( 0 ..^ N ) )
21 13 20 sseldd 
 |-  ( ( ph /\ x e. ( 0 ..^ ( # ` T ) ) ) -> ( T ` x ) e. J )
22 21 adantlr 
 |-  ( ( ( ph /\ x e. J ) /\ x e. ( 0 ..^ ( # ` T ) ) ) -> ( T ` x ) e. J )
23 2 a1i 
 |-  ( ph -> J = ( 0 ..^ ( N + 1 ) ) )
24 fzo0ssnn0 
 |-  ( 0 ..^ ( N + 1 ) ) C_ NN0
25 23 24 eqsstrdi 
 |-  ( ph -> J C_ NN0 )
26 25 sselda 
 |-  ( ( ph /\ x e. J ) -> x e. NN0 )
27 26 nn0cnd 
 |-  ( ( ph /\ x e. J ) -> x e. CC )
28 27 adantr 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> x e. CC )
29 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
30 9 29 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
31 30 ad2antrr 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> N e. ( ZZ>= ` 0 ) )
32 23 eleq2d 
 |-  ( ph -> ( x e. J <-> x e. ( 0 ..^ ( N + 1 ) ) ) )
33 32 biimpa 
 |-  ( ( ph /\ x e. J ) -> x e. ( 0 ..^ ( N + 1 ) ) )
34 33 adantr 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> x e. ( 0 ..^ ( N + 1 ) ) )
35 fzosplitsni 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( x e. ( 0 ..^ ( N + 1 ) ) <-> ( x e. ( 0 ..^ N ) \/ x = N ) ) )
36 35 biimpa 
 |-  ( ( N e. ( ZZ>= ` 0 ) /\ x e. ( 0 ..^ ( N + 1 ) ) ) -> ( x e. ( 0 ..^ N ) \/ x = N ) )
37 31 34 36 syl2anc 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> ( x e. ( 0 ..^ N ) \/ x = N ) )
38 18 notbid 
 |-  ( ph -> ( -. x e. ( 0 ..^ ( # ` T ) ) <-> -. x e. ( 0 ..^ N ) ) )
39 38 biimpa 
 |-  ( ( ph /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> -. x e. ( 0 ..^ N ) )
40 39 adantlr 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> -. x e. ( 0 ..^ N ) )
41 37 40 orcnd 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> x = N )
42 41 1 eqtrdi 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> x = ( # ` T ) )
43 28 42 subeq0bd 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> ( x - ( # ` T ) ) = 0 )
44 43 fveq2d 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> ( <" N "> ` ( x - ( # ` T ) ) ) = ( <" N "> ` 0 ) )
45 s1fv 
 |-  ( N e. NN0 -> ( <" N "> ` 0 ) = N )
46 9 45 syl 
 |-  ( ph -> ( <" N "> ` 0 ) = N )
47 46 ad2antrr 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> ( <" N "> ` 0 ) = N )
48 44 47 eqtrd 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> ( <" N "> ` ( x - ( # ` T ) ) ) = N )
49 fzonn0p1 
 |-  ( N e. NN0 -> N e. ( 0 ..^ ( N + 1 ) ) )
50 9 49 syl 
 |-  ( ph -> N e. ( 0 ..^ ( N + 1 ) ) )
51 50 2 eleqtrrdi 
 |-  ( ph -> N e. J )
52 51 ad2antrr 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> N e. J )
53 48 52 eqeltrd 
 |-  ( ( ( ph /\ x e. J ) /\ -. x e. ( 0 ..^ ( # ` T ) ) ) -> ( <" N "> ` ( x - ( # ` T ) ) ) e. J )
54 22 53 ifclda 
 |-  ( ( ph /\ x e. J ) -> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) e. J )
55 54 ralrimiva 
 |-  ( ph -> A. x e. J if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) e. J )
56 12 ad2antrr 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> ( 0 ..^ N ) C_ J )
57 f1ocnv 
 |-  ( T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) -> `' T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) )
58 f1of 
 |-  ( `' T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) -> `' T : ( 0 ..^ N ) --> ( 0 ..^ N ) )
59 3 57 58 3syl 
 |-  ( ph -> `' T : ( 0 ..^ N ) --> ( 0 ..^ N ) )
60 59 adantr 
 |-  ( ( ph /\ y e. J ) -> `' T : ( 0 ..^ N ) --> ( 0 ..^ N ) )
61 60 ffvelcdmda 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> ( `' T ` y ) e. ( 0 ..^ N ) )
62 56 61 sseldd 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> ( `' T ` y ) e. J )
63 1 oveq2i 
 |-  ( 0 ..^ N ) = ( 0 ..^ ( # ` T ) )
64 61 63 eleqtrdi 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> ( `' T ` y ) e. ( 0 ..^ ( # ` T ) ) )
65 64 iftrued 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> if ( ( `' T ` y ) e. ( 0 ..^ ( # ` T ) ) , ( T ` ( `' T ` y ) ) , ( <" N "> ` ( ( `' T ` y ) - ( # ` T ) ) ) ) = ( T ` ( `' T ` y ) ) )
66 3 ad2antrr 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) )
67 simpr 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> y e. ( 0 ..^ N ) )
68 f1ocnvfv2 
 |-  ( ( T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) /\ y e. ( 0 ..^ N ) ) -> ( T ` ( `' T ` y ) ) = y )
69 66 67 68 syl2anc 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> ( T ` ( `' T ` y ) ) = y )
70 65 69 eqtr2d 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> y = if ( ( `' T ` y ) e. ( 0 ..^ ( # ` T ) ) , ( T ` ( `' T ` y ) ) , ( <" N "> ` ( ( `' T ` y ) - ( # ` T ) ) ) ) )
71 simpr 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) )
72 30 adantr 
 |-  ( ( ph /\ x e. J ) -> N e. ( ZZ>= ` 0 ) )
73 72 33 36 syl2anc 
 |-  ( ( ph /\ x e. J ) -> ( x e. ( 0 ..^ N ) \/ x = N ) )
74 73 ad5ant14 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> ( x e. ( 0 ..^ N ) \/ x = N ) )
75 67 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> y e. ( 0 ..^ N ) )
76 71 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) )
77 simpr 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> x = N )
78 fzonel 
 |-  -. N e. ( 0 ..^ N )
79 78 a1i 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> -. N e. ( 0 ..^ N ) )
80 63 eleq2i 
 |-  ( N e. ( 0 ..^ N ) <-> N e. ( 0 ..^ ( # ` T ) ) )
81 79 80 sylnib 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> -. N e. ( 0 ..^ ( # ` T ) ) )
82 77 81 eqneltrd 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> -. x e. ( 0 ..^ ( # ` T ) ) )
83 82 iffalsed 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) = ( <" N "> ` ( x - ( # ` T ) ) ) )
84 2 24 eqsstri 
 |-  J C_ NN0
85 simpllr 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> x e. J )
86 84 85 sselid 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> x e. NN0 )
87 86 nn0cnd 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> x e. CC )
88 77 1 eqtrdi 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> x = ( # ` T ) )
89 87 88 subeq0bd 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> ( x - ( # ` T ) ) = 0 )
90 89 fveq2d 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> ( <" N "> ` ( x - ( # ` T ) ) ) = ( <" N "> ` 0 ) )
91 46 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> ( <" N "> ` 0 ) = N )
92 90 91 eqtrd 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> ( <" N "> ` ( x - ( # ` T ) ) ) = N )
93 76 83 92 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> y = N )
94 93 79 eqneltrd 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x = N ) -> -. y e. ( 0 ..^ N ) )
95 75 94 pm2.65da 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> -. x = N )
96 74 95 olcnd 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> x e. ( 0 ..^ N ) )
97 96 63 eleqtrdi 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> x e. ( 0 ..^ ( # ` T ) ) )
98 97 iftrued 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) = ( T ` x ) )
99 71 98 eqtrd 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> y = ( T ` x ) )
100 99 fveq2d 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> ( `' T ` y ) = ( `' T ` ( T ` x ) ) )
101 66 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) )
102 f1ocnvfv1 
 |-  ( ( T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) /\ x e. ( 0 ..^ N ) ) -> ( `' T ` ( T ` x ) ) = x )
103 101 96 102 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> ( `' T ` ( T ` x ) ) = x )
104 100 103 eqtr2d 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> x = ( `' T ` y ) )
105 104 ex 
 |-  ( ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) /\ x e. J ) -> ( y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) -> x = ( `' T ` y ) ) )
106 105 ralrimiva 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> A. x e. J ( y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) -> x = ( `' T ` y ) ) )
107 eleq1 
 |-  ( x = ( `' T ` y ) -> ( x e. ( 0 ..^ ( # ` T ) ) <-> ( `' T ` y ) e. ( 0 ..^ ( # ` T ) ) ) )
108 fveq2 
 |-  ( x = ( `' T ` y ) -> ( T ` x ) = ( T ` ( `' T ` y ) ) )
109 fvoveq1 
 |-  ( x = ( `' T ` y ) -> ( <" N "> ` ( x - ( # ` T ) ) ) = ( <" N "> ` ( ( `' T ` y ) - ( # ` T ) ) ) )
110 107 108 109 ifbieq12d 
 |-  ( x = ( `' T ` y ) -> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) = if ( ( `' T ` y ) e. ( 0 ..^ ( # ` T ) ) , ( T ` ( `' T ` y ) ) , ( <" N "> ` ( ( `' T ` y ) - ( # ` T ) ) ) ) )
111 110 eqeq2d 
 |-  ( x = ( `' T ` y ) -> ( y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) <-> y = if ( ( `' T ` y ) e. ( 0 ..^ ( # ` T ) ) , ( T ` ( `' T ` y ) ) , ( <" N "> ` ( ( `' T ` y ) - ( # ` T ) ) ) ) ) )
112 111 eqreu 
 |-  ( ( ( `' T ` y ) e. J /\ y = if ( ( `' T ` y ) e. ( 0 ..^ ( # ` T ) ) , ( T ` ( `' T ` y ) ) , ( <" N "> ` ( ( `' T ` y ) - ( # ` T ) ) ) ) /\ A. x e. J ( y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) -> x = ( `' T ` y ) ) ) -> E! x e. J y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) )
113 62 70 106 112 syl3anc 
 |-  ( ( ( ph /\ y e. J ) /\ y e. ( 0 ..^ N ) ) -> E! x e. J y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) )
114 51 ad2antrr 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> N e. J )
115 9 nn0cnd 
 |-  ( ph -> N e. CC )
116 115 ad2antrr 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> N e. CC )
117 1 a1i 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> N = ( # ` T ) )
118 116 117 subeq0bd 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> ( N - ( # ` T ) ) = 0 )
119 118 fveq2d 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> ( <" N "> ` ( N - ( # ` T ) ) ) = ( <" N "> ` 0 ) )
120 46 ad2antrr 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> ( <" N "> ` 0 ) = N )
121 119 120 eqtrd 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> ( <" N "> ` ( N - ( # ` T ) ) ) = N )
122 78 a1i 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> -. N e. ( 0 ..^ N ) )
123 122 80 sylnib 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> -. N e. ( 0 ..^ ( # ` T ) ) )
124 123 iffalsed 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> if ( N e. ( 0 ..^ ( # ` T ) ) , ( T ` N ) , ( <" N "> ` ( N - ( # ` T ) ) ) ) = ( <" N "> ` ( N - ( # ` T ) ) ) )
125 simpr 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> y = N )
126 121 124 125 3eqtr4rd 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> y = if ( N e. ( 0 ..^ ( # ` T ) ) , ( T ` N ) , ( <" N "> ` ( N - ( # ` T ) ) ) ) )
127 30 adantr 
 |-  ( ( ph /\ y e. J ) -> N e. ( ZZ>= ` 0 ) )
128 127 ad3antrrr 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> N e. ( ZZ>= ` 0 ) )
129 33 ad5ant14 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> x e. ( 0 ..^ ( N + 1 ) ) )
130 128 129 36 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> ( x e. ( 0 ..^ N ) \/ x = N ) )
131 simpr 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) )
132 simpllr 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> y = N )
133 131 132 eqtr3d 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) = N )
134 133 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x e. ( 0 ..^ N ) ) -> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) = N )
135 63 a1i 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> ( 0 ..^ N ) = ( 0 ..^ ( # ` T ) ) )
136 135 eleq2d 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> ( x e. ( 0 ..^ N ) <-> x e. ( 0 ..^ ( # ` T ) ) ) )
137 136 biimpa 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x e. ( 0 ..^ N ) ) -> x e. ( 0 ..^ ( # ` T ) ) )
138 137 iftrued 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x e. ( 0 ..^ N ) ) -> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) = ( T ` x ) )
139 5 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> T : ( 0 ..^ N ) --> ( 0 ..^ N ) )
140 139 ffvelcdmda 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x e. ( 0 ..^ N ) ) -> ( T ` x ) e. ( 0 ..^ N ) )
141 138 140 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x e. ( 0 ..^ N ) ) -> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) e. ( 0 ..^ N ) )
142 134 141 eqeltrrd 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x e. ( 0 ..^ N ) ) -> N e. ( 0 ..^ N ) )
143 78 a1i 
 |-  ( ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) /\ x e. ( 0 ..^ N ) ) -> -. N e. ( 0 ..^ N ) )
144 142 143 pm2.65da 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> -. x e. ( 0 ..^ N ) )
145 130 144 orcnd 
 |-  ( ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) /\ y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) -> x = N )
146 145 ex 
 |-  ( ( ( ( ph /\ y e. J ) /\ y = N ) /\ x e. J ) -> ( y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) -> x = N ) )
147 146 ralrimiva 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> A. x e. J ( y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) -> x = N ) )
148 eleq1 
 |-  ( x = N -> ( x e. ( 0 ..^ ( # ` T ) ) <-> N e. ( 0 ..^ ( # ` T ) ) ) )
149 fveq2 
 |-  ( x = N -> ( T ` x ) = ( T ` N ) )
150 fvoveq1 
 |-  ( x = N -> ( <" N "> ` ( x - ( # ` T ) ) ) = ( <" N "> ` ( N - ( # ` T ) ) ) )
151 148 149 150 ifbieq12d 
 |-  ( x = N -> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) = if ( N e. ( 0 ..^ ( # ` T ) ) , ( T ` N ) , ( <" N "> ` ( N - ( # ` T ) ) ) ) )
152 151 eqeq2d 
 |-  ( x = N -> ( y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) <-> y = if ( N e. ( 0 ..^ ( # ` T ) ) , ( T ` N ) , ( <" N "> ` ( N - ( # ` T ) ) ) ) ) )
153 152 eqreu 
 |-  ( ( N e. J /\ y = if ( N e. ( 0 ..^ ( # ` T ) ) , ( T ` N ) , ( <" N "> ` ( N - ( # ` T ) ) ) ) /\ A. x e. J ( y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) -> x = N ) ) -> E! x e. J y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) )
154 114 126 147 153 syl3anc 
 |-  ( ( ( ph /\ y e. J ) /\ y = N ) -> E! x e. J y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) )
155 23 eleq2d 
 |-  ( ph -> ( y e. J <-> y e. ( 0 ..^ ( N + 1 ) ) ) )
156 155 biimpa 
 |-  ( ( ph /\ y e. J ) -> y e. ( 0 ..^ ( N + 1 ) ) )
157 fzosplitsni 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( y e. ( 0 ..^ ( N + 1 ) ) <-> ( y e. ( 0 ..^ N ) \/ y = N ) ) )
158 157 biimpa 
 |-  ( ( N e. ( ZZ>= ` 0 ) /\ y e. ( 0 ..^ ( N + 1 ) ) ) -> ( y e. ( 0 ..^ N ) \/ y = N ) )
159 127 156 158 syl2anc 
 |-  ( ( ph /\ y e. J ) -> ( y e. ( 0 ..^ N ) \/ y = N ) )
160 113 154 159 mpjaodan 
 |-  ( ( ph /\ y e. J ) -> E! x e. J y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) )
161 160 ralrimiva 
 |-  ( ph -> A. y e. J E! x e. J y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) )
162 s1len 
 |-  ( # ` <" N "> ) = 1
163 15 162 oveq12i 
 |-  ( ( # ` T ) + ( # ` <" N "> ) ) = ( N + 1 )
164 163 oveq2i 
 |-  ( 0 ..^ ( ( # ` T ) + ( # ` <" N "> ) ) ) = ( 0 ..^ ( N + 1 ) )
165 164 2 eqtr4i 
 |-  ( 0 ..^ ( ( # ` T ) + ( # ` <" N "> ) ) ) = J
166 165 mpteq1i 
 |-  ( x e. ( 0 ..^ ( ( # ` T ) + ( # ` <" N "> ) ) ) |-> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) = ( x e. J |-> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) )
167 166 f1ompt 
 |-  ( ( x e. ( 0 ..^ ( ( # ` T ) + ( # ` <" N "> ) ) ) |-> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) : J -1-1-onto-> J <-> ( A. x e. J if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) e. J /\ A. y e. J E! x e. J y = if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) )
168 55 161 167 sylanbrc 
 |-  ( ph -> ( x e. ( 0 ..^ ( ( # ` T ) + ( # ` <" N "> ) ) ) |-> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) : J -1-1-onto-> J )
169 ovex 
 |-  ( 0 ..^ N ) e. _V
170 fex 
 |-  ( ( T : ( 0 ..^ N ) --> ( 0 ..^ N ) /\ ( 0 ..^ N ) e. _V ) -> T e. _V )
171 5 169 170 sylancl 
 |-  ( ph -> T e. _V )
172 s1cli 
 |-  <" N "> e. Word _V
173 ccatfval 
 |-  ( ( T e. _V /\ <" N "> e. Word _V ) -> ( T ++ <" N "> ) = ( x e. ( 0 ..^ ( ( # ` T ) + ( # ` <" N "> ) ) ) |-> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) )
174 171 172 173 sylancl 
 |-  ( ph -> ( T ++ <" N "> ) = ( x e. ( 0 ..^ ( ( # ` T ) + ( # ` <" N "> ) ) ) |-> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) )
175 174 f1oeq1d 
 |-  ( ph -> ( ( T ++ <" N "> ) : J -1-1-onto-> J <-> ( x e. ( 0 ..^ ( ( # ` T ) + ( # ` <" N "> ) ) ) |-> if ( x e. ( 0 ..^ ( # ` T ) ) , ( T ` x ) , ( <" N "> ` ( x - ( # ` T ) ) ) ) ) : J -1-1-onto-> J ) )
176 168 175 mpbird 
 |-  ( ph -> ( T ++ <" N "> ) : J -1-1-onto-> J )