Proof of Theorem ccatopth
Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . 4
⊢ ((𝐴 ++ 𝐵) = (𝐶 ++ 𝐷) → ((𝐴 ++ 𝐵) substr 〈0, (#‘𝐴)〉) = ((𝐶 ++ 𝐷) substr 〈0, (#‘𝐴)〉)) |
2 | | swrdccat1 13457 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) → ((𝐴 ++ 𝐵) substr 〈0, (#‘𝐴)〉) = 𝐴) |
3 | 2 | 3ad2ant1 1082 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → ((𝐴 ++ 𝐵) substr 〈0, (#‘𝐴)〉) = 𝐴) |
4 | | simp3 1063 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → (#‘𝐴) = (#‘𝐶)) |
5 | 4 | opeq2d 4409 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → 〈0, (#‘𝐴)〉 = 〈0,
(#‘𝐶)〉) |
6 | 5 | oveq2d 6666 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → ((𝐶 ++ 𝐷) substr 〈0, (#‘𝐴)〉) = ((𝐶 ++ 𝐷) substr 〈0, (#‘𝐶)〉)) |
7 | | swrdccat1 13457 |
. . . . . . 7
⊢ ((𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) → ((𝐶 ++ 𝐷) substr 〈0, (#‘𝐶)〉) = 𝐶) |
8 | 7 | 3ad2ant2 1083 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → ((𝐶 ++ 𝐷) substr 〈0, (#‘𝐶)〉) = 𝐶) |
9 | 6, 8 | eqtrd 2656 |
. . . . 5
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → ((𝐶 ++ 𝐷) substr 〈0, (#‘𝐴)〉) = 𝐶) |
10 | 3, 9 | eqeq12d 2637 |
. . . 4
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → (((𝐴 ++ 𝐵) substr 〈0, (#‘𝐴)〉) = ((𝐶 ++ 𝐷) substr 〈0, (#‘𝐴)〉) ↔ 𝐴 = 𝐶)) |
11 | 1, 10 | syl5ib 234 |
. . 3
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → ((𝐴 ++ 𝐵) = (𝐶 ++ 𝐷) → 𝐴 = 𝐶)) |
12 | | simpr 477 |
. . . . . 6
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) |
13 | | simpl3 1066 |
. . . . . . 7
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → (#‘𝐴) = (#‘𝐶)) |
14 | 12 | fveq2d 6195 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → (#‘(𝐴 ++ 𝐵)) = (#‘(𝐶 ++ 𝐷))) |
15 | | simpl1 1064 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → (𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋)) |
16 | | ccatlen 13360 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) → (#‘(𝐴 ++ 𝐵)) = ((#‘𝐴) + (#‘𝐵))) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → (#‘(𝐴 ++ 𝐵)) = ((#‘𝐴) + (#‘𝐵))) |
18 | | simpl2 1065 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋)) |
19 | | ccatlen 13360 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) → (#‘(𝐶 ++ 𝐷)) = ((#‘𝐶) + (#‘𝐷))) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → (#‘(𝐶 ++ 𝐷)) = ((#‘𝐶) + (#‘𝐷))) |
21 | 14, 17, 20 | 3eqtr3d 2664 |
. . . . . . 7
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → ((#‘𝐴) + (#‘𝐵)) = ((#‘𝐶) + (#‘𝐷))) |
22 | 13, 21 | opeq12d 4410 |
. . . . . 6
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → 〈(#‘𝐴), ((#‘𝐴) + (#‘𝐵))〉 = 〈(#‘𝐶), ((#‘𝐶) + (#‘𝐷))〉) |
23 | 12, 22 | oveq12d 6668 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → ((𝐴 ++ 𝐵) substr 〈(#‘𝐴), ((#‘𝐴) + (#‘𝐵))〉) = ((𝐶 ++ 𝐷) substr 〈(#‘𝐶), ((#‘𝐶) + (#‘𝐷))〉)) |
24 | | swrdccat2 13458 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) → ((𝐴 ++ 𝐵) substr 〈(#‘𝐴), ((#‘𝐴) + (#‘𝐵))〉) = 𝐵) |
25 | 15, 24 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → ((𝐴 ++ 𝐵) substr 〈(#‘𝐴), ((#‘𝐴) + (#‘𝐵))〉) = 𝐵) |
26 | | swrdccat2 13458 |
. . . . . 6
⊢ ((𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) → ((𝐶 ++ 𝐷) substr 〈(#‘𝐶), ((#‘𝐶) + (#‘𝐷))〉) = 𝐷) |
27 | 18, 26 | syl 17 |
. . . . 5
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → ((𝐶 ++ 𝐷) substr 〈(#‘𝐶), ((#‘𝐶) + (#‘𝐷))〉) = 𝐷) |
28 | 23, 25, 27 | 3eqtr3d 2664 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) ∧ (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) → 𝐵 = 𝐷) |
29 | 28 | ex 450 |
. . 3
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → ((𝐴 ++ 𝐵) = (𝐶 ++ 𝐷) → 𝐵 = 𝐷)) |
30 | 11, 29 | jcad 555 |
. 2
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → ((𝐴 ++ 𝐵) = (𝐶 ++ 𝐷) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
31 | | oveq12 6659 |
. 2
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐴 ++ 𝐵) = (𝐶 ++ 𝐷)) |
32 | 30, 31 | impbid1 215 |
1
⊢ (((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑋) ∧ (𝐶 ∈ Word 𝑋 ∧ 𝐷 ∈ Word 𝑋) ∧ (#‘𝐴) = (#‘𝐶)) → ((𝐴 ++ 𝐵) = (𝐶 ++ 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |