Metamath Proof Explorer

Theorem ccatf1

Description: Conditions for a concatenation to be injective. (Contributed by Thierry Arnoux, 11-Dec-2023)

Ref Expression
Hypotheses ccatf1.s 
|- ( ph -> S e. V )
ccatf1.a 
|- ( ph -> A e. Word S )
ccatf1.b 
|- ( ph -> B e. Word S )
ccatf1.1 
|- ( ph -> A : dom A -1-1-> S )
ccatf1.2 
|- ( ph -> B : dom B -1-1-> S )
ccatf1.3 
|- ( ph -> ( ran A i^i ran B ) = (/) )
Assertion ccatf1 
|- ( ph -> ( A ++ B ) : dom ( A ++ B ) -1-1-> S )

Proof

Step Hyp Ref Expression
1 ccatf1.s 
 |-  ( ph -> S e. V )
2 ccatf1.a 
 |-  ( ph -> A e. Word S )
3 ccatf1.b 
 |-  ( ph -> B e. Word S )
4 ccatf1.1 
 |-  ( ph -> A : dom A -1-1-> S )
5 ccatf1.2 
 |-  ( ph -> B : dom B -1-1-> S )
6 ccatf1.3 
 |-  ( ph -> ( ran A i^i ran B ) = (/) )
7 ccatcl 
 |-  ( ( A e. Word S /\ B e. Word S ) -> ( A ++ B ) e. Word S )
8 2 3 7 syl2anc 
 |-  ( ph -> ( A ++ B ) e. Word S )
