Metamath Proof Explorer


Theorem numclwwlk1lem2foalem

Description: Lemma for numclwwlk1lem2foa . (Contributed by AV, 29-May-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Assertion numclwwlk1lem2foalem WWordVW=N2XVYVN3W++⟨“X”⟩++⟨“Y”⟩prefixN2=WW++⟨“X”⟩++⟨“Y”⟩N1=YW++⟨“X”⟩++⟨“Y”⟩N2=X

Proof

Step Hyp Ref Expression
1 simpl WWordVW=N2WWordV
2 s1cl XV⟨“X”⟩WordV
3 s1cl YV⟨“Y”⟩WordV
4 1 2 3 3anim123i WWordVW=N2XVYVWWordV⟨“X”⟩WordV⟨“Y”⟩WordV
5 4 3expb WWordVW=N2XVYVWWordV⟨“X”⟩WordV⟨“Y”⟩WordV
6 ccatass WWordV⟨“X”⟩WordV⟨“Y”⟩WordVW++⟨“X”⟩++⟨“Y”⟩=W++⟨“X”⟩++⟨“Y”⟩
7 5 6 syl WWordVW=N2XVYVW++⟨“X”⟩++⟨“Y”⟩=W++⟨“X”⟩++⟨“Y”⟩
8 7 oveq1d WWordVW=N2XVYVW++⟨“X”⟩++⟨“Y”⟩prefixN2=W++⟨“X”⟩++⟨“Y”⟩prefixN2
9 1 adantr WWordVW=N2XVYVWWordV
10 ccat2s1cl XVYV⟨“X”⟩++⟨“Y”⟩WordV
11 10 adantl WWordVW=N2XVYV⟨“X”⟩++⟨“Y”⟩WordV
12 simpr WWordVW=N2W=N2
13 12 eqcomd WWordVW=N2N2=W
14 13 adantr WWordVW=N2XVYVN2=W
15 pfxccatid WWordV⟨“X”⟩++⟨“Y”⟩WordVN2=WW++⟨“X”⟩++⟨“Y”⟩prefixN2=W
16 9 11 14 15 syl3anc WWordVW=N2XVYVW++⟨“X”⟩++⟨“Y”⟩prefixN2=W
17 8 16 eqtrd WWordVW=N2XVYVW++⟨“X”⟩++⟨“Y”⟩prefixN2=W
18 17 3adant3 WWordVW=N2XVYVN3W++⟨“X”⟩++⟨“Y”⟩prefixN2=W
19 1e2m1 1=21
20 19 oveq2i N1=N21
21 eluzelcn N3N
22 2cnd N32
23 1cnd N31
24 21 22 23 subsubd N3N21=N-2+1
25 20 24 eqtrid N3N1=N-2+1
26 25 3ad2ant3 WWordVW=N2XVYVN3N1=N-2+1
27 26 fveq2d WWordVW=N2XVYVN3W++⟨“X”⟩++⟨“Y”⟩N1=W++⟨“X”⟩++⟨“Y”⟩N-2+1
28 ccatw2s1p2 WWordVW=N2XVYVW++⟨“X”⟩++⟨“Y”⟩N-2+1=Y
29 28 3adant3 WWordVW=N2XVYVN3W++⟨“X”⟩++⟨“Y”⟩N-2+1=Y
30 27 29 eqtrd WWordVW=N2XVYVN3W++⟨“X”⟩++⟨“Y”⟩N1=Y
31 simpl XVYVXV
32 ccatw2s1p1 WWordVW=N2XVW++⟨“X”⟩++⟨“Y”⟩N2=X
33 1 12 31 32 syl2an3an WWordVW=N2XVYVW++⟨“X”⟩++⟨“Y”⟩N2=X
34 33 3adant3 WWordVW=N2XVYVN3W++⟨“X”⟩++⟨“Y”⟩N2=X
35 18 30 34 3jca WWordVW=N2XVYVN3W++⟨“X”⟩++⟨“Y”⟩prefixN2=WW++⟨“X”⟩++⟨“Y”⟩N1=YW++⟨“X”⟩++⟨“Y”⟩N2=X