Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . . . 10
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | fviss 6166 |
. . . . . . . . . 10
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
3 | 1, 2 | eqsstri 3598 |
. . . . . . . . 9
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
4 | 3 | sseli 3564 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑊 → 𝐴 ∈ Word (𝐼 ×
2𝑜)) |
5 | | revcl 13361 |
. . . . . . . 8
⊢ (𝐴 ∈ Word (𝐼 × 2𝑜) →
(reverse‘𝐴) ∈
Word (𝐼 ×
2𝑜)) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑊 → (reverse‘𝐴) ∈ Word (𝐼 ×
2𝑜)) |
7 | | efgval2.m |
. . . . . . . 8
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
8 | 7 | efgmf 17949 |
. . . . . . 7
⊢ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜) |
9 | | revco 13431 |
. . . . . . 7
⊢
(((reverse‘𝐴)
∈ Word (𝐼 ×
2𝑜) ∧ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 × 2𝑜)) →
(𝑀 ∘
(reverse‘(reverse‘𝐴))) = (reverse‘(𝑀 ∘ (reverse‘𝐴)))) |
10 | 6, 8, 9 | sylancl 693 |
. . . . . 6
⊢ (𝐴 ∈ 𝑊 → (𝑀 ∘ (reverse‘(reverse‘𝐴))) = (reverse‘(𝑀 ∘ (reverse‘𝐴)))) |
11 | | revrev 13367 |
. . . . . . . 8
⊢ (𝐴 ∈ Word (𝐼 × 2𝑜) →
(reverse‘(reverse‘𝐴)) = 𝐴) |
12 | 4, 11 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑊 → (reverse‘(reverse‘𝐴)) = 𝐴) |
13 | 12 | coeq2d 5206 |
. . . . . 6
⊢ (𝐴 ∈ 𝑊 → (𝑀 ∘ (reverse‘(reverse‘𝐴))) = (𝑀 ∘ 𝐴)) |
14 | 10, 13 | eqtr3d 2646 |
. . . . 5
⊢ (𝐴 ∈ 𝑊 → (reverse‘(𝑀 ∘ (reverse‘𝐴))) = (𝑀 ∘ 𝐴)) |
15 | 14 | coeq2d 5206 |
. . . 4
⊢ (𝐴 ∈ 𝑊 → (𝑀 ∘ (reverse‘(𝑀 ∘ (reverse‘𝐴)))) = (𝑀 ∘ (𝑀 ∘ 𝐴))) |
16 | | wrdf 13165 |
. . . . . . . . 9
⊢ (𝐴 ∈ Word (𝐼 × 2𝑜) → 𝐴:(0..^(#‘𝐴))⟶(𝐼 ×
2𝑜)) |
17 | 4, 16 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑊 → 𝐴:(0..^(#‘𝐴))⟶(𝐼 ×
2𝑜)) |
18 | 17 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑊 ∧ 𝑐 ∈ (0..^(#‘𝐴))) → (𝐴‘𝑐) ∈ (𝐼 ×
2𝑜)) |
19 | 7 | efgmnvl 17950 |
. . . . . . 7
⊢ ((𝐴‘𝑐) ∈ (𝐼 × 2𝑜) →
(𝑀‘(𝑀‘(𝐴‘𝑐))) = (𝐴‘𝑐)) |
20 | 18, 19 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ 𝑐 ∈ (0..^(#‘𝐴))) → (𝑀‘(𝑀‘(𝐴‘𝑐))) = (𝐴‘𝑐)) |
21 | 20 | mpteq2dva 4672 |
. . . . 5
⊢ (𝐴 ∈ 𝑊 → (𝑐 ∈ (0..^(#‘𝐴)) ↦ (𝑀‘(𝑀‘(𝐴‘𝑐)))) = (𝑐 ∈ (0..^(#‘𝐴)) ↦ (𝐴‘𝑐))) |
22 | 8 | ffvelrni 6266 |
. . . . . . 7
⊢ ((𝐴‘𝑐) ∈ (𝐼 × 2𝑜) →
(𝑀‘(𝐴‘𝑐)) ∈ (𝐼 ×
2𝑜)) |
23 | 18, 22 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ 𝑐 ∈ (0..^(#‘𝐴))) → (𝑀‘(𝐴‘𝑐)) ∈ (𝐼 ×
2𝑜)) |
24 | | fcompt 6306 |
. . . . . . 7
⊢ ((𝑀:(𝐼 ×
2𝑜)⟶(𝐼 × 2𝑜) ∧ 𝐴:(0..^(#‘𝐴))⟶(𝐼 × 2𝑜)) →
(𝑀 ∘ 𝐴) = (𝑐 ∈ (0..^(#‘𝐴)) ↦ (𝑀‘(𝐴‘𝑐)))) |
25 | 8, 17, 24 | sylancr 694 |
. . . . . 6
⊢ (𝐴 ∈ 𝑊 → (𝑀 ∘ 𝐴) = (𝑐 ∈ (0..^(#‘𝐴)) ↦ (𝑀‘(𝐴‘𝑐)))) |
26 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑊 → 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜)) |
27 | 26 | feqmptd 6159 |
. . . . . 6
⊢ (𝐴 ∈ 𝑊 → 𝑀 = (𝑎 ∈ (𝐼 × 2𝑜) ↦
(𝑀‘𝑎))) |
28 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = (𝑀‘(𝐴‘𝑐)) → (𝑀‘𝑎) = (𝑀‘(𝑀‘(𝐴‘𝑐)))) |
29 | 23, 25, 27, 28 | fmptco 6303 |
. . . . 5
⊢ (𝐴 ∈ 𝑊 → (𝑀 ∘ (𝑀 ∘ 𝐴)) = (𝑐 ∈ (0..^(#‘𝐴)) ↦ (𝑀‘(𝑀‘(𝐴‘𝑐))))) |
30 | 17 | feqmptd 6159 |
. . . . 5
⊢ (𝐴 ∈ 𝑊 → 𝐴 = (𝑐 ∈ (0..^(#‘𝐴)) ↦ (𝐴‘𝑐))) |
31 | 21, 29, 30 | 3eqtr4d 2654 |
. . . 4
⊢ (𝐴 ∈ 𝑊 → (𝑀 ∘ (𝑀 ∘ 𝐴)) = 𝐴) |
32 | 15, 31 | eqtrd 2644 |
. . 3
⊢ (𝐴 ∈ 𝑊 → (𝑀 ∘ (reverse‘(𝑀 ∘ (reverse‘𝐴)))) = 𝐴) |
33 | 32 | oveq2d 6565 |
. 2
⊢ (𝐴 ∈ 𝑊 → ((𝑀 ∘ (reverse‘𝐴)) ++ (𝑀 ∘ (reverse‘(𝑀 ∘ (reverse‘𝐴))))) = ((𝑀 ∘ (reverse‘𝐴)) ++ 𝐴)) |
34 | | wrdco 13428 |
. . . . 5
⊢
(((reverse‘𝐴)
∈ Word (𝐼 ×
2𝑜) ∧ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 × 2𝑜)) →
(𝑀 ∘
(reverse‘𝐴)) ∈
Word (𝐼 ×
2𝑜)) |
35 | 6, 8, 34 | sylancl 693 |
. . . 4
⊢ (𝐴 ∈ 𝑊 → (𝑀 ∘ (reverse‘𝐴)) ∈ Word (𝐼 ×
2𝑜)) |
36 | 1 | efgrcl 17951 |
. . . . 5
⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
37 | 36 | simprd 478 |
. . . 4
⊢ (𝐴 ∈ 𝑊 → 𝑊 = Word (𝐼 ×
2𝑜)) |
38 | 35, 37 | eleqtrrd 2691 |
. . 3
⊢ (𝐴 ∈ 𝑊 → (𝑀 ∘ (reverse‘𝐴)) ∈ 𝑊) |
39 | | efgval.r |
. . . 4
⊢ ∼ = (
~FG ‘𝐼) |
40 | | efgval2.t |
. . . 4
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
41 | 1, 39, 7, 40 | efginvrel2 17963 |
. . 3
⊢ ((𝑀 ∘ (reverse‘𝐴)) ∈ 𝑊 → ((𝑀 ∘ (reverse‘𝐴)) ++ (𝑀 ∘ (reverse‘(𝑀 ∘ (reverse‘𝐴))))) ∼
∅) |
42 | 38, 41 | syl 17 |
. 2
⊢ (𝐴 ∈ 𝑊 → ((𝑀 ∘ (reverse‘𝐴)) ++ (𝑀 ∘ (reverse‘(𝑀 ∘ (reverse‘𝐴))))) ∼
∅) |
43 | 33, 42 | eqbrtrrd 4607 |
1
⊢ (𝐴 ∈ 𝑊 → ((𝑀 ∘ (reverse‘𝐴)) ++ 𝐴) ∼
∅) |