Step | Hyp | Ref
| Expression |
1 | | uzp1 11721 |
. 2
⊢ (𝑃 ∈
(ℤ≥‘𝑄) → (𝑃 = 𝑄 ∨ 𝑃 ∈ (ℤ≥‘(𝑄 + 1)))) |
2 | | efgredlemb.8 |
. . . . . 6
⊢ (𝜑 → ¬ (𝐴‘𝐾) = (𝐵‘𝐿)) |
3 | | efgval.w |
. . . . . . . . . . 11
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
4 | | fviss 6256 |
. . . . . . . . . . 11
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
5 | 3, 4 | eqsstri 3635 |
. . . . . . . . . 10
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
6 | | efgredlem.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ dom 𝑆) |
7 | | efgval.r |
. . . . . . . . . . . . . . 15
⊢ ∼ = (
~FG ‘𝐼) |
8 | | efgval2.m |
. . . . . . . . . . . . . . 15
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
9 | | efgval2.t |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
10 | | efgred.d |
. . . . . . . . . . . . . . 15
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
11 | | efgred.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) |
12 | 3, 7, 8, 9, 10, 11 | efgsdm 18143 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom 𝑆 ↔ (𝐴 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐴‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐴))(𝐴‘𝑖) ∈ ran (𝑇‘(𝐴‘(𝑖 − 1))))) |
13 | 12 | simp1bi 1076 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom 𝑆 → 𝐴 ∈ (Word 𝑊 ∖ {∅})) |
14 | 6, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ (Word 𝑊 ∖ {∅})) |
15 | | eldifi 3732 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (Word 𝑊 ∖ {∅}) → 𝐴 ∈ Word 𝑊) |
16 | | wrdf 13310 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑊 → 𝐴:(0..^(#‘𝐴))⟶𝑊) |
17 | 14, 15, 16 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴:(0..^(#‘𝐴))⟶𝑊) |
18 | | fzossfz 12488 |
. . . . . . . . . . . . 13
⊢
(0..^((#‘𝐴)
− 1)) ⊆ (0...((#‘𝐴) − 1)) |
19 | | efgredlemb.k |
. . . . . . . . . . . . . 14
⊢ 𝐾 = (((#‘𝐴) − 1) − 1) |
20 | | efgredlem.1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
21 | | efgredlem.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ dom 𝑆) |
22 | | efgredlem.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑆‘𝐴) = (𝑆‘𝐵)) |
23 | | efgredlem.5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ (𝐴‘0) = (𝐵‘0)) |
24 | 3, 7, 8, 9, 10, 11, 20, 6, 21, 22, 23 | efgredlema 18153 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((#‘𝐴) − 1) ∈ ℕ
∧ ((#‘𝐵) −
1) ∈ ℕ)) |
25 | 24 | simpld 475 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((#‘𝐴) − 1) ∈
ℕ) |
26 | | fzo0end 12560 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐴)
− 1) ∈ ℕ → (((#‘𝐴) − 1) − 1) ∈
(0..^((#‘𝐴) −
1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((#‘𝐴) − 1) − 1) ∈
(0..^((#‘𝐴) −
1))) |
28 | 19, 27 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ (0..^((#‘𝐴) − 1))) |
29 | 18, 28 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ (0...((#‘𝐴) − 1))) |
30 | | lencl 13324 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Word 𝑊 → (#‘𝐴) ∈
ℕ0) |
31 | 14, 15, 30 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (#‘𝐴) ∈
ℕ0) |
32 | 31 | nn0zd 11480 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (#‘𝐴) ∈ ℤ) |
33 | | fzoval 12471 |
. . . . . . . . . . . . 13
⊢
((#‘𝐴) ∈
ℤ → (0..^(#‘𝐴)) = (0...((#‘𝐴) − 1))) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0..^(#‘𝐴)) = (0...((#‘𝐴) − 1))) |
35 | 29, 34 | eleqtrrd 2704 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ (0..^(#‘𝐴))) |
36 | 17, 35 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴‘𝐾) ∈ 𝑊) |
37 | 5, 36 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴‘𝐾) ∈ Word (𝐼 ×
2𝑜)) |
38 | | efgredlemb.p |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) |
39 | | elfzuz 12338 |
. . . . . . . . . 10
⊢ (𝑃 ∈ (0...(#‘(𝐴‘𝐾))) → 𝑃 ∈
(ℤ≥‘0)) |
40 | | eluzfz1 12348 |
. . . . . . . . . 10
⊢ (𝑃 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑃)) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (0...𝑃)) |
42 | | lencl 13324 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
(#‘(𝐴‘𝐾)) ∈
ℕ0) |
43 | 37, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈
ℕ0) |
44 | | nn0uz 11722 |
. . . . . . . . . . 11
⊢
ℕ0 = (ℤ≥‘0) |
45 | 43, 44 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈
(ℤ≥‘0)) |
46 | | eluzfz2 12349 |
. . . . . . . . . 10
⊢
((#‘(𝐴‘𝐾)) ∈ (ℤ≥‘0)
→ (#‘(𝐴‘𝐾)) ∈ (0...(#‘(𝐴‘𝐾)))) |
47 | 45, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (#‘(𝐴‘𝐾)) ∈ (0...(#‘(𝐴‘𝐾)))) |
48 | | ccatswrd 13456 |
. . . . . . . . 9
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧ (0
∈ (0...𝑃) ∧ 𝑃 ∈ (0...(#‘(𝐴‘𝐾))) ∧ (#‘(𝐴‘𝐾)) ∈ (0...(#‘(𝐴‘𝐾))))) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) substr 〈0, (#‘(𝐴‘𝐾))〉)) |
49 | 37, 41, 38, 47, 48 | syl13anc 1328 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐴‘𝐾) substr 〈0, (#‘(𝐴‘𝐾))〉)) |
50 | | swrdid 13428 |
. . . . . . . . 9
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈0, (#‘(𝐴‘𝐾))〉) = (𝐴‘𝐾)) |
51 | 37, 50 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈0, (#‘(𝐴‘𝐾))〉) = (𝐴‘𝐾)) |
52 | 49, 51 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (𝐴‘𝐾)) |
53 | 3, 7, 8, 9, 10, 11 | efgsdm 18143 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ dom 𝑆 ↔ (𝐵 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐵‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝐵))(𝐵‘𝑖) ∈ ran (𝑇‘(𝐵‘(𝑖 − 1))))) |
54 | 53 | simp1bi 1076 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ dom 𝑆 → 𝐵 ∈ (Word 𝑊 ∖ {∅})) |
55 | 21, 54 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ (Word 𝑊 ∖ {∅})) |
56 | | eldifi 3732 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (Word 𝑊 ∖ {∅}) → 𝐵 ∈ Word 𝑊) |
57 | | wrdf 13310 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Word 𝑊 → 𝐵:(0..^(#‘𝐵))⟶𝑊) |
58 | 55, 56, 57 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵:(0..^(#‘𝐵))⟶𝑊) |
59 | | fzossfz 12488 |
. . . . . . . . . . . . 13
⊢
(0..^((#‘𝐵)
− 1)) ⊆ (0...((#‘𝐵) − 1)) |
60 | | efgredlemb.l |
. . . . . . . . . . . . . 14
⊢ 𝐿 = (((#‘𝐵) − 1) − 1) |
61 | 24 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((#‘𝐵) − 1) ∈
ℕ) |
62 | | fzo0end 12560 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐵)
− 1) ∈ ℕ → (((#‘𝐵) − 1) − 1) ∈
(0..^((#‘𝐵) −
1))) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((#‘𝐵) − 1) − 1) ∈
(0..^((#‘𝐵) −
1))) |
64 | 60, 63 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ (0..^((#‘𝐵) − 1))) |
65 | 59, 64 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐿 ∈ (0...((#‘𝐵) − 1))) |
66 | | lencl 13324 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ Word 𝑊 → (#‘𝐵) ∈
ℕ0) |
67 | 55, 56, 66 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (#‘𝐵) ∈
ℕ0) |
68 | 67 | nn0zd 11480 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (#‘𝐵) ∈ ℤ) |
69 | | fzoval 12471 |
. . . . . . . . . . . . 13
⊢
((#‘𝐵) ∈
ℤ → (0..^(#‘𝐵)) = (0...((#‘𝐵) − 1))) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0..^(#‘𝐵)) = (0...((#‘𝐵) − 1))) |
71 | 65, 70 | eleqtrrd 2704 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈ (0..^(#‘𝐵))) |
72 | 58, 71 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵‘𝐿) ∈ 𝑊) |
73 | 5, 72 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵‘𝐿) ∈ Word (𝐼 ×
2𝑜)) |
74 | | efgredlemb.q |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) |
75 | | elfzuz 12338 |
. . . . . . . . . 10
⊢ (𝑄 ∈ (0...(#‘(𝐵‘𝐿))) → 𝑄 ∈
(ℤ≥‘0)) |
76 | | eluzfz1 12348 |
. . . . . . . . . 10
⊢ (𝑄 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑄)) |
77 | 74, 75, 76 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ (0...𝑄)) |
78 | | lencl 13324 |
. . . . . . . . . . . 12
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
(#‘(𝐵‘𝐿)) ∈
ℕ0) |
79 | 73, 78 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘(𝐵‘𝐿)) ∈
ℕ0) |
80 | 79, 44 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘(𝐵‘𝐿)) ∈
(ℤ≥‘0)) |
81 | | eluzfz2 12349 |
. . . . . . . . . 10
⊢
((#‘(𝐵‘𝐿)) ∈ (ℤ≥‘0)
→ (#‘(𝐵‘𝐿)) ∈ (0...(#‘(𝐵‘𝐿)))) |
82 | 80, 81 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (#‘(𝐵‘𝐿)) ∈ (0...(#‘(𝐵‘𝐿)))) |
83 | | ccatswrd 13456 |
. . . . . . . . 9
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧ (0
∈ (0...𝑄) ∧ 𝑄 ∈ (0...(#‘(𝐵‘𝐿))) ∧ (#‘(𝐵‘𝐿)) ∈ (0...(#‘(𝐵‘𝐿))))) → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈0, (#‘(𝐵‘𝐿))〉)) |
84 | 73, 77, 74, 82, 83 | syl13anc 1328 |
. . . . . . . 8
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) = ((𝐵‘𝐿) substr 〈0, (#‘(𝐵‘𝐿))〉)) |
85 | | swrdid 13428 |
. . . . . . . . 9
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈0, (#‘(𝐵‘𝐿))〉) = (𝐵‘𝐿)) |
86 | 73, 85 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈0, (#‘(𝐵‘𝐿))〉) = (𝐵‘𝐿)) |
87 | 84, 86 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) = (𝐵‘𝐿)) |
88 | 52, 87 | eqeq12d 2637 |
. . . . . 6
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) ↔ (𝐴‘𝐾) = (𝐵‘𝐿))) |
89 | 2, 88 | mtbird 315 |
. . . . 5
⊢ (𝜑 → ¬ (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
90 | | efgredlemb.6 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) |
91 | | efgredlemb.u |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ∈ (𝐼 ×
2𝑜)) |
92 | 3, 7, 8, 9 | efgtval 18136 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ 𝑃 ∈ (0...(#‘(𝐴‘𝐾))) ∧ 𝑈 ∈ (𝐼 × 2𝑜)) →
(𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉)) |
93 | 36, 38, 91, 92 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃(𝑇‘(𝐴‘𝐾))𝑈) = ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉)) |
94 | 8 | efgmf 18126 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜) |
95 | 94 | ffvelrni 6358 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ (𝐼 × 2𝑜) →
(𝑀‘𝑈) ∈ (𝐼 ×
2𝑜)) |
96 | 91, 95 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀‘𝑈) ∈ (𝐼 ×
2𝑜)) |
97 | 91, 96 | s2cld 13616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 ×
2𝑜)) |
98 | | splval 13502 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝐾) ∈ 𝑊 ∧ (𝑃 ∈ (0...(#‘(𝐴‘𝐾))) ∧ 𝑃 ∈ (0...(#‘(𝐴‘𝐾))) ∧ 〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 ×
2𝑜))) → ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) |
99 | 36, 38, 38, 97, 98 | syl13anc 1328 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) splice 〈𝑃, 𝑃, 〈“𝑈(𝑀‘𝑈)”〉〉) = ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) |
100 | 90, 93, 99 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘𝐴) = ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) |
101 | | efgredlemb.7 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) |
102 | | efgredlemb.v |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑉 ∈ (𝐼 ×
2𝑜)) |
103 | 3, 7, 8, 9 | efgtval 18136 |
. . . . . . . . . . . . . 14
⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ 𝑄 ∈ (0...(#‘(𝐵‘𝐿))) ∧ 𝑉 ∈ (𝐼 × 2𝑜)) →
(𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) |
104 | 72, 74, 102, 103 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄(𝑇‘(𝐵‘𝐿))𝑉) = ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉)) |
105 | 94 | ffvelrni 6358 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 ∈ (𝐼 × 2𝑜) →
(𝑀‘𝑉) ∈ (𝐼 ×
2𝑜)) |
106 | 102, 105 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀‘𝑉) ∈ (𝐼 ×
2𝑜)) |
107 | 102, 106 | s2cld 13616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 ×
2𝑜)) |
108 | | splval 13502 |
. . . . . . . . . . . . . 14
⊢ (((𝐵‘𝐿) ∈ 𝑊 ∧ (𝑄 ∈ (0...(#‘(𝐵‘𝐿))) ∧ 𝑄 ∈ (0...(#‘(𝐵‘𝐿))) ∧ 〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 ×
2𝑜))) → ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
109 | 72, 74, 74, 107, 108 | syl13anc 1328 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵‘𝐿) splice 〈𝑄, 𝑄, 〈“𝑉(𝑀‘𝑉)”〉〉) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
110 | 101, 104,
109 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘𝐵) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
111 | 22, 100, 110 | 3eqtr3d 2664 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
112 | 111 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
113 | | swrdcl 13419 |
. . . . . . . . . . . . . 14
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
114 | 37, 113 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
115 | 114 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
116 | 97 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → 〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 ×
2𝑜)) |
117 | | ccatcl 13359 |
. . . . . . . . . . . 12
⊢ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2𝑜))
→ (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ∈ Word (𝐼 ×
2𝑜)) |
118 | 115, 116,
117 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ∈ Word (𝐼 ×
2𝑜)) |
119 | | swrdcl 13419 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 ×
2𝑜)) |
120 | 37, 119 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 ×
2𝑜)) |
121 | 120 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 ×
2𝑜)) |
122 | | swrdcl 13419 |
. . . . . . . . . . . . . 14
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 ×
2𝑜)) |
123 | 73, 122 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 ×
2𝑜)) |
124 | 123 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 ×
2𝑜)) |
125 | 107 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → 〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 ×
2𝑜)) |
126 | | ccatcl 13359 |
. . . . . . . . . . . 12
⊢ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2𝑜))
→ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ∈ Word (𝐼 ×
2𝑜)) |
127 | 124, 125,
126 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ∈ Word (𝐼 ×
2𝑜)) |
128 | | swrdcl 13419 |
. . . . . . . . . . . . 13
⊢ ((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) →
((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 ×
2𝑜)) |
129 | 73, 128 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 ×
2𝑜)) |
130 | 129 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 ×
2𝑜)) |
131 | | swrd0len 13422 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) ∧ 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) → (#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) = 𝑃) |
132 | 37, 38, 131 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) = 𝑃) |
133 | | swrd0len 13422 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵‘𝐿) ∈ Word (𝐼 × 2𝑜) ∧ 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) → (#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) = 𝑄) |
134 | 73, 74, 133 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) = 𝑄) |
135 | 132, 134 | eqeq12d 2637 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) = (#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) ↔ 𝑃 = 𝑄)) |
136 | 135 | biimpar 502 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) = (#‘((𝐵‘𝐿) substr 〈0, 𝑄〉))) |
137 | | s2len 13634 |
. . . . . . . . . . . . . . 15
⊢
(#‘〈“𝑈(𝑀‘𝑈)”〉) = 2 |
138 | | s2len 13634 |
. . . . . . . . . . . . . . 15
⊢
(#‘〈“𝑉(𝑀‘𝑉)”〉) = 2 |
139 | 137, 138 | eqtr4i 2647 |
. . . . . . . . . . . . . 14
⊢
(#‘〈“𝑈(𝑀‘𝑈)”〉) =
(#‘〈“𝑉(𝑀‘𝑉)”〉) |
140 | 139 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (#‘〈“𝑈(𝑀‘𝑈)”〉) =
(#‘〈“𝑉(𝑀‘𝑉)”〉)) |
141 | 136, 140 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ((#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) + (#‘〈“𝑈(𝑀‘𝑈)”〉)) = ((#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) + (#‘〈“𝑉(𝑀‘𝑉)”〉))) |
142 | | ccatlen 13360 |
. . . . . . . . . . . . 13
⊢ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2𝑜))
→ (#‘(((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉)) = ((#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) + (#‘〈“𝑈(𝑀‘𝑈)”〉))) |
143 | 115, 116,
142 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (#‘(((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉)) = ((#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) + (#‘〈“𝑈(𝑀‘𝑈)”〉))) |
144 | | ccatlen 13360 |
. . . . . . . . . . . . 13
⊢ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2𝑜))
→ (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉)) = ((#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) + (#‘〈“𝑉(𝑀‘𝑉)”〉))) |
145 | 124, 125,
144 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉)) = ((#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) + (#‘〈“𝑉(𝑀‘𝑉)”〉))) |
146 | 141, 143,
145 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (#‘(((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉)) = (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉))) |
147 | | ccatopth 13470 |
. . . . . . . . . . 11
⊢
((((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ∈ Word (𝐼 × 2𝑜)
∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2𝑜)) ∧
((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ∈ Word (𝐼 × 2𝑜)
∧ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2𝑜)) ∧
(#‘(((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉)) = (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉))) → (((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) ↔ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)))) |
148 | 118, 121,
127, 130, 146, 147 | syl221anc 1337 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) ↔ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)))) |
149 | 112, 148 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
150 | 149 | simpld 475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉)) |
151 | | ccatopth 13470 |
. . . . . . . . 9
⊢
(((((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 × 2𝑜)
∧ 〈“𝑈(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2𝑜))
∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜)
∧ 〈“𝑉(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2𝑜))
∧ (#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) = (#‘((𝐵‘𝐿) substr 〈0, 𝑄〉))) → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ↔ (((𝐴‘𝐾) substr 〈0, 𝑃〉) = ((𝐵‘𝐿) substr 〈0, 𝑄〉) ∧ 〈“𝑈(𝑀‘𝑈)”〉 = 〈“𝑉(𝑀‘𝑉)”〉))) |
152 | 115, 116,
124, 125, 136, 151 | syl221anc 1337 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ↔ (((𝐴‘𝐾) substr 〈0, 𝑃〉) = ((𝐵‘𝐿) substr 〈0, 𝑄〉) ∧ 〈“𝑈(𝑀‘𝑈)”〉 = 〈“𝑉(𝑀‘𝑉)”〉))) |
153 | 150, 152 | mpbid 222 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) = ((𝐵‘𝐿) substr 〈0, 𝑄〉) ∧ 〈“𝑈(𝑀‘𝑈)”〉 = 〈“𝑉(𝑀‘𝑉)”〉)) |
154 | 153 | simpld 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ((𝐴‘𝐾) substr 〈0, 𝑃〉) = ((𝐵‘𝐿) substr 〈0, 𝑄〉)) |
155 | 149 | simprd 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) |
156 | 154, 155 | oveq12d 6668 |
. . . . 5
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
157 | 89, 156 | mtand 691 |
. . . 4
⊢ (𝜑 → ¬ 𝑃 = 𝑄) |
158 | 157 | pm2.21d 118 |
. . 3
⊢ (𝜑 → (𝑃 = 𝑄 → (𝐴‘0) = (𝐵‘0))) |
159 | | uzp1 11721 |
. . . 4
⊢ (𝑃 ∈
(ℤ≥‘(𝑄 + 1)) → (𝑃 = (𝑄 + 1) ∨ 𝑃 ∈
(ℤ≥‘((𝑄 + 1) + 1)))) |
160 | 91 | s1cld 13383 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 〈“𝑈”〉 ∈ Word (𝐼 ×
2𝑜)) |
161 | | ccatcl 13359 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑈”〉
∈ Word (𝐼 ×
2𝑜)) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ∈ Word (𝐼 ×
2𝑜)) |
162 | 114, 160,
161 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ∈ Word (𝐼 ×
2𝑜)) |
163 | 96 | s1cld 13383 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 〈“(𝑀‘𝑈)”〉 ∈ Word (𝐼 ×
2𝑜)) |
164 | | ccatass 13371 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ∈ Word
(𝐼 ×
2𝑜) ∧ 〈“(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2𝑜)
∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2𝑜)) →
(((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++
〈“(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++ (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) |
165 | 162, 163,
120, 164 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++ 〈“(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++ (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) |
166 | | ccatass 13371 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑈”〉
∈ Word (𝐼 ×
2𝑜) ∧ 〈“(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2𝑜))
→ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++
〈“(𝑀‘𝑈)”〉) = (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ (〈“𝑈”〉 ++ 〈“(𝑀‘𝑈)”〉))) |
167 | 114, 160,
163, 166 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++ 〈“(𝑀‘𝑈)”〉) = (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ (〈“𝑈”〉 ++ 〈“(𝑀‘𝑈)”〉))) |
168 | | df-s2 13593 |
. . . . . . . . . . . . . . . . . . 19
⊢
〈“𝑈(𝑀‘𝑈)”〉 = (〈“𝑈”〉 ++
〈“(𝑀‘𝑈)”〉) |
169 | 168 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) = (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ (〈“𝑈”〉 ++ 〈“(𝑀‘𝑈)”〉)) |
170 | 167, 169 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++ 〈“(𝑀‘𝑈)”〉) = (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉)) |
171 | 170 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++ 〈“(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) |
172 | 102 | s1cld 13383 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 〈“𝑉”〉 ∈ Word (𝐼 ×
2𝑜)) |
173 | 106 | s1cld 13383 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 〈“(𝑀‘𝑉)”〉 ∈ Word (𝐼 ×
2𝑜)) |
174 | | ccatass 13371 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑉”〉
∈ Word (𝐼 ×
2𝑜) ∧ 〈“(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2𝑜))
→ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++
〈“(𝑀‘𝑉)”〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉”〉 ++ 〈“(𝑀‘𝑉)”〉))) |
175 | 123, 172,
173, 174 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉”〉 ++ 〈“(𝑀‘𝑉)”〉))) |
176 | | df-s2 13593 |
. . . . . . . . . . . . . . . . . . 19
⊢
〈“𝑉(𝑀‘𝑉)”〉 = (〈“𝑉”〉 ++
〈“(𝑀‘𝑉)”〉) |
177 | 176 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉”〉 ++ 〈“(𝑀‘𝑉)”〉)) |
178 | 175, 177 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉)) |
179 | 178 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
180 | 111, 171,
179 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++ 〈“(𝑀‘𝑈)”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
181 | 165, 180 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++ (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
182 | 181 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++ (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
183 | 162 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ∈ Word (𝐼 ×
2𝑜)) |
184 | 163 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → 〈“(𝑀‘𝑈)”〉 ∈ Word (𝐼 ×
2𝑜)) |
185 | 120 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 ×
2𝑜)) |
186 | | ccatcl 13359 |
. . . . . . . . . . . . . . 15
⊢
((〈“(𝑀‘𝑈)”〉 ∈ Word (𝐼 × 2𝑜)
∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2𝑜)) →
(〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 ×
2𝑜)) |
187 | 184, 185,
186 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 ×
2𝑜)) |
188 | | ccatcl 13359 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑉”〉
∈ Word (𝐼 ×
2𝑜)) → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ∈ Word (𝐼 ×
2𝑜)) |
189 | 123, 172,
188 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ∈ Word (𝐼 ×
2𝑜)) |
190 | 189 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ∈ Word (𝐼 ×
2𝑜)) |
191 | 173 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → 〈“(𝑀‘𝑉)”〉 ∈ Word (𝐼 ×
2𝑜)) |
192 | | ccatcl 13359 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ∈ Word
(𝐼 ×
2𝑜) ∧ 〈“(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2𝑜))
→ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++
〈“(𝑀‘𝑉)”〉) ∈ Word
(𝐼 ×
2𝑜)) |
193 | 190, 191,
192 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ∈ Word (𝐼 ×
2𝑜)) |
194 | 129 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 ×
2𝑜)) |
195 | | ccatlen 13360 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑉”〉
∈ Word (𝐼 ×
2𝑜)) → (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉)) = ((#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) + (#‘〈“𝑉”〉))) |
196 | 123, 172,
195 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉)) = ((#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) + (#‘〈“𝑉”〉))) |
197 | | s1len 13385 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(#‘〈“𝑉”〉) = 1 |
198 | 197 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(#‘〈“𝑉”〉) = 1) |
199 | 134, 198 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((#‘((𝐵‘𝐿) substr 〈0, 𝑄〉)) + (#‘〈“𝑉”〉)) = (𝑄 + 1)) |
200 | 196, 199 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉)) = (𝑄 + 1)) |
201 | 132, 200 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) = (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉)) ↔ 𝑃 = (𝑄 + 1))) |
202 | 201 | biimpar 502 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) = (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉))) |
203 | | s1len 13385 |
. . . . . . . . . . . . . . . . . 18
⊢
(#‘〈“𝑈”〉) = 1 |
204 | | s1len 13385 |
. . . . . . . . . . . . . . . . . 18
⊢
(#‘〈“(𝑀‘𝑉)”〉) = 1 |
205 | 203, 204 | eqtr4i 2647 |
. . . . . . . . . . . . . . . . 17
⊢
(#‘〈“𝑈”〉) =
(#‘〈“(𝑀‘𝑉)”〉) |
206 | 205 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (#‘〈“𝑈”〉) =
(#‘〈“(𝑀‘𝑉)”〉)) |
207 | 202, 206 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) + (#‘〈“𝑈”〉)) =
((#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉)) +
(#‘〈“(𝑀‘𝑉)”〉))) |
208 | 114 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 ×
2𝑜)) |
209 | 160 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → 〈“𝑈”〉 ∈ Word (𝐼 ×
2𝑜)) |
210 | | ccatlen 13360 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑈”〉
∈ Word (𝐼 ×
2𝑜)) → (#‘(((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉)) = ((#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) + (#‘〈“𝑈”〉))) |
211 | 208, 209,
210 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (#‘(((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉)) = ((#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) + (#‘〈“𝑈”〉))) |
212 | | ccatlen 13360 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ∈ Word
(𝐼 ×
2𝑜) ∧ 〈“(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2𝑜))
→ (#‘((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉)) = ((#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉)) +
(#‘〈“(𝑀‘𝑉)”〉))) |
213 | 190, 191,
212 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (#‘((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉)) = ((#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉)) +
(#‘〈“(𝑀‘𝑉)”〉))) |
214 | 207, 211,
213 | 3eqtr4d 2666 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (#‘(((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉)) = (#‘((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉))) |
215 | | ccatopth 13470 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ∈ Word
(𝐼 ×
2𝑜) ∧ (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 × 2𝑜)) ∧
(((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++
〈“(𝑀‘𝑉)”〉) ∈ Word
(𝐼 ×
2𝑜) ∧ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉) ∈ Word (𝐼 × 2𝑜)) ∧
(#‘(((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉)) =
(#‘((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++
〈“(𝑀‘𝑉)”〉))) →
(((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++
(〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) ↔ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ∧ (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)))) |
216 | 183, 187,
193, 194, 214, 215 | syl221anc 1337 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) ++ (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) ↔ ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ∧ (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)))) |
217 | 182, 216 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ∧ (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
218 | 217 | simpld 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉)) |
219 | | ccatopth 13470 |
. . . . . . . . . . . 12
⊢
(((((𝐴‘𝐾) substr 〈0, 𝑃〉) ∈ Word (𝐼 × 2𝑜)
∧ 〈“𝑈”〉 ∈ Word (𝐼 × 2𝑜)) ∧
((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ∈ Word
(𝐼 ×
2𝑜) ∧ 〈“(𝑀‘𝑉)”〉 ∈ Word (𝐼 × 2𝑜))
∧ (#‘((𝐴‘𝐾) substr 〈0, 𝑃〉)) = (#‘(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉))) → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ↔ (((𝐴‘𝐾) substr 〈0, 𝑃〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ∧ 〈“𝑈”〉 =
〈“(𝑀‘𝑉)”〉))) |
220 | 208, 209,
190, 191, 202, 219 | syl221anc 1337 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ 〈“𝑈”〉) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ 〈“(𝑀‘𝑉)”〉) ↔ (((𝐴‘𝐾) substr 〈0, 𝑃〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ∧ 〈“𝑈”〉 =
〈“(𝑀‘𝑉)”〉))) |
221 | 218, 220 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ∧ 〈“𝑈”〉 =
〈“(𝑀‘𝑉)”〉)) |
222 | 221 | simpld 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((𝐴‘𝐾) substr 〈0, 𝑃〉) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉)) |
223 | 222 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) |
224 | 123 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 ×
2𝑜)) |
225 | 172 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → 〈“𝑉”〉 ∈ Word (𝐼 ×
2𝑜)) |
226 | | ccatass 13371 |
. . . . . . . . 9
⊢ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑉”〉
∈ Word (𝐼 ×
2𝑜) ∧ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2𝑜)) →
((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) |
227 | 224, 225,
185, 226 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ 〈“𝑉”〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)))) |
228 | 221 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → 〈“𝑈”〉 = 〈“(𝑀‘𝑉)”〉) |
229 | | s111 13395 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ (𝐼 × 2𝑜) ∧ (𝑀‘𝑉) ∈ (𝐼 × 2𝑜)) →
(〈“𝑈”〉 = 〈“(𝑀‘𝑉)”〉 ↔ 𝑈 = (𝑀‘𝑉))) |
230 | 91, 106, 229 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (〈“𝑈”〉 =
〈“(𝑀‘𝑉)”〉 ↔ 𝑈 = (𝑀‘𝑉))) |
231 | 230 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (〈“𝑈”〉 =
〈“(𝑀‘𝑉)”〉 ↔ 𝑈 = (𝑀‘𝑉))) |
232 | 228, 231 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → 𝑈 = (𝑀‘𝑉)) |
233 | 232 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (𝑀‘𝑈) = (𝑀‘(𝑀‘𝑉))) |
234 | 8 | efgmnvl 18127 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 ∈ (𝐼 × 2𝑜) →
(𝑀‘(𝑀‘𝑉)) = 𝑉) |
235 | 102, 234 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀‘(𝑀‘𝑉)) = 𝑉) |
236 | 235 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (𝑀‘(𝑀‘𝑉)) = 𝑉) |
237 | 233, 236 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (𝑀‘𝑈) = 𝑉) |
238 | 237 | s1eqd 13381 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → 〈“(𝑀‘𝑈)”〉 = 〈“𝑉”〉) |
239 | 238 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (〈“𝑉”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) |
240 | 217 | simprd 479 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (〈“(𝑀‘𝑈)”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) |
241 | 239, 240 | eqtr3d 2658 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (〈“𝑉”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉)) |
242 | 241 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ (〈“𝑉”〉 ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉))) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
243 | 223, 227,
242 | 3eqtrd 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 = (𝑄 + 1)) → (((𝐴‘𝐾) substr 〈0, 𝑃〉) ++ ((𝐴‘𝐾) substr 〈𝑃, (#‘(𝐴‘𝐾))〉)) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐵‘𝐿) substr 〈𝑄, (#‘(𝐵‘𝐿))〉))) |
244 | 89, 243 | mtand 691 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑃 = (𝑄 + 1)) |
245 | 244 | pm2.21d 118 |
. . . . 5
⊢ (𝜑 → (𝑃 = (𝑄 + 1) → (𝐴‘0) = (𝐵‘0))) |
246 | | elfzelz 12342 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ (0...(#‘(𝐵‘𝐿))) → 𝑄 ∈ ℤ) |
247 | 74, 246 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℤ) |
248 | 247 | zcnd 11483 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℂ) |
249 | | 1cnd 10056 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
250 | 248, 249,
249 | addassd 10062 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑄 + 1) + 1) = (𝑄 + (1 + 1))) |
251 | | df-2 11079 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
252 | 251 | oveq2i 6661 |
. . . . . . . . 9
⊢ (𝑄 + 2) = (𝑄 + (1 + 1)) |
253 | 250, 252 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄 + 1) + 1) = (𝑄 + 2)) |
254 | 253 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜑 →
(ℤ≥‘((𝑄 + 1) + 1)) =
(ℤ≥‘(𝑄 + 2))) |
255 | 254 | eleq2d 2687 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∈
(ℤ≥‘((𝑄 + 1) + 1)) ↔ 𝑃 ∈ (ℤ≥‘(𝑄 + 2)))) |
256 | 3, 7, 8, 9, 10, 11 | efgsfo 18152 |
. . . . . . . . . 10
⊢ 𝑆:dom 𝑆–onto→𝑊 |
257 | | swrdcl 13419 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ Word (𝐼 × 2𝑜) →
((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 ×
2𝑜)) |
258 | 37, 257 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 ×
2𝑜)) |
259 | | ccatcl 13359 |
. . . . . . . . . . . 12
⊢ ((((𝐵‘𝐿) substr 〈0, 𝑄〉) ∈ Word (𝐼 × 2𝑜) ∧
((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉) ∈ Word (𝐼 × 2𝑜)) →
(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 ×
2𝑜)) |
260 | 123, 258,
259 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) ∈ Word (𝐼 ×
2𝑜)) |
261 | 3 | efgrcl 18128 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝐾) ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
262 | 36, 261 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
263 | 262 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 = Word (𝐼 ×
2𝑜)) |
264 | 260, 263 | eleqtrrd 2704 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) ∈ 𝑊) |
265 | | foelrn 6378 |
. . . . . . . . . 10
⊢ ((𝑆:dom 𝑆–onto→𝑊 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) ∈ 𝑊) → ∃𝑐 ∈ dom 𝑆(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐)) |
266 | 256, 264,
265 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑐 ∈ dom 𝑆(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐)) |
267 | 266 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) → ∃𝑐 ∈ dom 𝑆(((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐)) |
268 | 20 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝐴)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
269 | 6 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → 𝐴 ∈ dom 𝑆) |
270 | 21 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → 𝐵 ∈ dom 𝑆) |
271 | 22 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → (𝑆‘𝐴) = (𝑆‘𝐵)) |
272 | 23 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → ¬ (𝐴‘0) = (𝐵‘0)) |
273 | 38 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → 𝑃 ∈ (0...(#‘(𝐴‘𝐾)))) |
274 | 74 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → 𝑄 ∈ (0...(#‘(𝐵‘𝐿)))) |
275 | 91 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → 𝑈 ∈ (𝐼 ×
2𝑜)) |
276 | 102 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → 𝑉 ∈ (𝐼 ×
2𝑜)) |
277 | 90 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → (𝑆‘𝐴) = (𝑃(𝑇‘(𝐴‘𝐾))𝑈)) |
278 | 101 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → (𝑆‘𝐵) = (𝑄(𝑇‘(𝐵‘𝐿))𝑉)) |
279 | 2 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → ¬ (𝐴‘𝐾) = (𝐵‘𝐿)) |
280 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) |
281 | | simprl 794 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → 𝑐 ∈ dom 𝑆) |
282 | | simprr 796 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐)) |
283 | 282 | eqcomd 2628 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → (𝑆‘𝑐) = (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉))) |
284 | 3, 7, 8, 9, 10, 11, 268, 269, 270, 271, 272, 19, 60, 273, 274, 275, 276, 277, 278, 279, 280, 281, 283 | efgredlemd 18157 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) ∧ (𝑐 ∈ dom 𝑆 ∧ (((𝐵‘𝐿) substr 〈0, 𝑄〉) ++ ((𝐴‘𝐾) substr 〈(𝑄 + 2), (#‘(𝐴‘𝐾))〉)) = (𝑆‘𝑐))) → (𝐴‘0) = (𝐵‘0)) |
285 | 267, 284 | rexlimddv 3035 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∈ (ℤ≥‘(𝑄 + 2))) → (𝐴‘0) = (𝐵‘0)) |
286 | 285 | ex 450 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∈ (ℤ≥‘(𝑄 + 2)) → (𝐴‘0) = (𝐵‘0))) |
287 | 255, 286 | sylbid 230 |
. . . . 5
⊢ (𝜑 → (𝑃 ∈
(ℤ≥‘((𝑄 + 1) + 1)) → (𝐴‘0) = (𝐵‘0))) |
288 | 245, 287 | jaod 395 |
. . . 4
⊢ (𝜑 → ((𝑃 = (𝑄 + 1) ∨ 𝑃 ∈
(ℤ≥‘((𝑄 + 1) + 1))) → (𝐴‘0) = (𝐵‘0))) |
289 | 159, 288 | syl5 34 |
. . 3
⊢ (𝜑 → (𝑃 ∈ (ℤ≥‘(𝑄 + 1)) → (𝐴‘0) = (𝐵‘0))) |
290 | 158, 289 | jaod 395 |
. 2
⊢ (𝜑 → ((𝑃 = 𝑄 ∨ 𝑃 ∈ (ℤ≥‘(𝑄 + 1))) → (𝐴‘0) = (𝐵‘0))) |
291 | 1, 290 | syl5 34 |
1
⊢ (𝜑 → (𝑃 ∈ (ℤ≥‘𝑄) → (𝐴‘0) = (𝐵‘0))) |