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 Word V B Word V M 0 L N L L + B A ++ B Word V M 0 N N 0 A ++ B

Proof

Step Hyp Ref Expression
1 swrdccatin2.l L = A
2 ccatcl A Word V B Word V A ++ B Word V
3 2 adantr A Word V B Word V M 0 L N L L + B A ++ B Word V
4 elfz0fzfz0 M 0 L N L L + B M 0 N
5 4 adantl A Word V B Word V M 0 L N L L + B M 0 N
6 elfzuz2 M 0 L L 0
7 fzss1 L 0 L L + B 0 L + B
8 6 7 syl M 0 L L L + B 0 L + B
9 8 sselda M 0 L N L L + B N 0 L + B
10 ccatlen A Word V B Word V A ++ B = A + B
11 1 oveq1i L + B = A + B
12 10 11 eqtr4di A Word V B Word V A ++ B = L + B
13 12 oveq2d A Word V B Word V 0 A ++ B = 0 L + B
14 13 eleq2d A Word V B Word V N 0 A ++ B N 0 L + B
15 9 14 syl5ibr A Word V B Word V M 0 L N L L + B N 0 A ++ B
16 15 imp A Word V B Word V M 0 L N L L + B N 0 A ++ B
17 3 5 16 3jca A Word V B Word V M 0 L N L L + B A ++ B Word V M 0 N N 0 A ++ B