Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . 4
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | fviss 6256 |
. . . 4
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
3 | 1, 2 | eqsstri 3635 |
. . 3
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
4 | 3 | sseli 3599 |
. 2
⊢ (𝐴 ∈ 𝑊 → 𝐴 ∈ Word (𝐼 ×
2𝑜)) |
5 | | id 22 |
. . . . . 6
⊢ (𝑐 = ∅ → 𝑐 = ∅) |
6 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑐 = ∅ →
(reverse‘𝑐) =
(reverse‘∅)) |
7 | | rev0 13513 |
. . . . . . . . 9
⊢
(reverse‘∅) = ∅ |
8 | 6, 7 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑐 = ∅ →
(reverse‘𝑐) =
∅) |
9 | 8 | coeq2d 5284 |
. . . . . . 7
⊢ (𝑐 = ∅ → (𝑀 ∘ (reverse‘𝑐)) = (𝑀 ∘ ∅)) |
10 | | co02 5649 |
. . . . . . 7
⊢ (𝑀 ∘ ∅) =
∅ |
11 | 9, 10 | syl6eq 2672 |
. . . . . 6
⊢ (𝑐 = ∅ → (𝑀 ∘ (reverse‘𝑐)) = ∅) |
12 | 5, 11 | oveq12d 6668 |
. . . . 5
⊢ (𝑐 = ∅ → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) = (∅ ++ ∅)) |
13 | 12 | breq1d 4663 |
. . . 4
⊢ (𝑐 = ∅ → ((𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅ ↔
(∅ ++ ∅) ∼
∅)) |
14 | 13 | imbi2d 330 |
. . 3
⊢ (𝑐 = ∅ → ((𝐴 ∈ 𝑊 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅) ↔
(𝐴 ∈ 𝑊 → (∅ ++ ∅) ∼
∅))) |
15 | | id 22 |
. . . . . 6
⊢ (𝑐 = 𝑎 → 𝑐 = 𝑎) |
16 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑐 = 𝑎 → (reverse‘𝑐) = (reverse‘𝑎)) |
17 | 16 | coeq2d 5284 |
. . . . . 6
⊢ (𝑐 = 𝑎 → (𝑀 ∘ (reverse‘𝑐)) = (𝑀 ∘ (reverse‘𝑎))) |
18 | 15, 17 | oveq12d 6668 |
. . . . 5
⊢ (𝑐 = 𝑎 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) = (𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) |
19 | 18 | breq1d 4663 |
. . . 4
⊢ (𝑐 = 𝑎 → ((𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅ ↔
(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼
∅)) |
20 | 19 | imbi2d 330 |
. . 3
⊢ (𝑐 = 𝑎 → ((𝐴 ∈ 𝑊 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅) ↔
(𝐴 ∈ 𝑊 → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼
∅))) |
21 | | id 22 |
. . . . . 6
⊢ (𝑐 = (𝑎 ++ 〈“𝑏”〉) → 𝑐 = (𝑎 ++ 〈“𝑏”〉)) |
22 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑐 = (𝑎 ++ 〈“𝑏”〉) → (reverse‘𝑐) = (reverse‘(𝑎 ++ 〈“𝑏”〉))) |
23 | 22 | coeq2d 5284 |
. . . . . 6
⊢ (𝑐 = (𝑎 ++ 〈“𝑏”〉) → (𝑀 ∘ (reverse‘𝑐)) = (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) |
24 | 21, 23 | oveq12d 6668 |
. . . . 5
⊢ (𝑐 = (𝑎 ++ 〈“𝑏”〉) → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) = ((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉))))) |
25 | 24 | breq1d 4663 |
. . . 4
⊢ (𝑐 = (𝑎 ++ 〈“𝑏”〉) → ((𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅ ↔
((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) ∼
∅)) |
26 | 25 | imbi2d 330 |
. . 3
⊢ (𝑐 = (𝑎 ++ 〈“𝑏”〉) → ((𝐴 ∈ 𝑊 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅) ↔
(𝐴 ∈ 𝑊 → ((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) ∼
∅))) |
27 | | id 22 |
. . . . . 6
⊢ (𝑐 = 𝐴 → 𝑐 = 𝐴) |
28 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑐 = 𝐴 → (reverse‘𝑐) = (reverse‘𝐴)) |
29 | 28 | coeq2d 5284 |
. . . . . 6
⊢ (𝑐 = 𝐴 → (𝑀 ∘ (reverse‘𝑐)) = (𝑀 ∘ (reverse‘𝐴))) |
30 | 27, 29 | oveq12d 6668 |
. . . . 5
⊢ (𝑐 = 𝐴 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) = (𝐴 ++ (𝑀 ∘ (reverse‘𝐴)))) |
31 | 30 | breq1d 4663 |
. . . 4
⊢ (𝑐 = 𝐴 → ((𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅ ↔
(𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼
∅)) |
32 | 31 | imbi2d 330 |
. . 3
⊢ (𝑐 = 𝐴 → ((𝐴 ∈ 𝑊 → (𝑐 ++ (𝑀 ∘ (reverse‘𝑐))) ∼ ∅) ↔
(𝐴 ∈ 𝑊 → (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼
∅))) |
33 | | wrd0 13330 |
. . . . 5
⊢ ∅
∈ Word (𝐼 ×
2𝑜) |
34 | | ccatlid 13369 |
. . . . 5
⊢ (∅
∈ Word (𝐼 ×
2𝑜) → (∅ ++ ∅) = ∅) |
35 | 33, 34 | ax-mp 5 |
. . . 4
⊢ (∅
++ ∅) = ∅ |
36 | | efgval.r |
. . . . . . 7
⊢ ∼ = (
~FG ‘𝐼) |
37 | 1, 36 | efger 18131 |
. . . . . 6
⊢ ∼ Er
𝑊 |
38 | 37 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ 𝑊 → ∼ Er 𝑊) |
39 | 1 | efgrcl 18128 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
40 | 39 | simprd 479 |
. . . . . 6
⊢ (𝐴 ∈ 𝑊 → 𝑊 = Word (𝐼 ×
2𝑜)) |
41 | 33, 40 | syl5eleqr 2708 |
. . . . 5
⊢ (𝐴 ∈ 𝑊 → ∅ ∈ 𝑊) |
42 | 38, 41 | erref 7762 |
. . . 4
⊢ (𝐴 ∈ 𝑊 → ∅ ∼
∅) |
43 | 35, 42 | syl5eqbr 4688 |
. . 3
⊢ (𝐴 ∈ 𝑊 → (∅ ++ ∅) ∼
∅) |
44 | 37 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
∼
Er 𝑊) |
45 | | simprl 794 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑎 ∈ Word (𝐼 ×
2𝑜)) |
46 | | revcl 13510 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ Word (𝐼 × 2𝑜) →
(reverse‘𝑎) ∈
Word (𝐼 ×
2𝑜)) |
47 | 46 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(reverse‘𝑎) ∈
Word (𝐼 ×
2𝑜)) |
48 | | efgval2.m |
. . . . . . . . . . . 12
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
49 | 48 | efgmf 18126 |
. . . . . . . . . . 11
⊢ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜) |
50 | | wrdco 13577 |
. . . . . . . . . . 11
⊢
(((reverse‘𝑎)
∈ Word (𝐼 ×
2𝑜) ∧ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 × 2𝑜)) →
(𝑀 ∘
(reverse‘𝑎)) ∈
Word (𝐼 ×
2𝑜)) |
51 | 47, 49, 50 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑀 ∘
(reverse‘𝑎)) ∈
Word (𝐼 ×
2𝑜)) |
52 | | ccatcl 13359 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ Word (𝐼 × 2𝑜) ∧ (𝑀 ∘ (reverse‘𝑎)) ∈ Word (𝐼 × 2𝑜))
→ (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ Word (𝐼 ×
2𝑜)) |
53 | 45, 51, 52 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ Word (𝐼 ×
2𝑜)) |
54 | 40 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑊 = Word (𝐼 ×
2𝑜)) |
55 | 53, 54 | eleqtrrd 2704 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ 𝑊) |
56 | | lencl 13324 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ Word (𝐼 × 2𝑜) →
(#‘𝑎) ∈
ℕ0) |
57 | 56 | ad2antrl 764 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘𝑎) ∈
ℕ0) |
58 | | nn0uz 11722 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
59 | 57, 58 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘𝑎) ∈
(ℤ≥‘0)) |
60 | | ccatlen 13360 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ Word (𝐼 × 2𝑜) ∧ (𝑀 ∘ (reverse‘𝑎)) ∈ Word (𝐼 × 2𝑜))
→ (#‘(𝑎 ++
(𝑀 ∘
(reverse‘𝑎)))) =
((#‘𝑎) +
(#‘(𝑀 ∘
(reverse‘𝑎))))) |
61 | 45, 51, 60 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) = ((#‘𝑎) + (#‘(𝑀 ∘ (reverse‘𝑎))))) |
62 | 57 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘𝑎) ∈
ℤ) |
63 | | uzid 11702 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑎) ∈
ℤ → (#‘𝑎)
∈ (ℤ≥‘(#‘𝑎))) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘𝑎) ∈
(ℤ≥‘(#‘𝑎))) |
65 | | lencl 13324 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∘ (reverse‘𝑎)) ∈ Word (𝐼 × 2𝑜)
→ (#‘(𝑀 ∘
(reverse‘𝑎))) ∈
ℕ0) |
66 | 51, 65 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘(𝑀 ∘
(reverse‘𝑎))) ∈
ℕ0) |
67 | | uzaddcl 11744 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝑎) ∈
(ℤ≥‘(#‘𝑎)) ∧ (#‘(𝑀 ∘ (reverse‘𝑎))) ∈ ℕ0) →
((#‘𝑎) +
(#‘(𝑀 ∘
(reverse‘𝑎)))) ∈
(ℤ≥‘(#‘𝑎))) |
68 | 64, 66, 67 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((#‘𝑎) +
(#‘(𝑀 ∘
(reverse‘𝑎)))) ∈
(ℤ≥‘(#‘𝑎))) |
69 | 61, 68 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) ∈
(ℤ≥‘(#‘𝑎))) |
70 | | elfzuzb 12336 |
. . . . . . . . . . . 12
⊢
((#‘𝑎) ∈
(0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) ↔ ((#‘𝑎) ∈
(ℤ≥‘0) ∧ (#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) ∈
(ℤ≥‘(#‘𝑎)))) |
71 | 59, 69, 70 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘𝑎) ∈
(0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))))) |
72 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑏 ∈ (𝐼 ×
2𝑜)) |
73 | | efgval2.t |
. . . . . . . . . . . 12
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
74 | 1, 36, 48, 73 | efgtval 18136 |
. . . . . . . . . . 11
⊢ (((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ 𝑊 ∧ (#‘𝑎) ∈ (0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) ∧ 𝑏 ∈ (𝐼 × 2𝑜)) →
((#‘𝑎)(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))𝑏) = ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) splice 〈(#‘𝑎), (#‘𝑎), 〈“𝑏(𝑀‘𝑏)”〉〉)) |
75 | 55, 71, 72, 74 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((#‘𝑎)(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))𝑏) = ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) splice 〈(#‘𝑎), (#‘𝑎), 〈“𝑏(𝑀‘𝑏)”〉〉)) |
76 | 33 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
∅ ∈ Word (𝐼
× 2𝑜)) |
77 | 49 | ffvelrni 6358 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (𝐼 × 2𝑜) →
(𝑀‘𝑏) ∈ (𝐼 ×
2𝑜)) |
78 | 72, 77 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑀‘𝑏) ∈ (𝐼 ×
2𝑜)) |
79 | 72, 78 | s2cld 13616 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
〈“𝑏(𝑀‘𝑏)”〉 ∈ Word (𝐼 ×
2𝑜)) |
80 | | ccatrid 13370 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ Word (𝐼 × 2𝑜) →
(𝑎 ++ ∅) = 𝑎) |
81 | 80 | ad2antrl 764 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑎 ++ ∅) = 𝑎) |
82 | 81 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑎 = (𝑎 ++ ∅)) |
83 | 82 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) = ((𝑎 ++ ∅) ++ (𝑀 ∘ (reverse‘𝑎)))) |
84 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘𝑎) =
(#‘𝑎)) |
85 | | hash0 13158 |
. . . . . . . . . . . . 13
⊢
(#‘∅) = 0 |
86 | 85 | oveq2i 6661 |
. . . . . . . . . . . 12
⊢
((#‘𝑎) +
(#‘∅)) = ((#‘𝑎) + 0) |
87 | 57 | nn0cnd 11353 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘𝑎) ∈
ℂ) |
88 | 87 | addid1d 10236 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((#‘𝑎) + 0) =
(#‘𝑎)) |
89 | 86, 88 | syl5req 2669 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(#‘𝑎) =
((#‘𝑎) +
(#‘∅))) |
90 | 45, 76, 51, 79, 83, 84, 89 | splval2 13508 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) splice 〈(#‘𝑎), (#‘𝑎), 〈“𝑏(𝑀‘𝑏)”〉〉) = ((𝑎 ++ 〈“𝑏(𝑀‘𝑏)”〉) ++ (𝑀 ∘ (reverse‘𝑎)))) |
91 | 72 | s1cld 13383 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
〈“𝑏”〉
∈ Word (𝐼 ×
2𝑜)) |
92 | | revccat 13515 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑏”〉
∈ Word (𝐼 ×
2𝑜)) → (reverse‘(𝑎 ++ 〈“𝑏”〉)) =
((reverse‘〈“𝑏”〉) ++ (reverse‘𝑎))) |
93 | 45, 91, 92 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(reverse‘(𝑎 ++
〈“𝑏”〉)) =
((reverse‘〈“𝑏”〉) ++ (reverse‘𝑎))) |
94 | | revs1 13514 |
. . . . . . . . . . . . . . . 16
⊢
(reverse‘〈“𝑏”〉) = 〈“𝑏”〉 |
95 | 94 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
⊢
((reverse‘〈“𝑏”〉) ++ (reverse‘𝑎)) = (〈“𝑏”〉 ++
(reverse‘𝑎)) |
96 | 93, 95 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(reverse‘(𝑎 ++
〈“𝑏”〉)) = (〈“𝑏”〉 ++
(reverse‘𝑎))) |
97 | 96 | coeq2d 5284 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑀 ∘
(reverse‘(𝑎 ++
〈“𝑏”〉))) = (𝑀 ∘ (〈“𝑏”〉 ++ (reverse‘𝑎)))) |
98 | 49 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
𝑀:(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜)) |
99 | | ccatco 13581 |
. . . . . . . . . . . . . 14
⊢
((〈“𝑏”〉 ∈ Word (𝐼 × 2𝑜) ∧
(reverse‘𝑎) ∈
Word (𝐼 ×
2𝑜) ∧ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 × 2𝑜)) →
(𝑀 ∘
(〈“𝑏”〉 ++ (reverse‘𝑎))) = ((𝑀 ∘ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘𝑎)))) |
100 | 91, 47, 98, 99 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑀 ∘
(〈“𝑏”〉 ++ (reverse‘𝑎))) = ((𝑀 ∘ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘𝑎)))) |
101 | | s1co 13579 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ (𝐼 × 2𝑜) ∧ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 × 2𝑜)) →
(𝑀 ∘
〈“𝑏”〉) = 〈“(𝑀‘𝑏)”〉) |
102 | 72, 49, 101 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑀 ∘
〈“𝑏”〉) = 〈“(𝑀‘𝑏)”〉) |
103 | 102 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((𝑀 ∘
〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘𝑎))) = (〈“(𝑀‘𝑏)”〉 ++ (𝑀 ∘ (reverse‘𝑎)))) |
104 | 97, 100, 103 | 3eqtrd 2660 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑀 ∘
(reverse‘(𝑎 ++
〈“𝑏”〉))) = (〈“(𝑀‘𝑏)”〉 ++ (𝑀 ∘ (reverse‘𝑎)))) |
105 | 104 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) = ((𝑎 ++ 〈“𝑏”〉) ++
(〈“(𝑀‘𝑏)”〉 ++ (𝑀 ∘ (reverse‘𝑎))))) |
106 | | ccatcl 13359 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑏”〉
∈ Word (𝐼 ×
2𝑜)) → (𝑎 ++ 〈“𝑏”〉) ∈ Word (𝐼 ×
2𝑜)) |
107 | 45, 91, 106 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑎 ++ 〈“𝑏”〉) ∈ Word
(𝐼 ×
2𝑜)) |
108 | 78 | s1cld 13383 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
〈“(𝑀‘𝑏)”〉 ∈ Word
(𝐼 ×
2𝑜)) |
109 | | ccatass 13371 |
. . . . . . . . . . . 12
⊢ (((𝑎 ++ 〈“𝑏”〉) ∈ Word
(𝐼 ×
2𝑜) ∧ 〈“(𝑀‘𝑏)”〉 ∈ Word (𝐼 × 2𝑜) ∧ (𝑀 ∘ (reverse‘𝑎)) ∈ Word (𝐼 × 2𝑜))
→ (((𝑎 ++
〈“𝑏”〉) ++ 〈“(𝑀‘𝑏)”〉) ++ (𝑀 ∘ (reverse‘𝑎))) = ((𝑎 ++ 〈“𝑏”〉) ++ (〈“(𝑀‘𝑏)”〉 ++ (𝑀 ∘ (reverse‘𝑎))))) |
110 | 107, 108,
51, 109 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(((𝑎 ++ 〈“𝑏”〉) ++
〈“(𝑀‘𝑏)”〉) ++ (𝑀 ∘ (reverse‘𝑎))) = ((𝑎 ++ 〈“𝑏”〉) ++ (〈“(𝑀‘𝑏)”〉 ++ (𝑀 ∘ (reverse‘𝑎))))) |
111 | | ccatass 13371 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑏”〉
∈ Word (𝐼 ×
2𝑜) ∧ 〈“(𝑀‘𝑏)”〉 ∈ Word (𝐼 × 2𝑜)) →
((𝑎 ++ 〈“𝑏”〉) ++
〈“(𝑀‘𝑏)”〉) = (𝑎 ++ (〈“𝑏”〉 ++
〈“(𝑀‘𝑏)”〉))) |
112 | 45, 91, 108, 111 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((𝑎 ++ 〈“𝑏”〉) ++
〈“(𝑀‘𝑏)”〉) = (𝑎 ++ (〈“𝑏”〉 ++
〈“(𝑀‘𝑏)”〉))) |
113 | | df-s2 13593 |
. . . . . . . . . . . . . 14
⊢
〈“𝑏(𝑀‘𝑏)”〉 = (〈“𝑏”〉 ++
〈“(𝑀‘𝑏)”〉) |
114 | 113 | oveq2i 6661 |
. . . . . . . . . . . . 13
⊢ (𝑎 ++ 〈“𝑏(𝑀‘𝑏)”〉) = (𝑎 ++ (〈“𝑏”〉 ++ 〈“(𝑀‘𝑏)”〉)) |
115 | 112, 114 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((𝑎 ++ 〈“𝑏”〉) ++
〈“(𝑀‘𝑏)”〉) = (𝑎 ++ 〈“𝑏(𝑀‘𝑏)”〉)) |
116 | 115 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(((𝑎 ++ 〈“𝑏”〉) ++
〈“(𝑀‘𝑏)”〉) ++ (𝑀 ∘ (reverse‘𝑎))) = ((𝑎 ++ 〈“𝑏(𝑀‘𝑏)”〉) ++ (𝑀 ∘ (reverse‘𝑎)))) |
117 | 105, 110,
116 | 3eqtr2rd 2663 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((𝑎 ++ 〈“𝑏(𝑀‘𝑏)”〉) ++ (𝑀 ∘ (reverse‘𝑎))) = ((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉))))) |
118 | 75, 90, 117 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((#‘𝑎)(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))𝑏) = ((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉))))) |
119 | 1, 36, 48, 73 | efgtf 18135 |
. . . . . . . . . . . 12
⊢ ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ 𝑊 → ((𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) = (𝑚 ∈ (0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))), 𝑢 ∈ (𝐼 × 2𝑜) ↦
((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) splice 〈𝑚, 𝑚, 〈“𝑢(𝑀‘𝑢)”〉〉)) ∧ (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))):((0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 ×
2𝑜))⟶𝑊)) |
120 | 119 | simprd 479 |
. . . . . . . . . . 11
⊢ ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ 𝑊 → (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))):((0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 ×
2𝑜))⟶𝑊) |
121 | | ffn 6045 |
. . . . . . . . . . 11
⊢ ((𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))):((0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 ×
2𝑜))⟶𝑊 → (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) Fn ((0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 ×
2𝑜))) |
122 | 55, 120, 121 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) Fn ((0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 ×
2𝑜))) |
123 | | fnovrn 6809 |
. . . . . . . . . 10
⊢ (((𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) Fn ((0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) × (𝐼 × 2𝑜)) ∧
(#‘𝑎) ∈
(0...(#‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) ∧ 𝑏 ∈ (𝐼 × 2𝑜)) →
((#‘𝑎)(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))𝑏) ∈ ran (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) |
124 | 122, 71, 72, 123 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((#‘𝑎)(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))𝑏) ∈ ran (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) |
125 | 118, 124 | eqeltrrd 2702 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) ∈ ran
(𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) |
126 | 1, 36, 48, 73 | efgi2 18138 |
. . . . . . . 8
⊢ (((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∈ 𝑊 ∧ ((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) ∈ ran (𝑇‘(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))))) → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉))))) |
127 | 55, 125, 126 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
(𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉))))) |
128 | 44, 127 | ersym 7754 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) ∼ (𝑎 ++ (𝑀 ∘ (reverse‘𝑎)))) |
129 | 44 | ertr 7757 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) ∼ (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∧ (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ∅) →
((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) ∼
∅)) |
130 | 128, 129 | mpand 711 |
. . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜))) →
((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ∅ →
((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) ∼
∅)) |
131 | 130 | expcom 451 |
. . . 4
⊢ ((𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜)) →
(𝐴 ∈ 𝑊 → ((𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ∅ →
((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) ∼
∅))) |
132 | 131 | a2d 29 |
. . 3
⊢ ((𝑎 ∈ Word (𝐼 × 2𝑜) ∧ 𝑏 ∈ (𝐼 × 2𝑜)) →
((𝐴 ∈ 𝑊 → (𝑎 ++ (𝑀 ∘ (reverse‘𝑎))) ∼ ∅) →
(𝐴 ∈ 𝑊 → ((𝑎 ++ 〈“𝑏”〉) ++ (𝑀 ∘ (reverse‘(𝑎 ++ 〈“𝑏”〉)))) ∼
∅))) |
133 | 14, 20, 26, 32, 43, 132 | wrdind 13476 |
. 2
⊢ (𝐴 ∈ Word (𝐼 × 2𝑜) →
(𝐴 ∈ 𝑊 → (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼
∅)) |
134 | 4, 133 | mpcom 38 |
1
⊢ (𝐴 ∈ 𝑊 → (𝐴 ++ (𝑀 ∘ (reverse‘𝐴))) ∼
∅) |