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

Metamath Proof Explorer

Theorem pfxccatin12lem2c

Description: Lemma for pfxccatin12lem2 and pfxccatin12lem3 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 27-May-2018)

Ref

Expression

Hypothesis

swrdccatin2.l

|- L = ( # ` A )

Assertion

pfxccatin12lem2c

|- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		swrdccatin2.l	\|- L = ( # ` A )
2		ccatcl	\|- ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) e. Word V )
3	2	adantr	\|- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( A ++ B ) e. Word V )
4		elfz0fzfz0	\|- ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> M e. ( 0 ... N ) )
5	4	adantl	\|- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> M e. ( 0 ... N ) )
6		elfzuz2	\|- ( M e. ( 0 ... L ) -> L e. ( ZZ>= ` 0 ) )
7		fzss1	\|- ( L e. ( ZZ>= ` 0 ) -> ( L ... ( L + ( # ` B ) ) ) C_ ( 0 ... ( L + ( # ` B ) ) ) )
8	6 7	syl	\|- ( M e. ( 0 ... L ) -> ( L ... ( L + ( # ` B ) ) ) C_ ( 0 ... ( L + ( # ` B ) ) ) )
9	8	sselda	\|- ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> N e. ( 0 ... ( L + ( # ` B ) ) ) )
10		ccatlen	\|- ( ( A e. Word V /\ B e. Word V ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
11	1	oveq1i	\|- ( L + ( # ` B ) ) = ( ( # ` A ) + ( # ` B ) )
12	10 11	eqtr4di	\|- ( ( A e. Word V /\ B e. Word V ) -> ( # ` ( A ++ B ) ) = ( L + ( # ` B ) ) )
13	12	oveq2d	\|- ( ( A e. Word V /\ B e. Word V ) -> ( 0 ... ( # ` ( A ++ B ) ) ) = ( 0 ... ( L + ( # ` B ) ) ) )
14	13	eleq2d	\|- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` ( A ++ B ) ) ) <-> N e. ( 0 ... ( L + ( # ` B ) ) ) ) )
15	9 14	imbitrrid	\|- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )
16	15	imp	\|- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) )
17	3 5 16	3jca	\|- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )