Step |
Hyp |
Ref |
Expression |
1 |
|
efgval.w |
⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) ) |
2 |
|
efgval.r |
⊢ ∼ = ( ~FG ‘ 𝐼 ) |
3 |
|
efgval2.m |
⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ) |
4 |
|
efgval2.t |
⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice 〈 𝑛 , 𝑛 , 〈“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”〉 〉 ) ) ) |
5 |
|
efgred.d |
⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) ) |
6 |
|
efgred.s |
⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) ) |
7 |
|
efgcpbllem.1 |
⊢ 𝐿 = { 〈 𝑖 , 𝑗 〉 ∣ ( { 𝑖 , 𝑗 } ⊆ 𝑊 ∧ ( ( 𝐴 ++ 𝑖 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑗 ) ++ 𝐵 ) ) } |
8 |
1 2 3 4
|
efgval2 |
⊢ ∼ = ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } |
9 |
7
|
relopabi |
⊢ Rel 𝐿 |
10 |
9
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → Rel 𝐿 ) |
11 |
1 2 3 4 5 6 7
|
efgcpbllema |
⊢ ( 𝑓 𝐿 𝑔 ↔ ( 𝑓 ∈ 𝑊 ∧ 𝑔 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ) ) |
12 |
11
|
simp2bi |
⊢ ( 𝑓 𝐿 𝑔 → 𝑔 ∈ 𝑊 ) |
13 |
12
|
adantl |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → 𝑔 ∈ 𝑊 ) |
14 |
11
|
simp1bi |
⊢ ( 𝑓 𝐿 𝑔 → 𝑓 ∈ 𝑊 ) |
15 |
14
|
adantl |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → 𝑓 ∈ 𝑊 ) |
16 |
1 2
|
efger |
⊢ ∼ Er 𝑊 |
17 |
16
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → ∼ Er 𝑊 ) |
18 |
11
|
simp3bi |
⊢ ( 𝑓 𝐿 𝑔 → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ) |
19 |
18
|
adantl |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ) |
20 |
17 19
|
ersym |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) |
21 |
1 2 3 4 5 6 7
|
efgcpbllema |
⊢ ( 𝑔 𝐿 𝑓 ↔ ( 𝑔 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) |
22 |
13 15 20 21
|
syl3anbrc |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 𝐿 𝑔 ) → 𝑔 𝐿 𝑓 ) |
23 |
14
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → 𝑓 ∈ 𝑊 ) |
24 |
1 2 3 4 5 6 7
|
efgcpbllema |
⊢ ( 𝑔 𝐿 ℎ ↔ ( 𝑔 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ℎ ) ++ 𝐵 ) ) ) |
25 |
24
|
simp2bi |
⊢ ( 𝑔 𝐿 ℎ → ℎ ∈ 𝑊 ) |
26 |
25
|
ad2antll |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → ℎ ∈ 𝑊 ) |
27 |
16
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → ∼ Er 𝑊 ) |
28 |
18
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ) |
29 |
24
|
simp3bi |
⊢ ( 𝑔 𝐿 ℎ → ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ℎ ) ++ 𝐵 ) ) |
30 |
29
|
ad2antll |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → ( ( 𝐴 ++ 𝑔 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ℎ ) ++ 𝐵 ) ) |
31 |
27 28 30
|
ertrd |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ℎ ) ++ 𝐵 ) ) |
32 |
1 2 3 4 5 6 7
|
efgcpbllema |
⊢ ( 𝑓 𝐿 ℎ ↔ ( 𝑓 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ℎ ) ++ 𝐵 ) ) ) |
33 |
23 26 31 32
|
syl3anbrc |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑓 𝐿 𝑔 ∧ 𝑔 𝐿 ℎ ) ) → 𝑓 𝐿 ℎ ) |
34 |
16
|
a1i |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ∼ Er 𝑊 ) |
35 |
|
fviss |
⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o ) |
36 |
1 35
|
eqsstri |
⊢ 𝑊 ⊆ Word ( 𝐼 × 2o ) |
37 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐴 ∈ 𝑊 ) |
38 |
36 37
|
sseldi |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐴 ∈ Word ( 𝐼 × 2o ) ) |
39 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝑓 ∈ 𝑊 ) |
40 |
36 39
|
sseldi |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝑓 ∈ Word ( 𝐼 × 2o ) ) |
41 |
|
ccatcl |
⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ 𝑓 ∈ Word ( 𝐼 × 2o ) ) → ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2o ) ) |
42 |
38 40 41
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2o ) ) |
43 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 ) |
44 |
36 43
|
sseldi |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝐵 ∈ Word ( 𝐼 × 2o ) ) |
45 |
|
ccatcl |
⊢ ( ( ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2o ) ) |
46 |
42 44 45
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2o ) ) |
47 |
1
|
efgrcl |
⊢ ( 𝐴 ∈ 𝑊 → ( 𝐼 ∈ V ∧ 𝑊 = Word ( 𝐼 × 2o ) ) ) |
48 |
47
|
simprd |
⊢ ( 𝐴 ∈ 𝑊 → 𝑊 = Word ( 𝐼 × 2o ) ) |
49 |
48
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → 𝑊 = Word ( 𝐼 × 2o ) ) |
50 |
46 49
|
eleqtrrd |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 ) |
51 |
34 50
|
erref |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) |
52 |
51
|
ex |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑓 ∈ 𝑊 → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) |
53 |
52
|
pm4.71d |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑓 ∈ 𝑊 ↔ ( 𝑓 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ) |
54 |
1 2 3 4 5 6 7
|
efgcpbllema |
⊢ ( 𝑓 𝐿 𝑓 ↔ ( 𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) |
55 |
|
df-3an |
⊢ ( ( 𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ↔ ( ( 𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ) ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) |
56 |
|
anidm |
⊢ ( ( 𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ) ↔ 𝑓 ∈ 𝑊 ) |
57 |
56
|
anbi1i |
⊢ ( ( ( 𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ) ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ↔ ( 𝑓 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) |
58 |
54 55 57
|
3bitri |
⊢ ( 𝑓 𝐿 𝑓 ↔ ( 𝑓 ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) |
59 |
53 58
|
bitr4di |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑓 ∈ 𝑊 ↔ 𝑓 𝐿 𝑓 ) ) |
60 |
10 22 33 59
|
iserd |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐿 Er 𝑊 ) |
61 |
1 2 3 4
|
efgtf |
⊢ ( 𝑓 ∈ 𝑊 → ( ( 𝑇 ‘ 𝑓 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑓 splice 〈 𝑎 , 𝑎 , 〈“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”〉 〉 ) ) ∧ ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) ) |
62 |
61
|
simprd |
⊢ ( 𝑓 ∈ 𝑊 → ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) |
63 |
62
|
adantl |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) |
64 |
|
ffn |
⊢ ( ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 → ( 𝑇 ‘ 𝑓 ) Fn ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ) |
65 |
|
ovelrn |
⊢ ( ( 𝑇 ‘ 𝑓 ) Fn ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) → ( 𝑎 ∈ ran ( 𝑇 ‘ 𝑓 ) ↔ ∃ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∃ 𝑢 ∈ ( 𝐼 × 2o ) 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ) |
66 |
63 64 65
|
3syl |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑎 ∈ ran ( 𝑇 ‘ 𝑓 ) ↔ ∃ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∃ 𝑢 ∈ ( 𝐼 × 2o ) 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ) |
67 |
|
simplr |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑓 ∈ 𝑊 ) |
68 |
62
|
ad2antlr |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑇 ‘ 𝑓 ) : ( ( 0 ... ( ♯ ‘ 𝑓 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) |
69 |
|
simprl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ) |
70 |
|
simprr |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑢 ∈ ( 𝐼 × 2o ) ) |
71 |
68 69 70
|
fovrnd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ∈ 𝑊 ) |
72 |
50
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 ) |
73 |
37
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝐴 ∈ 𝑊 ) |
74 |
36 73
|
sseldi |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝐴 ∈ Word ( 𝐼 × 2o ) ) |
75 |
40
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑓 ∈ Word ( 𝐼 × 2o ) ) |
76 |
|
pfxcl |
⊢ ( 𝑓 ∈ Word ( 𝐼 × 2o ) → ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ) |
77 |
75 76
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ) |
78 |
|
ccatcl |
⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ) → ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2o ) ) |
79 |
74 77 78
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2o ) ) |
80 |
3
|
efgmf |
⊢ 𝑀 : ( 𝐼 × 2o ) ⟶ ( 𝐼 × 2o ) |
81 |
80
|
ffvelrni |
⊢ ( 𝑢 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ 𝑢 ) ∈ ( 𝐼 × 2o ) ) |
82 |
81
|
ad2antll |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑀 ‘ 𝑢 ) ∈ ( 𝐼 × 2o ) ) |
83 |
70 82
|
s2cld |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ∈ Word ( 𝐼 × 2o ) ) |
84 |
|
ccatcl |
⊢ ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2o ) ∧ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ∈ Word ( 𝐼 × 2o ) ) |
85 |
79 83 84
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ∈ Word ( 𝐼 × 2o ) ) |
86 |
|
swrdcl |
⊢ ( 𝑓 ∈ Word ( 𝐼 × 2o ) → ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ∈ Word ( 𝐼 × 2o ) ) |
87 |
75 86
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ∈ Word ( 𝐼 × 2o ) ) |
88 |
44
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝐵 ∈ Word ( 𝐼 × 2o ) ) |
89 |
|
ccatass |
⊢ ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2o ) ) → ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ++ 𝐵 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ) ) |
90 |
85 87 88 89
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ++ 𝐵 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ) ) |
91 |
|
ccatcl |
⊢ ( ( ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ∧ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ∈ Word ( 𝐼 × 2o ) ) |
92 |
77 83 91
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ∈ Word ( 𝐼 × 2o ) ) |
93 |
|
ccatass |
⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) = ( 𝐴 ++ ( ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) ) |
94 |
74 92 87 93
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) = ( 𝐴 ++ ( ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) ) |
95 |
|
ccatass |
⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ∧ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ) ) |
96 |
74 77 83 95
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ) ) |
97 |
96
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) = ( ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) |
98 |
1 2 3 4
|
efgtval |
⊢ ( ( 𝑓 ∈ 𝑊 ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) = ( 𝑓 splice 〈 𝑐 , 𝑐 , 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 〉 ) ) |
99 |
67 69 70 98
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) = ( 𝑓 splice 〈 𝑐 , 𝑐 , 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 〉 ) ) |
100 |
|
splval |
⊢ ( ( 𝑓 ∈ 𝑊 ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ∈ Word ( 𝐼 × 2o ) ) ) → ( 𝑓 splice 〈 𝑐 , 𝑐 , 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 〉 ) = ( ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) |
101 |
67 69 69 83 100
|
syl13anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑓 splice 〈 𝑐 , 𝑐 , 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 〉 ) = ( ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) |
102 |
99 101
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) = ( ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) |
103 |
102
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) = ( 𝐴 ++ ( ( ( 𝑓 prefix 𝑐 ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) ) |
104 |
94 97 103
|
3eqtr4rd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) |
105 |
104
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) = ( ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ++ 𝐵 ) ) |
106 |
|
lencl |
⊢ ( 𝐴 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) |
107 |
74 106
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) |
108 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
109 |
107 108
|
eleqtrdi |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) ) |
110 |
|
elfznn0 |
⊢ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) → 𝑐 ∈ ℕ0 ) |
111 |
110
|
ad2antrl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑐 ∈ ℕ0 ) |
112 |
|
uzaddcl |
⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑐 ∈ ℕ0 ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( ℤ≥ ‘ 0 ) ) |
113 |
109 111 112
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( ℤ≥ ‘ 0 ) ) |
114 |
42
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2o ) ) |
115 |
|
ccatlen |
⊢ ( ( ( 𝐴 ++ 𝑓 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) = ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) ) |
116 |
114 88 115
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) = ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) ) |
117 |
|
ccatlen |
⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ 𝑓 ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) ) |
118 |
74 75 117
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) ) |
119 |
|
elfzuz3 |
⊢ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) → ( ♯ ‘ 𝑓 ) ∈ ( ℤ≥ ‘ 𝑐 ) ) |
120 |
119
|
ad2antrl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ( ℤ≥ ‘ 𝑐 ) ) |
121 |
107
|
nn0zd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℤ ) |
122 |
|
eluzadd |
⊢ ( ( ( ♯ ‘ 𝑓 ) ∈ ( ℤ≥ ‘ 𝑐 ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℤ ) → ( ( ♯ ‘ 𝑓 ) + ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( 𝑐 + ( ♯ ‘ 𝐴 ) ) ) ) |
123 |
120 121 122
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝑓 ) + ( ♯ ‘ 𝐴 ) ) ∈ ( ℤ≥ ‘ ( 𝑐 + ( ♯ ‘ 𝐴 ) ) ) ) |
124 |
|
lencl |
⊢ ( 𝑓 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝑓 ) ∈ ℕ0 ) |
125 |
75 124
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ℕ0 ) |
126 |
125
|
nn0cnd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ℂ ) |
127 |
107
|
nn0cnd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℂ ) |
128 |
126 127
|
addcomd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝑓 ) + ( ♯ ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) ) |
129 |
111
|
nn0cnd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑐 ∈ ℂ ) |
130 |
129 127
|
addcomd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑐 + ( ♯ ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) |
131 |
130
|
fveq2d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ℤ≥ ‘ ( 𝑐 + ( ♯ ‘ 𝐴 ) ) ) = ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ) |
132 |
123 128 131
|
3eltr3d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝑓 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ) |
133 |
118 132
|
eqeltrd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ) |
134 |
|
lencl |
⊢ ( 𝐵 ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) |
135 |
88 134
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) |
136 |
|
uzaddcl |
⊢ ( ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ) |
137 |
133 135 136
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ ( 𝐴 ++ 𝑓 ) ) + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ) |
138 |
116 137
|
eqeltrd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ) |
139 |
|
elfzuzb |
⊢ ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ↔ ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) ) ) |
140 |
113 138 139
|
sylanbrc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ) |
141 |
1 2 3 4
|
efgtval |
⊢ ( ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 ∧ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) = ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice 〈 ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 〉 ) ) |
142 |
72 140 70 141
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) = ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice 〈 ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 〉 ) ) |
143 |
|
wrd0 |
⊢ ∅ ∈ Word ( 𝐼 × 2o ) |
144 |
143
|
a1i |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ∅ ∈ Word ( 𝐼 × 2o ) ) |
145 |
|
ccatcl |
⊢ ( ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2o ) ) |
146 |
87 88 145
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ∈ Word ( 𝐼 × 2o ) ) |
147 |
|
ccatrid |
⊢ ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2o ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) = ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) |
148 |
79 147
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) = ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) |
149 |
148
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) ++ ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ) = ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ) ) |
150 |
|
ccatass |
⊢ ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ∈ Word ( 𝐼 × 2o ) ∧ 𝐵 ∈ Word ( 𝐼 × 2o ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ++ 𝐵 ) = ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ) ) |
151 |
79 87 88 150
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ++ 𝐵 ) = ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ) ) |
152 |
|
ccatass |
⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ∈ Word ( 𝐼 × 2o ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) ) |
153 |
74 77 87 152
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) = ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) ) |
154 |
125 108
|
eleqtrdi |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ( ℤ≥ ‘ 0 ) ) |
155 |
|
eluzfz2 |
⊢ ( ( ♯ ‘ 𝑓 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ 𝑓 ) ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ) |
156 |
154 155
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ 𝑓 ) ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ) |
157 |
|
ccatpfx |
⊢ ( ( 𝑓 ∈ Word ( 𝐼 × 2o ) ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ ( ♯ ‘ 𝑓 ) ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) = ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) ) |
158 |
75 69 156 157
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) = ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) ) |
159 |
|
pfxid |
⊢ ( 𝑓 ∈ Word ( 𝐼 × 2o ) → ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) = 𝑓 ) |
160 |
75 159
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑓 prefix ( ♯ ‘ 𝑓 ) ) = 𝑓 ) |
161 |
158 160
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) = 𝑓 ) |
162 |
161
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝐴 ++ ( ( 𝑓 prefix 𝑐 ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ) = ( 𝐴 ++ 𝑓 ) ) |
163 |
153 162
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) = ( 𝐴 ++ 𝑓 ) ) |
164 |
163
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ) ++ 𝐵 ) = ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) |
165 |
149 151 164
|
3eqtr2rd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ ∅ ) ++ ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ) ) |
166 |
|
ccatlen |
⊢ ( ( 𝐴 ∈ Word ( 𝐼 × 2o ) ∧ ( 𝑓 prefix 𝑐 ) ∈ Word ( 𝐼 × 2o ) ) → ( ♯ ‘ ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) ) ) |
167 |
74 77 166
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) ) ) |
168 |
|
pfxlen |
⊢ ( ( 𝑓 ∈ Word ( 𝐼 × 2o ) ∧ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ) → ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) = 𝑐 ) |
169 |
75 69 168
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) = 𝑐 ) |
170 |
169
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ ( 𝑓 prefix 𝑐 ) ) ) = ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) |
171 |
167 170
|
eqtr2d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) = ( ♯ ‘ ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ) ) |
172 |
|
hash0 |
⊢ ( ♯ ‘ ∅ ) = 0 |
173 |
172
|
oveq2i |
⊢ ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + ( ♯ ‘ ∅ ) ) = ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + 0 ) |
174 |
107 111
|
nn0addcld |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ℕ0 ) |
175 |
174
|
nn0cnd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ℂ ) |
176 |
175
|
addid1d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + 0 ) = ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ) |
177 |
173 176
|
syl5req |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ♯ ‘ 𝐴 ) + 𝑐 ) = ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) + ( ♯ ‘ ∅ ) ) ) |
178 |
79 144 146 83 165 171 177
|
splval2 |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice 〈 ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , ( ( ♯ ‘ 𝐴 ) + 𝑐 ) , 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 〉 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ) ) |
179 |
142 178
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) = ( ( ( 𝐴 ++ ( 𝑓 prefix 𝑐 ) ) ++ 〈“ 𝑢 ( 𝑀 ‘ 𝑢 ) ”〉 ) ++ ( ( 𝑓 substr 〈 𝑐 , ( ♯ ‘ 𝑓 ) 〉 ) ++ 𝐵 ) ) ) |
180 |
90 105 179
|
3eqtr4d |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) = ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) ) |
181 |
1 2 3 4
|
efgtf |
⊢ ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 → ( ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) splice 〈 𝑎 , 𝑎 , 〈“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”〉 〉 ) ) ∧ ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) : ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) ) |
182 |
181
|
simprd |
⊢ ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 → ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) : ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) |
183 |
|
ffn |
⊢ ( ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) : ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 → ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) Fn ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) ) |
184 |
72 182 183
|
3syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) Fn ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) ) |
185 |
|
fnovrn |
⊢ ( ( ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) Fn ( ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) × ( 𝐼 × 2o ) ) ∧ ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ∈ ( 0 ... ( ♯ ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) |
186 |
184 140 70 185
|
syl3anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( ( ♯ ‘ 𝐴 ) + 𝑐 ) ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) 𝑢 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) |
187 |
180 186
|
eqeltrd |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) |
188 |
1 2 3 4
|
efgi2 |
⊢ ( ( ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∈ 𝑊 ∧ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ∈ ran ( 𝑇 ‘ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ) |
189 |
72 187 188
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ) |
190 |
1 2 3 4 5 6 7
|
efgcpbllema |
⊢ ( 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ↔ ( 𝑓 ∈ 𝑊 ∧ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ∈ 𝑊 ∧ ( ( 𝐴 ++ 𝑓 ) ++ 𝐵 ) ∼ ( ( 𝐴 ++ ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ++ 𝐵 ) ) ) |
191 |
67 71 189 190
|
syl3anbrc |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) |
192 |
|
vex |
⊢ 𝑎 ∈ V |
193 |
|
vex |
⊢ 𝑓 ∈ V |
194 |
192 193
|
elec |
⊢ ( 𝑎 ∈ [ 𝑓 ] 𝐿 ↔ 𝑓 𝐿 𝑎 ) |
195 |
|
breq2 |
⊢ ( 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → ( 𝑓 𝐿 𝑎 ↔ 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ) |
196 |
194 195
|
syl5bb |
⊢ ( 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → ( 𝑎 ∈ [ 𝑓 ] 𝐿 ↔ 𝑓 𝐿 ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) ) ) |
197 |
191 196
|
syl5ibrcom |
⊢ ( ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) ∧ ( 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∧ 𝑢 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → 𝑎 ∈ [ 𝑓 ] 𝐿 ) ) |
198 |
197
|
rexlimdvva |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( ∃ 𝑐 ∈ ( 0 ... ( ♯ ‘ 𝑓 ) ) ∃ 𝑢 ∈ ( 𝐼 × 2o ) 𝑎 = ( 𝑐 ( 𝑇 ‘ 𝑓 ) 𝑢 ) → 𝑎 ∈ [ 𝑓 ] 𝐿 ) ) |
199 |
66 198
|
sylbid |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ( 𝑎 ∈ ran ( 𝑇 ‘ 𝑓 ) → 𝑎 ∈ [ 𝑓 ] 𝐿 ) ) |
200 |
199
|
ssrdv |
⊢ ( ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑓 ∈ 𝑊 ) → ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) |
201 |
200
|
ralrimiva |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) |
202 |
1
|
fvexi |
⊢ 𝑊 ∈ V |
203 |
|
erex |
⊢ ( 𝐿 Er 𝑊 → ( 𝑊 ∈ V → 𝐿 ∈ V ) ) |
204 |
60 202 203
|
mpisyl |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐿 ∈ V ) |
205 |
|
ereq1 |
⊢ ( 𝑟 = 𝐿 → ( 𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊 ) ) |
206 |
|
eceq2 |
⊢ ( 𝑟 = 𝐿 → [ 𝑓 ] 𝑟 = [ 𝑓 ] 𝐿 ) |
207 |
206
|
sseq2d |
⊢ ( 𝑟 = 𝐿 → ( ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ↔ ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) ) |
208 |
207
|
ralbidv |
⊢ ( 𝑟 = 𝐿 → ( ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ↔ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) ) |
209 |
205 208
|
anbi12d |
⊢ ( 𝑟 = 𝐿 → ( ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) ↔ ( 𝐿 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) ) ) |
210 |
209
|
elabg |
⊢ ( 𝐿 ∈ V → ( 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } ↔ ( 𝐿 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) ) ) |
211 |
204 210
|
syl |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } ↔ ( 𝐿 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝐿 ) ) ) |
212 |
60 201 211
|
mpbir2and |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } ) |
213 |
|
intss1 |
⊢ ( 𝐿 ∈ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } ⊆ 𝐿 ) |
214 |
212 213
|
syl |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ∩ { 𝑟 ∣ ( 𝑟 Er 𝑊 ∧ ∀ 𝑓 ∈ 𝑊 ran ( 𝑇 ‘ 𝑓 ) ⊆ [ 𝑓 ] 𝑟 ) } ⊆ 𝐿 ) |
215 |
8 214
|
eqsstrid |
⊢ ( ( 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊 ) → ∼ ⊆ 𝐿 ) |