Step | Hyp | Ref
| Expression |
1 | | ccatws1len 13251 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → (#‘(𝑋 ++ 〈“𝐶”〉)) = ((#‘𝑋) + 1)) |
2 | 1 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (#‘(𝑋 ++ 〈“𝐶”〉)) = ((#‘𝑋) + 1)) |
3 | 2 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (0..^(#‘(𝑋 ++ 〈“𝐶”〉))) = (0..^((#‘𝑋) + 1))) |
4 | | lencl 13179 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Word 𝐵 → (#‘𝑋) ∈
ℕ0) |
5 | | elnn0uz 11601 |
. . . . . . . . . . 11
⊢
((#‘𝑋) ∈
ℕ0 ↔ (#‘𝑋) ∈
(ℤ≥‘0)) |
6 | 4, 5 | sylib 207 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Word 𝐵 → (#‘𝑋) ∈
(ℤ≥‘0)) |
7 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → (#‘𝑋) ∈
(ℤ≥‘0)) |
8 | | fzosplitsn 12442 |
. . . . . . . . 9
⊢
((#‘𝑋) ∈
(ℤ≥‘0) → (0..^((#‘𝑋) + 1)) = ((0..^(#‘𝑋)) ∪ {(#‘𝑋)})) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → (0..^((#‘𝑋) + 1)) = ((0..^(#‘𝑋)) ∪ {(#‘𝑋)})) |
10 | 9 | 3ad2ant1 1075 |
. . . . . . 7
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (0..^((#‘𝑋) + 1)) = ((0..^(#‘𝑋)) ∪ {(#‘𝑋)})) |
11 | 3, 10 | eqtrd 2644 |
. . . . . 6
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (0..^(#‘(𝑋 ++ 〈“𝐶”〉))) = ((0..^(#‘𝑋)) ∪ {(#‘𝑋)})) |
12 | 11 | raleqdv 3121 |
. . . . 5
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ ∀𝑖 ∈ ((0..^(#‘𝑋)) ∪ {(#‘𝑋)})∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛))) |
13 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → (#‘𝑋) ∈
ℕ0) |
14 | 13 | 3ad2ant1 1075 |
. . . . . 6
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (#‘𝑋) ∈
ℕ0) |
15 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑖 = (#‘𝑋) → ((𝑋 ++ 〈“𝐶”〉)‘𝑖) = ((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋))) |
16 | 15 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑖 = (#‘𝑋) → (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋))‘𝑛)) |
17 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑖 = (#‘𝑋) → ((𝑌 ++ 〈“𝑅”〉)‘𝑖) = ((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))) |
18 | 17 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑖 = (#‘𝑋) → (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))‘𝑛)) |
19 | 16, 18 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑖 = (#‘𝑋) → ((((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ (((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))‘𝑛))) |
20 | 19 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑖 = (#‘𝑋) → (∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ ∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))‘𝑛))) |
21 | 20 | ralunsn 4360 |
. . . . . 6
⊢
((#‘𝑋) ∈
ℕ0 → (∀𝑖 ∈ ((0..^(#‘𝑋)) ∪ {(#‘𝑋)})∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))‘𝑛)))) |
22 | 14, 21 | syl 17 |
. . . . 5
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (∀𝑖 ∈ ((0..^(#‘𝑋)) ∪ {(#‘𝑋)})∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))‘𝑛)))) |
23 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → 𝑋 ∈ Word 𝐵) |
24 | 23 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → 𝑋 ∈ Word 𝐵) |
25 | 24 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝑋 ∈ Word 𝐵) |
26 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵) |
27 | 26 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → 𝐶 ∈ 𝐵) |
28 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝐶 ∈ 𝐵) |
29 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝑖 ∈ (0..^(#‘𝑋))) |
30 | | ccats1val1 13255 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ 𝑖 ∈ (0..^(#‘𝑋))) → ((𝑋 ++ 〈“𝐶”〉)‘𝑖) = (𝑋‘𝑖)) |
31 | 25, 28, 29, 30 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → ((𝑋 ++ 〈“𝐶”〉)‘𝑖) = (𝑋‘𝑖)) |
32 | 31 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = ((𝑋‘𝑖)‘𝑛)) |
33 | | simpl2l 1107 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝑌 ∈ Word 𝑃) |
34 | | simpl2r 1108 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝑅 ∈ 𝑃) |
35 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝑋) =
(#‘𝑌) →
(0..^(#‘𝑋)) =
(0..^(#‘𝑌))) |
36 | 35 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑋) =
(#‘𝑌) → (𝑖 ∈ (0..^(#‘𝑋)) ↔ 𝑖 ∈ (0..^(#‘𝑌)))) |
37 | 36 | biimpd 218 |
. . . . . . . . . . . . 13
⊢
((#‘𝑋) =
(#‘𝑌) → (𝑖 ∈ (0..^(#‘𝑋)) → 𝑖 ∈ (0..^(#‘𝑌)))) |
38 | 37 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (𝑖 ∈ (0..^(#‘𝑋)) → 𝑖 ∈ (0..^(#‘𝑌)))) |
39 | 38 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → 𝑖 ∈ (0..^(#‘𝑌))) |
40 | | ccats1val1 13255 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ∧ 𝑖 ∈ (0..^(#‘𝑌))) → ((𝑌 ++ 〈“𝑅”〉)‘𝑖) = (𝑌‘𝑖)) |
41 | 33, 34, 39, 40 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → ((𝑌 ++ 〈“𝑅”〉)‘𝑖) = (𝑌‘𝑖)) |
42 | 41 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛)) |
43 | 32, 42 | eqeq12d 2625 |
. . . . . . . 8
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → ((((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛))) |
44 | 43 | ralbidv 2969 |
. . . . . . 7
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) ∧ 𝑖 ∈ (0..^(#‘𝑋))) → (∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ ∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛))) |
45 | 44 | ralbidva 2968 |
. . . . . 6
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ ∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛))) |
46 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → (#‘𝑋) = (#‘𝑋)) |
47 | 23, 26, 46 | 3jca 1235 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → (𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ (#‘𝑋) = (#‘𝑋))) |
48 | 47 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ (#‘𝑋) = (#‘𝑋))) |
49 | | ccats1val2 13256 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ (#‘𝑋) = (#‘𝑋)) → ((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋)) = 𝐶) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → ((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋)) = 𝐶) |
51 | 50 | fveq1d 6105 |
. . . . . . . 8
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋))‘𝑛) = (𝐶‘𝑛)) |
52 | | df-3an 1033 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ∧ (#‘𝑋) = (#‘𝑌)) ↔ ((𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) |
53 | 52 | biimpri 217 |
. . . . . . . . . 10
⊢ (((𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ∧ (#‘𝑋) = (#‘𝑌))) |
54 | 53 | 3adant1 1072 |
. . . . . . . . 9
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ∧ (#‘𝑋) = (#‘𝑌))) |
55 | | ccats1val2 13256 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ∧ (#‘𝑋) = (#‘𝑌)) → ((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋)) = 𝑅) |
56 | 55 | fveq1d 6105 |
. . . . . . . . 9
⊢ ((𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ∧ (#‘𝑋) = (#‘𝑌)) → (((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))‘𝑛) = (𝑅‘𝑛)) |
57 | 54, 56 | syl 17 |
. . . . . . . 8
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))‘𝑛) = (𝑅‘𝑛)) |
58 | 51, 57 | eqeq12d 2625 |
. . . . . . 7
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → ((((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))‘𝑛) ↔ (𝐶‘𝑛) = (𝑅‘𝑛))) |
59 | 58 | ralbidv 2969 |
. . . . . 6
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))‘𝑛) ↔ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛))) |
60 | 45, 59 | anbi12d 743 |
. . . . 5
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘(#‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(#‘𝑋))‘𝑛)) ↔ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)))) |
61 | 12, 22, 60 | 3bitrd 293 |
. . . 4
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌)) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)))) |
62 | 61 | ad2antlr 759 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)))) |
63 | | pm3.35 609 |
. . . . . . 7
⊢
((∀𝑖 ∈
(0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) |
64 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → ((𝑆 Σg 𝑋)‘𝑛) = ((𝑆 Σg 𝑋)‘𝑗)) |
65 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → ((𝑍 Σg 𝑌)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑗)) |
66 | 64, 65 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ↔ ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗))) |
67 | 66 | cbvralv 3147 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ↔ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) |
68 | | simp-4l 802 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → 𝑁 ∈ Fin) |
69 | | simp-4r 803 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → 𝑀 ∈ Fin) |
70 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → 𝑛 ∈ 𝐼) |
71 | 68, 69, 70 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → (𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛 ∈ 𝐼)) |
72 | 71 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) ∧ (𝐶‘𝑛) = (𝑅‘𝑛)) → (𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛 ∈ 𝐼)) |
73 | | simp-4r 803 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) ∧ (𝐶‘𝑛) = (𝑅‘𝑛)) → ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) |
74 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) → ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) |
76 | 75 | anim1i 590 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) ∧ (𝐶‘𝑛) = (𝑅‘𝑛)) → (∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) ∧ (𝐶‘𝑛) = (𝑅‘𝑛))) |
77 | | gsmsymgrfix.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (SymGrp‘𝑁) |
78 | | gsmsymgrfix.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑆) |
79 | | gsmsymgreq.z |
. . . . . . . . . . . . . . 15
⊢ 𝑍 = (SymGrp‘𝑀) |
80 | | gsmsymgreq.p |
. . . . . . . . . . . . . . 15
⊢ 𝑃 = (Base‘𝑍) |
81 | | gsmsymgreq.i |
. . . . . . . . . . . . . . 15
⊢ 𝐼 = (𝑁 ∩ 𝑀) |
82 | 77, 78, 79, 80, 81 | gsmsymgreqlem1 17673 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ((∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) ∧ (𝐶‘𝑛) = (𝑅‘𝑛)) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛))) |
83 | 82 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ (∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) ∧ (𝐶‘𝑛) = (𝑅‘𝑛))) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)) |
84 | 72, 73, 76, 83 | syl21anc 1317 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) ∧ (𝐶‘𝑛) = (𝑅‘𝑛)) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)) |
85 | 84 | ex 449 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → ((𝐶‘𝑛) = (𝑅‘𝑛) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛))) |
86 | 85 | ralimdva 2945 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) → (∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛))) |
87 | 86 | expcom 450 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → (∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
88 | 67, 87 | sylbi 206 |
. . . . . . . 8
⊢
(∀𝑛 ∈
𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → (∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
89 | 88 | com23 84 |
. . . . . . 7
⊢
(∀𝑛 ∈
𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) → (∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
90 | 63, 89 | syl 17 |
. . . . . 6
⊢
((∀𝑖 ∈
(0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → (∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
91 | 90 | impancom 455 |
. . . . 5
⊢
((∀𝑖 ∈
(0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
92 | 91 | com13 86 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
93 | 92 | imp 444 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛))) |
94 | 62, 93 | sylbid 229 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) ∧ (∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛))) |
95 | 94 | ex 449 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |