Step |
Hyp |
Ref |
Expression |
1 |
|
s1cl |
⊢ ( 𝑋 ∈ 𝑉 → 〈“ 𝑋 ”〉 ∈ Word 𝑉 ) |
2 |
1
|
adantr |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 〈“ 𝑋 ”〉 ∈ Word 𝑉 ) |
3 |
|
s1cl |
⊢ ( 𝑌 ∈ 𝑉 → 〈“ 𝑌 ”〉 ∈ Word 𝑉 ) |
4 |
3
|
adantl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 〈“ 𝑌 ”〉 ∈ Word 𝑉 ) |
5 |
|
1z |
⊢ 1 ∈ ℤ |
6 |
|
2z |
⊢ 2 ∈ ℤ |
7 |
|
1lt2 |
⊢ 1 < 2 |
8 |
|
fzolb |
⊢ ( 1 ∈ ( 1 ..^ 2 ) ↔ ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 < 2 ) ) |
9 |
5 6 7 8
|
mpbir3an |
⊢ 1 ∈ ( 1 ..^ 2 ) |
10 |
|
s1len |
⊢ ( ♯ ‘ 〈“ 𝑋 ”〉 ) = 1 |
11 |
|
s1len |
⊢ ( ♯ ‘ 〈“ 𝑌 ”〉 ) = 1 |
12 |
10 11
|
oveq12i |
⊢ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) + ( ♯ ‘ 〈“ 𝑌 ”〉 ) ) = ( 1 + 1 ) |
13 |
|
1p1e2 |
⊢ ( 1 + 1 ) = 2 |
14 |
12 13
|
eqtri |
⊢ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) + ( ♯ ‘ 〈“ 𝑌 ”〉 ) ) = 2 |
15 |
10 14
|
oveq12i |
⊢ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) ..^ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) + ( ♯ ‘ 〈“ 𝑌 ”〉 ) ) ) = ( 1 ..^ 2 ) |
16 |
9 15
|
eleqtrri |
⊢ 1 ∈ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) ..^ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) + ( ♯ ‘ 〈“ 𝑌 ”〉 ) ) ) |
17 |
16
|
a1i |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 1 ∈ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) ..^ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) + ( ♯ ‘ 〈“ 𝑌 ”〉 ) ) ) ) |
18 |
|
ccatval2 |
⊢ ( ( 〈“ 𝑋 ”〉 ∈ Word 𝑉 ∧ 〈“ 𝑌 ”〉 ∈ Word 𝑉 ∧ 1 ∈ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) ..^ ( ( ♯ ‘ 〈“ 𝑋 ”〉 ) + ( ♯ ‘ 〈“ 𝑌 ”〉 ) ) ) ) → ( ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ‘ 1 ) = ( 〈“ 𝑌 ”〉 ‘ ( 1 − ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) ) ) |
19 |
2 4 17 18
|
syl3anc |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ‘ 1 ) = ( 〈“ 𝑌 ”〉 ‘ ( 1 − ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) ) ) |
20 |
10
|
oveq2i |
⊢ ( 1 − ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) = ( 1 − 1 ) |
21 |
|
1m1e0 |
⊢ ( 1 − 1 ) = 0 |
22 |
20 21
|
eqtri |
⊢ ( 1 − ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) = 0 |
23 |
22
|
a1i |
⊢ ( 𝑌 ∈ 𝑉 → ( 1 − ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) = 0 ) |
24 |
23
|
fveq2d |
⊢ ( 𝑌 ∈ 𝑉 → ( 〈“ 𝑌 ”〉 ‘ ( 1 − ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) ) = ( 〈“ 𝑌 ”〉 ‘ 0 ) ) |
25 |
|
s1fv |
⊢ ( 𝑌 ∈ 𝑉 → ( 〈“ 𝑌 ”〉 ‘ 0 ) = 𝑌 ) |
26 |
24 25
|
eqtrd |
⊢ ( 𝑌 ∈ 𝑉 → ( 〈“ 𝑌 ”〉 ‘ ( 1 − ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) ) = 𝑌 ) |
27 |
26
|
adantl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 〈“ 𝑌 ”〉 ‘ ( 1 − ( ♯ ‘ 〈“ 𝑋 ”〉 ) ) ) = 𝑌 ) |
28 |
19 27
|
eqtrd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 〈“ 𝑋 ”〉 ++ 〈“ 𝑌 ”〉 ) ‘ 1 ) = 𝑌 ) |