This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pfxccat3a

Description: A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018) (Revised by AV, 10-May-2020)

Ref Expression
Hypotheses swrdccatin2.l 
|- L = ( # ` A )
pfxccatpfx2.m 
|- M = ( # ` B )
Assertion pfxccat3a 
|- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( L + M ) ) -> ( ( A ++ B ) prefix N ) = if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 pfxccatpfx2.m 
 |-  M = ( # ` B )
3 simprl 
 |-  ( ( N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> ( A e. Word V /\ B e. Word V ) )
4 elfznn0 
 |-  ( N e. ( 0 ... ( L + M ) ) -> N e. NN0 )
5 4 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) -> N e. NN0 )
6 5 adantl 
 |-  ( ( N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> N e. NN0 )
7 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
8 1 7 eqeltrid 
 |-  ( A e. Word V -> L e. NN0 )
9 8 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> L e. NN0 )
10 9 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) -> L e. NN0 )
11 10 adantl 
 |-  ( ( N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> L e. NN0 )
12 simpl 
 |-  ( ( N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> N <_ L )
13 elfz2nn0 
 |-  ( N e. ( 0 ... L ) <-> ( N e. NN0 /\ L e. NN0 /\ N <_ L ) )
14 6 11 12 13 syl3anbrc 
 |-  ( ( N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> N e. ( 0 ... L ) )
15 df-3an 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) <-> ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... L ) ) )
16 3 14 15 sylanbrc 
 |-  ( ( N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) )
17 1 pfxccatpfx1 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) )
18 16 17 syl 
 |-  ( ( N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) )
19 iftrue 
 |-  ( N <_ L -> if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) = ( A prefix N ) )
20 19 adantr 
 |-  ( ( N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) = ( A prefix N ) )
21 18 20 eqtr4d 
 |-  ( ( N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> ( ( A ++ B ) prefix N ) = if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) )
22 simprl 
 |-  ( ( -. N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> ( A e. Word V /\ B e. Word V ) )
23 elfz2nn0 
 |-  ( N e. ( 0 ... ( L + M ) ) <-> ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) )
24 1 eleq1i 
 |-  ( L e. NN0 <-> ( # ` A ) e. NN0 )
25 nn0ltp1le 
 |-  ( ( L e. NN0 /\ N e. NN0 ) -> ( L < N <-> ( L + 1 ) <_ N ) )
26 nn0re 
 |-  ( L e. NN0 -> L e. RR )
27 nn0re 
 |-  ( N e. NN0 -> N e. RR )
28 ltnle 
 |-  ( ( L e. RR /\ N e. RR ) -> ( L < N <-> -. N <_ L ) )
29 26 27 28 syl2an 
 |-  ( ( L e. NN0 /\ N e. NN0 ) -> ( L < N <-> -. N <_ L ) )
30 25 29 bitr3d 
 |-  ( ( L e. NN0 /\ N e. NN0 ) -> ( ( L + 1 ) <_ N <-> -. N <_ L ) )
31 30 3ad2antr1 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) -> ( ( L + 1 ) <_ N <-> -. N <_ L ) )
32 simpr3 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) -> N <_ ( L + M ) )
33 32 anim1ci 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) /\ ( L + 1 ) <_ N ) -> ( ( L + 1 ) <_ N /\ N <_ ( L + M ) ) )
34 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
35 34 3ad2ant1 
 |-  ( ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) -> N e. ZZ )
36 35 adantl 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) -> N e. ZZ )
37 36 adantr 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) /\ ( L + 1 ) <_ N ) -> N e. ZZ )
38 peano2nn0 
 |-  ( L e. NN0 -> ( L + 1 ) e. NN0 )
39 38 nn0zd 
 |-  ( L e. NN0 -> ( L + 1 ) e. ZZ )
40 39 adantr 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) -> ( L + 1 ) e. ZZ )
41 40 adantr 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) /\ ( L + 1 ) <_ N ) -> ( L + 1 ) e. ZZ )
42 nn0z 
 |-  ( ( L + M ) e. NN0 -> ( L + M ) e. ZZ )
43 42 3ad2ant2 
 |-  ( ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) -> ( L + M ) e. ZZ )
44 43 adantl 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) -> ( L + M ) e. ZZ )
45 44 adantr 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) /\ ( L + 1 ) <_ N ) -> ( L + M ) e. ZZ )
46 elfz 
 |-  ( ( N e. ZZ /\ ( L + 1 ) e. ZZ /\ ( L + M ) e. ZZ ) -> ( N e. ( ( L + 1 ) ... ( L + M ) ) <-> ( ( L + 1 ) <_ N /\ N <_ ( L + M ) ) ) )
47 37 41 45 46 syl3anc 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) /\ ( L + 1 ) <_ N ) -> ( N e. ( ( L + 1 ) ... ( L + M ) ) <-> ( ( L + 1 ) <_ N /\ N <_ ( L + M ) ) ) )
48 33 47 mpbird 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) /\ ( L + 1 ) <_ N ) -> N e. ( ( L + 1 ) ... ( L + M ) ) )
49 48 ex 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) -> ( ( L + 1 ) <_ N -> N e. ( ( L + 1 ) ... ( L + M ) ) ) )
50 31 49 sylbird 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) ) -> ( -. N <_ L -> N e. ( ( L + 1 ) ... ( L + M ) ) ) )
51 50 ex 
 |-  ( L e. NN0 -> ( ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) -> ( -. N <_ L -> N e. ( ( L + 1 ) ... ( L + M ) ) ) ) )
52 24 51 sylbir 
 |-  ( ( # ` A ) e. NN0 -> ( ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) -> ( -. N <_ L -> N e. ( ( L + 1 ) ... ( L + M ) ) ) ) )
53 7 52 syl 
 |-  ( A e. Word V -> ( ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) -> ( -. N <_ L -> N e. ( ( L + 1 ) ... ( L + M ) ) ) ) )
54 53 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( N e. NN0 /\ ( L + M ) e. NN0 /\ N <_ ( L + M ) ) -> ( -. N <_ L -> N e. ( ( L + 1 ) ... ( L + M ) ) ) ) )
55 23 54 biimtrid 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( L + M ) ) -> ( -. N <_ L -> N e. ( ( L + 1 ) ... ( L + M ) ) ) ) )
56 55 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) -> ( -. N <_ L -> N e. ( ( L + 1 ) ... ( L + M ) ) ) )
57 56 impcom 
 |-  ( ( -. N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> N e. ( ( L + 1 ) ... ( L + M ) ) )
58 df-3an 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) <-> ( ( A e. Word V /\ B e. Word V ) /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) )
59 22 57 58 sylanbrc 
 |-  ( ( -. N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) )
60 1 2 pfxccatpfx2 
 |-  ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( A ++ ( B prefix ( N - L ) ) ) )
61 59 60 syl 
 |-  ( ( -. N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> ( ( A ++ B ) prefix N ) = ( A ++ ( B prefix ( N - L ) ) ) )
62 iffalse 
 |-  ( -. N <_ L -> if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) = ( A ++ ( B prefix ( N - L ) ) ) )
63 62 adantr 
 |-  ( ( -. N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) = ( A ++ ( B prefix ( N - L ) ) ) )
64 61 63 eqtr4d 
 |-  ( ( -. N <_ L /\ ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) ) -> ( ( A ++ B ) prefix N ) = if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) )
65 21 64 pm2.61ian 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) )
66 65 ex 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( L + M ) ) -> ( ( A ++ B ) prefix N ) = if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) ) )