Metamath Proof Explorer


Theorem ccatco

Description: Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion ccatco S Word A T Word A F : A B F S ++ T = F S ++ F T

Proof

Step Hyp Ref Expression
1 lenco S Word A F : A B F S = S
2 1 3adant2 S Word A T Word A F : A B F S = S
3 lenco T Word A F : A B F T = T
4 3 3adant1 S Word A T Word A F : A B F T = T
5 2 4 oveq12d S Word A T Word A F : A B F S + F T = S + T
6 5 oveq2d S Word A T Word A F : A B 0 ..^ F S + F T = 0 ..^ S + T
7 6 mpteq1d S Word A T Word A F : A B x 0 ..^ F S + F T if x 0 ..^ F S F S x F T x F S = x 0 ..^ S + T if x 0 ..^ F S F S x F T x F S
8 2 oveq2d S Word A T Word A F : A B 0 ..^ F S = 0 ..^ S
9 8 adantr S Word A T Word A F : A B x 0 ..^ S + T 0 ..^ F S = 0 ..^ S
10 9 eleq2d S Word A T Word A F : A B x 0 ..^ S + T x 0 ..^ F S x 0 ..^ S
11 10 ifbid S Word A T Word A F : A B x 0 ..^ S + T if x 0 ..^ F S F S x F T x F S = if x 0 ..^ S F S x F T x F S
12 wrdf S Word A S : 0 ..^ S A
13 12 3ad2ant1 S Word A T Word A F : A B S : 0 ..^ S A
14 13 adantr S Word A T Word A F : A B x 0 ..^ S + T S : 0 ..^ S A
15 14 ffnd S Word A T Word A F : A B x 0 ..^ S + T S Fn 0 ..^ S
16 fvco2 S Fn 0 ..^ S x 0 ..^ S F S x = F S x
17 15 16 sylan S Word A T Word A F : A B x 0 ..^ S + T x 0 ..^ S F S x = F S x
18 iftrue x 0 ..^ S if x 0 ..^ S F S x F T x S = F S x
19 18 adantl S Word A T Word A F : A B x 0 ..^ S + T x 0 ..^ S if x 0 ..^ S F S x F T x S = F S x
20 17 19 eqtr4d S Word A T Word A F : A B x 0 ..^ S + T x 0 ..^ S F S x = if x 0 ..^ S F S x F T x S
21 wrdf T Word A T : 0 ..^ T A
22 21 3ad2ant2 S Word A T Word A F : A B T : 0 ..^ T A
23 22 ad2antrr S Word A T Word A F : A B x 0 ..^ S + T ¬ x 0 ..^ S T : 0 ..^ T A
24 23 ffnd S Word A T Word A F : A B x 0 ..^ S + T ¬ x 0 ..^ S T Fn 0 ..^ T
25 lencl S Word A S 0
26 25 nn0zd S Word A S
27 26 3ad2ant1 S Word A T Word A F : A B S
28 fzospliti x 0 ..^ S + T S x 0 ..^ S x S ..^ S + T
29 28 ancoms S x 0 ..^ S + T x 0 ..^ S x S ..^ S + T
30 27 29 sylan S Word A T Word A F : A B x 0 ..^ S + T x 0 ..^ S x S ..^ S + T
31 30 orcanai S Word A T Word A F : A B x 0 ..^ S + T ¬ x 0 ..^ S x S ..^ S + T
32 lencl T Word A T 0
33 32 nn0zd T Word A T
34 33 3ad2ant2 S Word A T Word A F : A B T
35 34 ad2antrr S Word A T Word A F : A B x 0 ..^ S + T ¬ x 0 ..^ S T
36 fzosubel3 x S ..^ S + T T x S 0 ..^ T
37 31 35 36 syl2anc S Word A T Word A F : A B x 0 ..^ S + T ¬ x 0 ..^ S x S 0 ..^ T
38 fvco2 T Fn 0 ..^ T x S 0 ..^ T F T x S = F T x S
39 24 37 38 syl2anc S Word A T Word A F : A B x 0 ..^ S + T ¬ x 0 ..^ S F T x S = F T x S
40 2 oveq2d S Word A T Word A F : A B x F S = x S
41 40 fveq2d S Word A T Word A F : A B F T x F S = F T x S
42 41 ad2antrr S Word A T Word A F : A B x 0 ..^ S + T ¬ x 0 ..^ S F T x F S = F T x S
43 iffalse ¬ x 0 ..^ S if x 0 ..^ S F S x F T x S = F T x S
44 43 adantl S Word A T Word A F : A B x 0 ..^ S + T ¬ x 0 ..^ S if x 0 ..^ S F S x F T x S = F T x S
45 39 42 44 3eqtr4d S Word A T Word A F : A B x 0 ..^ S + T ¬ x 0 ..^ S F T x F S = if x 0 ..^ S F S x F T x S
46 20 45 ifeqda S Word A T Word A F : A B x 0 ..^ S + T if x 0 ..^ S F S x F T x F S = if x 0 ..^ S F S x F T x S
47 11 46 eqtrd S Word A T Word A F : A B x 0 ..^ S + T if x 0 ..^ F S F S x F T x F S = if x 0 ..^ S F S x F T x S
48 47 mpteq2dva S Word A T Word A F : A B x 0 ..^ S + T if x 0 ..^ F S F S x F T x F S = x 0 ..^ S + T if x 0 ..^ S F S x F T x S
49 7 48 eqtr2d S Word A T Word A F : A B x 0 ..^ S + T if x 0 ..^ S F S x F T x S = x 0 ..^ F S + F T if x 0 ..^ F S F S x F T x F S
50 14 ffvelrnda S Word A T Word A F : A B x 0 ..^ S + T x 0 ..^ S S x A
51 23 37 ffvelrnd S Word A T Word A F : A B x 0 ..^ S + T ¬ x 0 ..^ S T x S A
52 50 51 ifclda S Word A T Word A F : A B x 0 ..^ S + T if x 0 ..^ S S x T x S A
53 ccatfval S Word A T Word A S ++ T = x 0 ..^ S + T if x 0 ..^ S S x T x S
54 53 3adant3 S Word A T Word A F : A B S ++ T = x 0 ..^ S + T if x 0 ..^ S S x T x S
55 simp3 S Word A T Word A F : A B F : A B
56 55 feqmptd S Word A T Word A F : A B F = y A F y
57 fveq2 y = if x 0 ..^ S S x T x S F y = F if x 0 ..^ S S x T x S
58 fvif F if x 0 ..^ S S x T x S = if x 0 ..^ S F S x F T x S
59 57 58 eqtrdi y = if x 0 ..^ S S x T x S F y = if x 0 ..^ S F S x F T x S
60 52 54 56 59 fmptco S Word A T Word A F : A B F S ++ T = x 0 ..^ S + T if x 0 ..^ S F S x F T x S
61 ffun F : A B Fun F
62 61 3ad2ant3 S Word A T Word A F : A B Fun F
63 simp1 S Word A T Word A F : A B S Word A
64 cofunexg Fun F S Word A F S V
65 62 63 64 syl2anc S Word A T Word A F : A B F S V
66 simp2 S Word A T Word A F : A B T Word A
67 cofunexg Fun F T Word A F T V
68 62 66 67 syl2anc S Word A T Word A F : A B F T V
69 ccatfval F S V F T V F S ++ F T = x 0 ..^ F S + F T if x 0 ..^ F S F S x F T x F S
70 65 68 69 syl2anc S Word A T Word A F : A B F S ++ F T = x 0 ..^ F S + F T if x 0 ..^ F S F S x F T x F S
71 49 60 70 3eqtr4d S Word A T Word A F : A B F S ++ T = F S ++ F T