9 wrdf 
 |-  ( ( A ++ B ) e. Word S -> ( A ++ B ) : ( 0 ..^ ( # ` ( A ++ B ) ) ) --> S )
10 8 9 syl 
 |-  ( ph -> ( A ++ B ) : ( 0 ..^ ( # ` ( A ++ B ) ) ) --> S )
11 10 ffdmd 
 |-  ( ph -> ( A ++ B ) : dom ( A ++ B ) --> S )
12 simpllr 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) )
13 id 
 |-  ( i e. ( 0 ..^ ( # ` A ) ) -> i e. ( 0 ..^ ( # ` A ) ) )
14 ccatval1 
 |-  ( ( A e. Word S /\ B e. Word S /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` i ) = ( A ` i ) )
15 2 3 13 14 syl2an3an 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` i ) = ( A ` i ) )
16 15 ad4ant13 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` i ) = ( A ` i ) )
17 id 
 |-  ( j e. ( 0 ..^ ( # ` A ) ) -> j e. ( 0 ..^ ( # ` A ) ) )
18 ccatval1 
 |-  ( ( A e. Word S /\ B e. Word S /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` j ) = ( A ` j ) )
19 2 3 17 18 syl2an3an 
 |-  ( ( ph /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` j ) = ( A ` j ) )
20 19 ad4ant14 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` j ) = ( A ` j ) )
21 12 16 20 3eqtr3d 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` i ) = ( A ` j ) )
22 wrddm 
 |-  ( A e. Word S -> dom A = ( 0 ..^ ( # ` A ) ) )
23 2 22 syl 
 |-  ( ph -> dom A = ( 0 ..^ ( # ` A ) ) )
24 f1eq2 
 |-  ( dom A = ( 0 ..^ ( # ` A ) ) -> ( A : dom A -1-1-> S <-> A : ( 0 ..^ ( # ` A ) ) -1-1-> S ) )
25 24 biimpa 
 |-  ( ( dom A = ( 0 ..^ ( # ` A ) ) /\ A : dom A -1-1-> S ) -> A : ( 0 ..^ ( # ` A ) ) -1-1-> S )
26 23 4 25 syl2anc 
 |-  ( ph -> A : ( 0 ..^ ( # ` A ) ) -1-1-> S )
27 dff13 
 |-  ( A : ( 0 ..^ ( # ` A ) ) -1-1-> S <-> ( A : ( 0 ..^ ( # ` A ) ) --> S /\ A. i e. ( 0 ..^ ( # ` A ) ) A. j e. ( 0 ..^ ( # ` A ) ) ( ( A ` i ) = ( A ` j ) -> i = j ) ) )
28 27 simprbi 
 |-  ( A : ( 0 ..^ ( # ` A ) ) -1-1-> S -> A. i e. ( 0 ..^ ( # ` A ) ) A. j e. ( 0 ..^ ( # ` A ) ) ( ( A ` i ) = ( A ` j ) -> i = j ) )
29 26 28 syl 
 |-  ( ph -> A. i e. ( 0 ..^ ( # ` A ) ) A. j e. ( 0 ..^ ( # ` A ) ) ( ( A ` i ) = ( A ` j ) -> i = j ) )
30 29 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` A ) ) ) -> A. j e. ( 0 ..^ ( # ` A ) ) ( ( A ` i ) = ( A ` j ) -> i = j ) )
31 30 r19.21bi 
 |-  ( ( ( ph /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ` i ) = ( A ` j ) -> i = j ) )
32 31 adantllr 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ` i ) = ( A ` j ) -> i = j ) )
33 21 32 mpd 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> i = j )
34 33 ex 
 |-  ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( j e. ( 0 ..^ ( # ` A ) ) -> i = j ) )
35 34 adantllr 
 |-  ( ( ( ( ph /\ j e. dom ( A ++ B ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( j e. ( 0 ..^ ( # ` A ) ) -> i = j ) )
36 f1fun 
 |-  ( A : dom A -1-1-> S -> Fun A )
37 4 36 syl 
 |-  ( ph -> Fun A )
38 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` A ) ) ) -> i e. ( 0 ..^ ( # ` A ) ) )
39 23 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` A ) ) ) -> dom A = ( 0 ..^ ( # ` A ) ) )
40 38 39 eleqtrrd 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` A ) ) ) -> i e. dom A )
41 fvelrn 
 |-  ( ( Fun A /\ i e. dom A ) -> ( A ` i ) e. ran A )
42 37 40 41 syl2an2r 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` i ) e. ran A )
43 42 ad4ant13 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( A ` i ) e. ran A )
44 simpllr 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) )
45 15 ad4ant13 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) ` i ) = ( A ` i ) )
46 2 adantr 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> A e. Word S )
47 3 adantr 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> B e. Word S )
48 simpr 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) )
49 ccatlen 
 |-  ( ( A e. Word S /\ B e. Word S ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
50 2 3 49 syl2anc 
 |-  ( ph -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
51 50 oveq2d 
 |-  ( ph -> ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) = ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
52 51 adantr 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) = ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
53 48 52 eleqtrd 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> j e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
54 ccatval2 
 |-  ( ( A e. Word S /\ B e. Word S /\ j e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) -> ( ( A ++ B ) ` j ) = ( B ` ( j - ( # ` A ) ) ) )
55 46 47 53 54 syl3anc 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) ` j ) = ( B ` ( j - ( # ` A ) ) ) )
56 55 ad4ant14 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) ` j ) = ( B ` ( j - ( # ` A ) ) ) )
57 44 45 56 3eqtr3d 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( A ` i ) = ( B ` ( j - ( # ` A ) ) ) )
58 f1fun 
 |-  ( B : dom B -1-1-> S -> Fun B )
59 5 58 syl 
 |-  ( ph -> Fun B )
60 lencl 
 |-  ( B e. Word S -> ( # ` B ) e. NN0 )
61 3 60 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
62 61 nn0zd 
 |-  ( ph -> ( # ` B ) e. ZZ )
63 62 adantr 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( # ` B ) e. ZZ )
64 fzosubel3 
 |-  ( ( j e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) /\ ( # ` B ) e. ZZ ) -> ( j - ( # ` A ) ) e. ( 0 ..^ ( # ` B ) ) )
65 53 63 64 syl2anc 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( j - ( # ` A ) ) e. ( 0 ..^ ( # ` B ) ) )
66 wrddm 
 |-  ( B e. Word S -> dom B = ( 0 ..^ ( # ` B ) ) )
67 3 66 syl 
 |-  ( ph -> dom B = ( 0 ..^ ( # ` B ) ) )
68 67 adantr 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> dom B = ( 0 ..^ ( # ` B ) ) )
69 65 68 eleqtrrd 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( j - ( # ` A ) ) e. dom B )
70 fvelrn 
 |-  ( ( Fun B /\ ( j - ( # ` A ) ) e. dom B ) -> ( B ` ( j - ( # ` A ) ) ) e. ran B )
71 59 69 70 syl2an2r 
 |-  ( ( ph /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( B ` ( j - ( # ` A ) ) ) e. ran B )
72 71 ad4ant14 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( B ` ( j - ( # ` A ) ) ) e. ran B )
73 57 72 eqeltrd 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( A ` i ) e. ran B )
74 43 73 elind 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( A ` i ) e. ( ran A i^i ran B ) )
75 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ran A i^i ran B ) = (/) )
76 74 75 eleqtrd 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( A ` i ) e. (/) )
77 noel 
 |-  -. ( A ` i ) e. (/)
78 77 a1i 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> -. ( A ` i ) e. (/) )
79 76 78 pm2.21dd 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> i = j )
80 79 ex 
 |-  ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) -> i = j ) )
81 80 adantllr 
 |-  ( ( ( ( ph /\ j e. dom ( A ++ B ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) -> i = j ) )
82 wrddm 
 |-  ( ( A ++ B ) e. Word S -> dom ( A ++ B ) = ( 0 ..^ ( # ` ( A ++ B ) ) ) )
83 8 82 syl 
 |-  ( ph -> dom ( A ++ B ) = ( 0 ..^ ( # ` ( A ++ B ) ) ) )
84 83 eleq2d 
 |-  ( ph -> ( j e. dom ( A ++ B ) <-> j e. ( 0 ..^ ( # ` ( A ++ B ) ) ) ) )
85 84 biimpa 
 |-  ( ( ph /\ j e. dom ( A ++ B ) ) -> j e. ( 0 ..^ ( # ` ( A ++ B ) ) ) )
86 lencl 
 |-  ( A e. Word S -> ( # ` A ) e. NN0 )
87 2 86 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
88 87 nn0zd 
 |-  ( ph -> ( # ` A ) e. ZZ )
89 88 adantr 
 |-  ( ( ph /\ j e. dom ( A ++ B ) ) -> ( # ` A ) e. ZZ )
90 fzospliti 
 |-  ( ( j e. ( 0 ..^ ( # ` ( A ++ B ) ) ) /\ ( # ` A ) e. ZZ ) -> ( j e. ( 0 ..^ ( # ` A ) ) \/ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) )
91 85 89 90 syl2anc 
 |-  ( ( ph /\ j e. dom ( A ++ B ) ) -> ( j e. ( 0 ..^ ( # ` A ) ) \/ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) )
92 91 ad2antrr 
 |-  ( ( ( ( ph /\ j e. dom ( A ++ B ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( j e. ( 0 ..^ ( # ` A ) ) \/ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) )
93 35 81 92 mpjaod 
 |-  ( ( ( ( ph /\ j e. dom ( A ++ B ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> i = j )
94 93 ex 
 |-  ( ( ( ph /\ j e. dom ( A ++ B ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) -> ( i e. ( 0 ..^ ( # ` A ) ) -> i = j ) )
95 94 adantlrl 
 |-  ( ( ( ph /\ ( i e. dom ( A ++ B ) /\ j e. dom ( A ++ B ) ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) -> ( i e. ( 0 ..^ ( # ` A ) ) -> i = j ) )
96 simpr 
 |-  ( ( ph /\ j e. ( 0 ..^ ( # ` A ) ) ) -> j e. ( 0 ..^ ( # ` A ) ) )
97 23 adantr 
 |-  ( ( ph /\ j e. ( 0 ..^ ( # ` A ) ) ) -> dom A = ( 0 ..^ ( # ` A ) ) )
98 96 97 eleqtrrd 
 |-  ( ( ph /\ j e. ( 0 ..^ ( # ` A ) ) ) -> j e. dom A )
99 fvelrn 
 |-  ( ( Fun A /\ j e. dom A ) -> ( A ` j ) e. ran A )
100 37 98 99 syl2an2r 
 |-  ( ( ph /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` j ) e. ran A )
101 100 ad4ant14 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` j ) e. ran A )
102 simpllr 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) )
103 2 adantr 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> A e. Word S )
104 3 adantr 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> B e. Word S )
105 simpr 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) )
106 51 adantr 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) = ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
107 105 106 eleqtrd 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
108 ccatval2 
 |-  ( ( A e. Word S /\ B e. Word S /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) -> ( ( A ++ B ) ` i ) = ( B ` ( i - ( # ` A ) ) ) )
109 103 104 107 108 syl3anc 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) ` i ) = ( B ` ( i - ( # ` A ) ) ) )
110 109 ad4ant13 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` i ) = ( B ` ( i - ( # ` A ) ) ) )
111 19 ad4ant14 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` j ) = ( A ` j ) )
112 102 110 111 3eqtr3rd 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` j ) = ( B ` ( i - ( # ` A ) ) ) )
113 62 adantr 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( # ` B ) e. ZZ )
114 fzosubel3 
 |-  ( ( i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) /\ ( # ` B ) e. ZZ ) -> ( i - ( # ` A ) ) e. ( 0 ..^ ( # ` B ) ) )
115 107 113 114 syl2anc 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( i - ( # ` A ) ) e. ( 0 ..^ ( # ` B ) ) )
116 67 adantr 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> dom B = ( 0 ..^ ( # ` B ) ) )
117 115 116 eleqtrrd 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( i - ( # ` A ) ) e. dom B )
118 fvelrn 
 |-  ( ( Fun B /\ ( i - ( # ` A ) ) e. dom B ) -> ( B ` ( i - ( # ` A ) ) ) e. ran B )
119 59 117 118 syl2an2r 
 |-  ( ( ph /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( B ` ( i - ( # ` A ) ) ) e. ran B )
120 119 ad4ant13 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( B ` ( i - ( # ` A ) ) ) e. ran B )
121 112 120 eqeltrd 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` j ) e. ran B )
122 101 121 elind 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` j ) e. ( ran A i^i ran B ) )
123 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( ran A i^i ran B ) = (/) )
124 122 123 eleqtrd 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> ( A ` j ) e. (/) )
125 noel 
 |-  -. ( A ` j ) e. (/)
126 125 a1i 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> -. ( A ` j ) e. (/) )
127 124 126 pm2.21dd 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( 0 ..^ ( # ` A ) ) ) -> i = j )
128 127 ex 
 |-  ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( j e. ( 0 ..^ ( # ` A ) ) -> i = j ) )
129 128 adantllr 
 |-  ( ( ( ( ph /\ j e. dom ( A ++ B ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( j e. ( 0 ..^ ( # ` A ) ) -> i = j ) )
130 elfzoelz 
 |-  ( i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) -> i e. ZZ )
131 130 zcnd 
 |-  ( i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) -> i e. CC )
132 131 ad2antlr 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> i e. CC )
133 elfzoelz 
 |-  ( j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) -> j e. ZZ )
134 133 zcnd 
 |-  ( j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) -> j e. CC )
135 134 adantl 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> j e. CC )
136 87 nn0cnd 
 |-  ( ph -> ( # ` A ) e. CC )
137 136 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( # ` A ) e. CC )
138 5 ad3antrrr 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> B : dom B -1-1-> S )
139 117 ad4ant13 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( i - ( # ` A ) ) e. dom B )
140 69 ad4ant14 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( j - ( # ` A ) ) e. dom B )
141 139 140 jca 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( i - ( # ` A ) ) e. dom B /\ ( j - ( # ` A ) ) e. dom B ) )
142 simpllr 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) )
143 109 ad4ant13 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) ` i ) = ( B ` ( i - ( # ` A ) ) ) )
144 55 ad4ant14 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) ` j ) = ( B ` ( j - ( # ` A ) ) ) )
145 142 143 144 3eqtr3d 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( B ` ( i - ( # ` A ) ) ) = ( B ` ( j - ( # ` A ) ) ) )
146 f1veqaeq 
 |-  ( ( B : dom B -1-1-> S /\ ( ( i - ( # ` A ) ) e. dom B /\ ( j - ( # ` A ) ) e. dom B ) ) -> ( ( B ` ( i - ( # ` A ) ) ) = ( B ` ( j - ( # ` A ) ) ) -> ( i - ( # ` A ) ) = ( j - ( # ` A ) ) ) )
147 146 imp 
 |-  ( ( ( B : dom B -1-1-> S /\ ( ( i - ( # ` A ) ) e. dom B /\ ( j - ( # ` A ) ) e. dom B ) ) /\ ( B ` ( i - ( # ` A ) ) ) = ( B ` ( j - ( # ` A ) ) ) ) -> ( i - ( # ` A ) ) = ( j - ( # ` A ) ) )
148 138 141 145 147 syl21anc 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( i - ( # ` A ) ) = ( j - ( # ` A ) ) )
149 132 135 137 148 subcan2d 
 |-  ( ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) /\ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> i = j )
150 149 ex 
 |-  ( ( ( ph /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) -> i = j ) )
151 150 adantllr 
 |-  ( ( ( ( ph /\ j e. dom ( A ++ B ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) -> i = j ) )
152 91 ad2antrr 
 |-  ( ( ( ( ph /\ j e. dom ( A ++ B ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> ( j e. ( 0 ..^ ( # ` A ) ) \/ j e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) )
153 129 151 152 mpjaod 
 |-  ( ( ( ( ph /\ j e. dom ( A ++ B ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) /\ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) -> i = j )
154 153 ex 
 |-  ( ( ( ph /\ j e. dom ( A ++ B ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) -> ( i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) -> i = j ) )
155 154 adantlrl 
 |-  ( ( ( ph /\ ( i e. dom ( A ++ B ) /\ j e. dom ( A ++ B ) ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) -> ( i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) -> i = j ) )
156 83 eleq2d 
 |-  ( ph -> ( i e. dom ( A ++ B ) <-> i e. ( 0 ..^ ( # ` ( A ++ B ) ) ) ) )
157 156 biimpa 
 |-  ( ( ph /\ i e. dom ( A ++ B ) ) -> i e. ( 0 ..^ ( # ` ( A ++ B ) ) ) )
158 88 adantr 
 |-  ( ( ph /\ i e. dom ( A ++ B ) ) -> ( # ` A ) e. ZZ )
159 fzospliti 
 |-  ( ( i e. ( 0 ..^ ( # ` ( A ++ B ) ) ) /\ ( # ` A ) e. ZZ ) -> ( i e. ( 0 ..^ ( # ` A ) ) \/ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) )
160 157 158 159 syl2anc 
 |-  ( ( ph /\ i e. dom ( A ++ B ) ) -> ( i e. ( 0 ..^ ( # ` A ) ) \/ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) )
161 160 adantrr 
 |-  ( ( ph /\ ( i e. dom ( A ++ B ) /\ j e. dom ( A ++ B ) ) ) -> ( i e. ( 0 ..^ ( # ` A ) ) \/ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) )
162 161 adantr 
 |-  ( ( ( ph /\ ( i e. dom ( A ++ B ) /\ j e. dom ( A ++ B ) ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) -> ( i e. ( 0 ..^ ( # ` A ) ) \/ i e. ( ( # ` A ) ..^ ( # ` ( A ++ B ) ) ) ) )
163 95 155 162 mpjaod 
 |-  ( ( ( ph /\ ( i e. dom ( A ++ B ) /\ j e. dom ( A ++ B ) ) ) /\ ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) ) -> i = j )
164 163 ex 
 |-  ( ( ph /\ ( i e. dom ( A ++ B ) /\ j e. dom ( A ++ B ) ) ) -> ( ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) -> i = j ) )
165 164 ralrimivva 
 |-  ( ph -> A. i e. dom ( A ++ B ) A. j e. dom ( A ++ B ) ( ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) -> i = j ) )
166 dff13 
 |-  ( ( A ++ B ) : dom ( A ++ B ) -1-1-> S <-> ( ( A ++ B ) : dom ( A ++ B ) --> S /\ A. i e. dom ( A ++ B ) A. j e. dom ( A ++ B ) ( ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` j ) -> i = j ) ) )
167 11 165 166 sylanbrc 
 |-  ( ph -> ( A ++ B ) : dom ( A ++ B ) -1-1-> S )