| Step | Hyp | Ref
| Expression |
| 1 | | ccatws1len 14658 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Word 𝐵 → (♯‘(𝑋 ++ 〈“𝐶”〉)) = ((♯‘𝑋) + 1)) |
| 2 | 1 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑋 ∈ Word 𝐵 → (0..^(♯‘(𝑋 ++ 〈“𝐶”〉))) =
(0..^((♯‘𝑋) +
1))) |
| 3 | | lencl 14571 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Word 𝐵 → (♯‘𝑋) ∈
ℕ0) |
| 4 | | elnn0uz 12923 |
. . . . . . . . . . 11
⊢
((♯‘𝑋)
∈ ℕ0 ↔ (♯‘𝑋) ∈
(ℤ≥‘0)) |
| 5 | 3, 4 | sylib 218 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Word 𝐵 → (♯‘𝑋) ∈
(ℤ≥‘0)) |
| 6 | | fzosplitsn 13814 |
. . . . . . . . . 10
⊢
((♯‘𝑋)
∈ (ℤ≥‘0) → (0..^((♯‘𝑋) + 1)) =
((0..^(♯‘𝑋))
∪ {(♯‘𝑋)})) |
| 7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝑋 ∈ Word 𝐵 → (0..^((♯‘𝑋) + 1)) =
((0..^(♯‘𝑋))
∪ {(♯‘𝑋)})) |
| 8 | 2, 7 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑋 ∈ Word 𝐵 → (0..^(♯‘(𝑋 ++ 〈“𝐶”〉))) =
((0..^(♯‘𝑋))
∪ {(♯‘𝑋)})) |
| 9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → (0..^(♯‘(𝑋 ++ 〈“𝐶”〉))) =
((0..^(♯‘𝑋))
∪ {(♯‘𝑋)})) |
| 10 | 9 | 3ad2ant1 1134 |
. . . . . 6
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (0..^(♯‘(𝑋 ++ 〈“𝐶”〉))) =
((0..^(♯‘𝑋))
∪ {(♯‘𝑋)})) |
| 11 | 10 | raleqdv 3326 |
. . . . 5
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ ∀𝑖 ∈ ((0..^(♯‘𝑋)) ∪ {(♯‘𝑋)})∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛))) |
| 12 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → (♯‘𝑋) ∈
ℕ0) |
| 13 | 12 | 3ad2ant1 1134 |
. . . . . 6
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (♯‘𝑋) ∈
ℕ0) |
| 14 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = (♯‘𝑋) → ((𝑋 ++ 〈“𝐶”〉)‘𝑖) = ((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))) |
| 15 | 14 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑖 = (♯‘𝑋) → (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛)) |
| 16 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = (♯‘𝑋) → ((𝑌 ++ 〈“𝑅”〉)‘𝑖) = ((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))) |
| 17 | 16 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑖 = (♯‘𝑋) → (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛)) |
| 18 | 15, 17 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑖 = (♯‘𝑋) → ((((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ (((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛))) |
| 19 | 18 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑖 = (♯‘𝑋) → (∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ ∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛))) |
| 20 | 19 | ralunsn 4894 |
. . . . . 6
⊢
((♯‘𝑋)
∈ ℕ0 → (∀𝑖 ∈ ((0..^(♯‘𝑋)) ∪ {(♯‘𝑋)})∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛)))) |
| 21 | 13, 20 | syl 17 |
. . . . 5
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (∀𝑖 ∈ ((0..^(♯‘𝑋)) ∪ {(♯‘𝑋)})∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛)))) |
| 22 | | simp1l 1198 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → 𝑋 ∈ Word 𝐵) |
| 23 | | ccats1val1 14664 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝑖 ∈ (0..^(♯‘𝑋))) → ((𝑋 ++ 〈“𝐶”〉)‘𝑖) = (𝑋‘𝑖)) |
| 24 | 22, 23 | sylan 580 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) ∧ 𝑖 ∈ (0..^(♯‘𝑋))) → ((𝑋 ++ 〈“𝐶”〉)‘𝑖) = (𝑋‘𝑖)) |
| 25 | 24 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) ∧ 𝑖 ∈ (0..^(♯‘𝑋))) → (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = ((𝑋‘𝑖)‘𝑛)) |
| 26 | | simp2l 1200 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → 𝑌 ∈ Word 𝑃) |
| 27 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑋) =
(♯‘𝑌) →
(0..^(♯‘𝑋)) =
(0..^(♯‘𝑌))) |
| 28 | 27 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑋) =
(♯‘𝑌) →
(𝑖 ∈
(0..^(♯‘𝑋))
↔ 𝑖 ∈
(0..^(♯‘𝑌)))) |
| 29 | 28 | biimpd 229 |
. . . . . . . . . . . . 13
⊢
((♯‘𝑋) =
(♯‘𝑌) →
(𝑖 ∈
(0..^(♯‘𝑋))
→ 𝑖 ∈
(0..^(♯‘𝑌)))) |
| 30 | 29 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (𝑖 ∈ (0..^(♯‘𝑋)) → 𝑖 ∈ (0..^(♯‘𝑌)))) |
| 31 | 30 | imp 406 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) ∧ 𝑖 ∈ (0..^(♯‘𝑋))) → 𝑖 ∈ (0..^(♯‘𝑌))) |
| 32 | | ccats1val1 14664 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ Word 𝑃 ∧ 𝑖 ∈ (0..^(♯‘𝑌))) → ((𝑌 ++ 〈“𝑅”〉)‘𝑖) = (𝑌‘𝑖)) |
| 33 | 26, 31, 32 | syl2an2r 685 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) ∧ 𝑖 ∈ (0..^(♯‘𝑋))) → ((𝑌 ++ 〈“𝑅”〉)‘𝑖) = (𝑌‘𝑖)) |
| 34 | 33 | fveq1d 6908 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) ∧ 𝑖 ∈ (0..^(♯‘𝑋))) → (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛)) |
| 35 | 25, 34 | eqeq12d 2753 |
. . . . . . . 8
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) ∧ 𝑖 ∈ (0..^(♯‘𝑋))) → ((((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛))) |
| 36 | 35 | ralbidv 3178 |
. . . . . . 7
⊢ ((((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) ∧ 𝑖 ∈ (0..^(♯‘𝑋))) → (∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ ∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛))) |
| 37 | 36 | ralbidva 3176 |
. . . . . 6
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ ∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛))) |
| 38 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → (♯‘𝑋) = (♯‘𝑋)) |
| 39 | | ccats1val2 14665 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ (♯‘𝑋) = (♯‘𝑋)) → ((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋)) = 𝐶) |
| 40 | 39 | fveq1d 6908 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ (♯‘𝑋) = (♯‘𝑋)) → (((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛) = (𝐶‘𝑛)) |
| 41 | 38, 40 | mpd3an3 1464 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) → (((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛) = (𝐶‘𝑛)) |
| 42 | 41 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛) = (𝐶‘𝑛)) |
| 43 | | ccats1val2 14665 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ∧ (♯‘𝑋) = (♯‘𝑌)) → ((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋)) = 𝑅) |
| 44 | 43 | fveq1d 6908 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃 ∧ (♯‘𝑋) = (♯‘𝑌)) → (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛) = (𝑅‘𝑛)) |
| 45 | 44 | 3expa 1119 |
. . . . . . . . 9
⊢ (((𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛) = (𝑅‘𝑛)) |
| 46 | 45 | 3adant1 1131 |
. . . . . . . 8
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛) = (𝑅‘𝑛)) |
| 47 | 42, 46 | eqeq12d 2753 |
. . . . . . 7
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → ((((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛) ↔ (𝐶‘𝑛) = (𝑅‘𝑛))) |
| 48 | 47 | ralbidv 3178 |
. . . . . 6
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛) ↔ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛))) |
| 49 | 37, 48 | anbi12d 632 |
. . . . 5
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘(♯‘𝑋))‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘(♯‘𝑋))‘𝑛)) ↔ (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)))) |
| 50 | 11, 21, 49 | 3bitrd 305 |
. . . 4
⊢ (((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌)) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)))) |
| 51 | 50 | ad2antlr 727 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) ↔ (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)))) |
| 52 | | pm3.35 803 |
. . . . . . 7
⊢
((∀𝑖 ∈
(0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) |
| 53 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → ((𝑆 Σg 𝑋)‘𝑛) = ((𝑆 Σg 𝑋)‘𝑗)) |
| 54 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → ((𝑍 Σg 𝑌)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑗)) |
| 55 | 53, 54 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ↔ ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗))) |
| 56 | 55 | cbvralvw 3237 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ↔ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) |
| 57 | | simp-4l 783 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → 𝑁 ∈ Fin) |
| 58 | | simp-4r 784 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → 𝑀 ∈ Fin) |
| 59 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → 𝑛 ∈ 𝐼) |
| 60 | 57, 58, 59 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → (𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛 ∈ 𝐼)) |
| 61 | 60 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) ∧ (𝐶‘𝑛) = (𝑅‘𝑛)) → (𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛 ∈ 𝐼)) |
| 62 | | simp-4r 784 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) ∧ (𝐶‘𝑛) = (𝑅‘𝑛)) → ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) |
| 63 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) |
| 64 | 63 | anim1i 615 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) ∧ (𝐶‘𝑛) = (𝑅‘𝑛)) → (∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) ∧ (𝐶‘𝑛) = (𝑅‘𝑛))) |
| 65 | | gsmsymgrfix.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (SymGrp‘𝑁) |
| 66 | | gsmsymgrfix.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝑆) |
| 67 | | gsmsymgreq.z |
. . . . . . . . . . . . . . 15
⊢ 𝑍 = (SymGrp‘𝑀) |
| 68 | | gsmsymgreq.p |
. . . . . . . . . . . . . . 15
⊢ 𝑃 = (Base‘𝑍) |
| 69 | | gsmsymgreq.i |
. . . . . . . . . . . . . . 15
⊢ 𝐼 = (𝑁 ∩ 𝑀) |
| 70 | 65, 66, 67, 68, 69 | gsmsymgreqlem1 19448 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) ∧ (𝐶‘𝑛) = (𝑅‘𝑛)) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛))) |
| 71 | 70 | imp 406 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝑛 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ (∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) ∧ (𝐶‘𝑛) = (𝑅‘𝑛))) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)) |
| 72 | 61, 62, 64, 71 | syl21anc 838 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) ∧ (𝐶‘𝑛) = (𝑅‘𝑛)) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)) |
| 73 | 72 | ex 412 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑀 ∈ Fin) ∧
((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) ∧ 𝑛 ∈ 𝐼) → ((𝐶‘𝑛) = (𝑅‘𝑛) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛))) |
| 74 | 73 | ralimdva 3167 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ ∀𝑗 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗)) → (∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛))) |
| 75 | 74 | expcom 413 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
𝐼 ((𝑆 Σg 𝑋)‘𝑗) = ((𝑍 Σg 𝑌)‘𝑗) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → (∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
| 76 | 56, 75 | sylbi 217 |
. . . . . . . 8
⊢
(∀𝑛 ∈
𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → (∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
| 77 | 76 | com23 86 |
. . . . . . 7
⊢
(∀𝑛 ∈
𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) → (∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
| 78 | 52, 77 | syl 17 |
. . . . . 6
⊢
((∀𝑖 ∈
(0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → (∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
| 79 | 78 | impancom 451 |
. . . . 5
⊢
((∀𝑖 ∈
(0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
| 80 | 79 | com13 88 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |
| 81 | 80 | imp 406 |
. . 3
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) ∧ ∀𝑛 ∈ 𝐼 (𝐶‘𝑛) = (𝑅‘𝑛)) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛))) |
| 82 | 51, 81 | sylbid 240 |
. 2
⊢ ((((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) ∧ (∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛))) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛))) |
| 83 | 82 | ex 412 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) |