Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ccatopth Unicode version

Theorem ccatopth 12695
 Description: An opth 4726-like theorem for recovering the two halves of a concatenated word. (Contributed by Mario Carneiro, 1-Oct-2015.)
Assertion
Ref Expression
ccatopth

Proof of Theorem ccatopth
StepHypRef Expression
1 oveq1 6303 . . . 4
2 swrdccat1 12682 . . . . . 6
323ad2ant1 1017 . . . . 5
4 simp3 998 . . . . . . . 8
54opeq2d 4224 . . . . . . 7
65oveq2d 6312 . . . . . 6
7 swrdccat1 12682 . . . . . . 7
873ad2ant2 1018 . . . . . 6
96, 8eqtrd 2498 . . . . 5
103, 9eqeq12d 2479 . . . 4
111, 10syl5ib 219 . . 3
12 simpr 461 . . . . . 6
13 simpl3 1001 . . . . . . 7
1412fveq2d 5875 . . . . . . . 8
15 simpl1 999 . . . . . . . . 9
16 ccatlen 12594 . . . . . . . . 9
1715, 16syl 16 . . . . . . . 8
18 simpl2 1000 . . . . . . . . 9
19 ccatlen 12594 . . . . . . . . 9
2018, 19syl 16 . . . . . . . 8
2114, 17, 203eqtr3d 2506 . . . . . . 7
2213, 21opeq12d 4225 . . . . . 6
2312, 22oveq12d 6314 . . . . 5
24 swrdccat2 12683 . . . . . 6
2515, 24syl 16 . . . . 5
26 swrdccat2 12683 . . . . . 6
2718, 26syl 16 . . . . 5
2823, 25, 273eqtr3d 2506 . . . 4
2928ex 434 . . 3