Step |
Hyp |
Ref |
Expression |
1 |
|
cycpmco2.c |
⊢ 𝑀 = ( toCyc ‘ 𝐷 ) |
2 |
|
cycpmco2.s |
⊢ 𝑆 = ( SymGrp ‘ 𝐷 ) |
3 |
|
cycpmco2.d |
⊢ ( 𝜑 → 𝐷 ∈ 𝑉 ) |
4 |
|
cycpmco2.w |
⊢ ( 𝜑 → 𝑊 ∈ dom 𝑀 ) |
5 |
|
cycpmco2.i |
⊢ ( 𝜑 → 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) ) |
6 |
|
cycpmco2.j |
⊢ ( 𝜑 → 𝐽 ∈ ran 𝑊 ) |
7 |
|
cycpmco2.e |
⊢ 𝐸 = ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) |
8 |
|
cycpmco2.1 |
⊢ 𝑈 = ( 𝑊 splice 〈 𝐸 , 𝐸 , 〈“ 𝐼 ”〉 〉 ) |
9 |
|
cycpmco2lem.1 |
⊢ ( 𝜑 → 𝐾 ∈ ran 𝑊 ) |
10 |
|
cycpmco2lem5.1 |
⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) |
11 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → 𝐾 ∈ ran 𝑊 ) |
12 |
|
ovexd |
⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ V ) |
13 |
7 12
|
eqeltrid |
⊢ ( 𝜑 → 𝐸 ∈ V ) |
14 |
5
|
eldifad |
⊢ ( 𝜑 → 𝐼 ∈ 𝐷 ) |
15 |
14
|
s1cld |
⊢ ( 𝜑 → 〈“ 𝐼 ”〉 ∈ Word 𝐷 ) |
16 |
|
splval |
⊢ ( ( 𝑊 ∈ dom 𝑀 ∧ ( 𝐸 ∈ V ∧ 𝐸 ∈ V ∧ 〈“ 𝐼 ”〉 ∈ Word 𝐷 ) ) → ( 𝑊 splice 〈 𝐸 , 𝐸 , 〈“ 𝐼 ”〉 〉 ) = ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ++ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) |
17 |
4 13 13 15 16
|
syl13anc |
⊢ ( 𝜑 → ( 𝑊 splice 〈 𝐸 , 𝐸 , 〈“ 𝐼 ”〉 〉 ) = ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ++ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) |
18 |
8 17
|
syl5eq |
⊢ ( 𝜑 → 𝑈 = ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ++ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) |
19 |
18
|
fveq2d |
⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ++ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) ) |
20 |
|
ssrab2 |
⊢ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⊆ Word 𝐷 |
21 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
22 |
1 2 21
|
tocycf |
⊢ ( 𝐷 ∈ 𝑉 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) ) |
23 |
3 22
|
syl |
⊢ ( 𝜑 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) ) |
24 |
23
|
fdmd |
⊢ ( 𝜑 → dom 𝑀 = { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) |
25 |
4 24
|
eleqtrd |
⊢ ( 𝜑 → 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) |
26 |
20 25
|
sselid |
⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 ) |
27 |
|
pfxcl |
⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ) |
28 |
26 27
|
syl |
⊢ ( 𝜑 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ) |
29 |
|
ccatcl |
⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ 〈“ 𝐼 ”〉 ∈ Word 𝐷 ) → ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ∈ Word 𝐷 ) |
30 |
28 15 29
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ∈ Word 𝐷 ) |
31 |
|
swrdcl |
⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ∈ Word 𝐷 ) |
32 |
26 31
|
syl |
⊢ ( 𝜑 → ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ∈ Word 𝐷 ) |
33 |
|
ccatlen |
⊢ ( ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ∈ Word 𝐷 ∧ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ∈ Word 𝐷 ) → ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ++ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) = ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ) + ( ♯ ‘ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) ) |
34 |
30 32 33
|
syl2anc |
⊢ ( 𝜑 → ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ++ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) = ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ) + ( ♯ ‘ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) ) |
35 |
|
ccatws1len |
⊢ ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) ) |
36 |
28 35
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) ) |
37 |
|
id |
⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 ) |
38 |
|
dmeq |
⊢ ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 ) |
39 |
|
eqidd |
⊢ ( 𝑤 = 𝑊 → 𝐷 = 𝐷 ) |
40 |
37 38 39
|
f1eq123d |
⊢ ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) ) |
41 |
40
|
elrab |
⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) ) |
42 |
25 41
|
sylib |
⊢ ( 𝜑 → ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) ) |
43 |
42
|
simprd |
⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 ) |
44 |
|
f1cnv |
⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 ) |
45 |
43 44
|
syl |
⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 ) |
46 |
|
f1of |
⊢ ( ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 ) |
47 |
45 46
|
syl |
⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 ) |
48 |
47 6
|
ffvelrnd |
⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ dom 𝑊 ) |
49 |
|
wrddm |
⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
50 |
26 49
|
syl |
⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
51 |
48 50
|
eleqtrd |
⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
52 |
|
fzofzp1 |
⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
53 |
51 52
|
syl |
⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
54 |
7 53
|
eqeltrid |
⊢ ( 𝜑 → 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
55 |
|
pfxlen |
⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 ) |
56 |
26 54 55
|
syl2anc |
⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 ) |
57 |
56
|
oveq1d |
⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) = ( 𝐸 + 1 ) ) |
58 |
36 57
|
eqtrd |
⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ) = ( 𝐸 + 1 ) ) |
59 |
|
lencl |
⊢ ( 𝑊 ∈ Word 𝐷 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
60 |
26 59
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
61 |
|
nn0fz0 |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
62 |
60 61
|
sylib |
⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
63 |
|
swrdlen |
⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) = ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) |
64 |
26 54 62 63
|
syl3anc |
⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) = ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) |
65 |
58 64
|
oveq12d |
⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ) + ( ♯ ‘ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ) |
66 |
19 34 65
|
3eqtrd |
⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ) |
67 |
|
fz0ssnn0 |
⊢ ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℕ0 |
68 |
67 54
|
sselid |
⊢ ( 𝜑 → 𝐸 ∈ ℕ0 ) |
69 |
68
|
nn0zd |
⊢ ( 𝜑 → 𝐸 ∈ ℤ ) |
70 |
69
|
peano2zd |
⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℤ ) |
71 |
70
|
zcnd |
⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℂ ) |
72 |
60
|
nn0cnd |
⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℂ ) |
73 |
68
|
nn0cnd |
⊢ ( 𝜑 → 𝐸 ∈ ℂ ) |
74 |
71 72 73
|
addsubassd |
⊢ ( 𝜑 → ( ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) − 𝐸 ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ) |
75 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
76 |
73 75 72
|
addassd |
⊢ ( 𝜑 → ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) = ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) ) |
77 |
76
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) − 𝐸 ) = ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) ) |
78 |
66 74 77
|
3eqtr2d |
⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) ) |
79 |
75 72
|
addcld |
⊢ ( 𝜑 → ( 1 + ( ♯ ‘ 𝑊 ) ) ∈ ℂ ) |
80 |
73 79
|
pncan2d |
⊢ ( 𝜑 → ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) = ( 1 + ( ♯ ‘ 𝑊 ) ) ) |
81 |
75 72
|
addcomd |
⊢ ( 𝜑 → ( 1 + ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) |
82 |
78 80 81
|
3eqtrd |
⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) |
83 |
|
oveq1 |
⊢ ( ( ♯ ‘ 𝑊 ) = 𝐸 → ( ( ♯ ‘ 𝑊 ) + 1 ) = ( 𝐸 + 1 ) ) |
84 |
82 83
|
sylan9eq |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( ♯ ‘ 𝑈 ) = ( 𝐸 + 1 ) ) |
85 |
84
|
oveq1d |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ( 𝐸 + 1 ) − 1 ) ) |
86 |
73 75
|
pncand |
⊢ ( 𝜑 → ( ( 𝐸 + 1 ) − 1 ) = 𝐸 ) |
87 |
86
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( ( 𝐸 + 1 ) − 1 ) = 𝐸 ) |
88 |
85 87
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( ( ♯ ‘ 𝑈 ) − 1 ) = 𝐸 ) |
89 |
88
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( 𝑈 ‘ 𝐸 ) ) |
90 |
10
|
fveq2d |
⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) |
91 |
1 2 3 4 5 6 7 8
|
cycpmco2f1 |
⊢ ( 𝜑 → 𝑈 : dom 𝑈 –1-1→ 𝐷 ) |
92 |
|
f1f1orn |
⊢ ( 𝑈 : dom 𝑈 –1-1→ 𝐷 → 𝑈 : dom 𝑈 –1-1-onto→ ran 𝑈 ) |
93 |
91 92
|
syl |
⊢ ( 𝜑 → 𝑈 : dom 𝑈 –1-1-onto→ ran 𝑈 ) |
94 |
|
ssun1 |
⊢ ran 𝑊 ⊆ ( ran 𝑊 ∪ { 𝐼 } ) |
95 |
1 2 3 4 5 6 7 8
|
cycpmco2rn |
⊢ ( 𝜑 → ran 𝑈 = ( ran 𝑊 ∪ { 𝐼 } ) ) |
96 |
94 95
|
sseqtrrid |
⊢ ( 𝜑 → ran 𝑊 ⊆ ran 𝑈 ) |
97 |
96
|
sselda |
⊢ ( ( 𝜑 ∧ 𝐾 ∈ ran 𝑊 ) → 𝐾 ∈ ran 𝑈 ) |
98 |
|
f1ocnvfv2 |
⊢ ( ( 𝑈 : dom 𝑈 –1-1-onto→ ran 𝑈 ∧ 𝐾 ∈ ran 𝑈 ) → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = 𝐾 ) |
99 |
93 97 98
|
syl2an2r |
⊢ ( ( 𝜑 ∧ 𝐾 ∈ ran 𝑊 ) → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = 𝐾 ) |
100 |
9 99
|
mpdan |
⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = 𝐾 ) |
101 |
90 100
|
eqtr3d |
⊢ ( 𝜑 → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = 𝐾 ) |
102 |
101
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = 𝐾 ) |
103 |
1 2 3 4 5 6 7 8
|
cycpmco2lem2 |
⊢ ( 𝜑 → ( 𝑈 ‘ 𝐸 ) = 𝐼 ) |
104 |
103
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( 𝑈 ‘ 𝐸 ) = 𝐼 ) |
105 |
89 102 104
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → 𝐾 = 𝐼 ) |
106 |
5
|
eldifbd |
⊢ ( 𝜑 → ¬ 𝐼 ∈ ran 𝑊 ) |
107 |
106
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ¬ 𝐼 ∈ ran 𝑊 ) |
108 |
105 107
|
eqneltrd |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ¬ 𝐾 ∈ ran 𝑊 ) |
109 |
11 108
|
pm2.21dd |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) ) |
110 |
|
splcl |
⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 〈“ 𝐼 ”〉 ∈ Word 𝐷 ) → ( 𝑊 splice 〈 𝐸 , 𝐸 , 〈“ 𝐼 ”〉 〉 ) ∈ Word 𝐷 ) |
111 |
26 15 110
|
syl2anc |
⊢ ( 𝜑 → ( 𝑊 splice 〈 𝐸 , 𝐸 , 〈“ 𝐼 ”〉 〉 ) ∈ Word 𝐷 ) |
112 |
8 111
|
eqeltrid |
⊢ ( 𝜑 → 𝑈 ∈ Word 𝐷 ) |
113 |
|
nn0p1gt0 |
⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) ) |
114 |
60 113
|
syl |
⊢ ( 𝜑 → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) ) |
115 |
114 82
|
breqtrrd |
⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑈 ) ) |
116 |
|
eqidd |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) ) |
117 |
1 3 112 91 115 116
|
cycpmfv2 |
⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( 𝑈 ‘ 0 ) ) |
118 |
117
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( 𝑈 ‘ 0 ) ) |
119 |
|
f1f |
⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 ⟶ 𝐷 ) |
120 |
43 119
|
syl |
⊢ ( 𝜑 → 𝑊 : dom 𝑊 ⟶ 𝐷 ) |
121 |
120
|
frnd |
⊢ ( 𝜑 → ran 𝑊 ⊆ 𝐷 ) |
122 |
3 121
|
ssexd |
⊢ ( 𝜑 → ran 𝑊 ∈ V ) |
123 |
6
|
ne0d |
⊢ ( 𝜑 → ran 𝑊 ≠ ∅ ) |
124 |
|
hashgt0 |
⊢ ( ( ran 𝑊 ∈ V ∧ ran 𝑊 ≠ ∅ ) → 0 < ( ♯ ‘ ran 𝑊 ) ) |
125 |
122 123 124
|
syl2anc |
⊢ ( 𝜑 → 0 < ( ♯ ‘ ran 𝑊 ) ) |
126 |
4
|
dmexd |
⊢ ( 𝜑 → dom 𝑊 ∈ V ) |
127 |
|
hashf1rn |
⊢ ( ( dom 𝑊 ∈ V ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ran 𝑊 ) ) |
128 |
126 43 127
|
syl2anc |
⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ran 𝑊 ) ) |
129 |
125 128
|
breqtrrd |
⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑊 ) ) |
130 |
|
eqidd |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) |
131 |
1 3 26 43 129 130
|
cycpmfv2 |
⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ 0 ) ) |
132 |
131
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ 0 ) ) |
133 |
8
|
a1i |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 𝑈 = ( 𝑊 splice 〈 𝐸 , 𝐸 , 〈“ 𝐼 ”〉 〉 ) ) |
134 |
1 2 3 4 5 6 7 8
|
cycpmco2lem3 |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ♯ ‘ 𝑊 ) ) |
135 |
73 75
|
addcomd |
⊢ ( 𝜑 → ( 𝐸 + 1 ) = ( 1 + 𝐸 ) ) |
136 |
135
|
oveq2d |
⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) = ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 1 + 𝐸 ) ) ) |
137 |
72 75
|
subcld |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℂ ) |
138 |
137 73 75
|
nppcan3d |
⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 1 + 𝐸 ) ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) ) |
139 |
72 75
|
npcand |
⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) ) |
140 |
136 138 139
|
3eqtrd |
⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) = ( ♯ ‘ 𝑊 ) ) |
141 |
134 140
|
eqtr4d |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) ) |
142 |
141
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) ) |
143 |
133 142
|
fveq12d |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( ( 𝑊 splice 〈 𝐸 , 𝐸 , 〈“ 𝐼 ”〉 〉 ) ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) ) ) |
144 |
26
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 𝑊 ∈ Word 𝐷 ) |
145 |
|
nn0fz0 |
⊢ ( 𝐸 ∈ ℕ0 ↔ 𝐸 ∈ ( 0 ... 𝐸 ) ) |
146 |
68 145
|
sylib |
⊢ ( 𝜑 → 𝐸 ∈ ( 0 ... 𝐸 ) ) |
147 |
146
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 𝐸 ∈ ( 0 ... 𝐸 ) ) |
148 |
54
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) |
149 |
15
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 〈“ 𝐼 ”〉 ∈ Word 𝐷 ) |
150 |
72
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ♯ ‘ 𝑊 ) ∈ ℂ ) |
151 |
|
1cnd |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 1 ∈ ℂ ) |
152 |
73
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 𝐸 ∈ ℂ ) |
153 |
150 151 152
|
sub32d |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) = ( ( ( ♯ ‘ 𝑊 ) − 𝐸 ) − 1 ) ) |
154 |
|
fznn0sub |
⊢ ( 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℕ0 ) |
155 |
54 154
|
syl |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℕ0 ) |
156 |
155
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℕ0 ) |
157 |
|
simpr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) |
158 |
150 152 156 157
|
subne0nn |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℕ ) |
159 |
|
fzo0end |
⊢ ( ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℕ → ( ( ( ♯ ‘ 𝑊 ) − 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ) |
160 |
158 159
|
syl |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ( ♯ ‘ 𝑊 ) − 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ) |
161 |
153 160
|
eqeltrd |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ) |
162 |
|
s1len |
⊢ ( ♯ ‘ 〈“ 𝐼 ”〉 ) = 1 |
163 |
162
|
eqcomi |
⊢ 1 = ( ♯ ‘ 〈“ 𝐼 ”〉 ) |
164 |
163
|
oveq2i |
⊢ ( 𝐸 + 1 ) = ( 𝐸 + ( ♯ ‘ 〈“ 𝐼 ”〉 ) ) |
165 |
164
|
a1i |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝐸 + 1 ) = ( 𝐸 + ( ♯ ‘ 〈“ 𝐼 ”〉 ) ) ) |
166 |
144 147 148 149 161 165
|
splfv3 |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( 𝑊 splice 〈 𝐸 , 𝐸 , 〈“ 𝐼 ”〉 〉 ) ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) ) = ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + 𝐸 ) ) ) |
167 |
137 73
|
npcand |
⊢ ( 𝜑 → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + 𝐸 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) ) |
168 |
167
|
fveq2d |
⊢ ( 𝜑 → ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + 𝐸 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
169 |
168
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + 𝐸 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
170 |
143 166 169
|
3eqtrd |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) |
171 |
170
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) ) |
172 |
18
|
fveq1d |
⊢ ( 𝜑 → ( 𝑈 ‘ 0 ) = ( ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ++ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ‘ 0 ) ) |
173 |
|
nn0p1nn |
⊢ ( 𝐸 ∈ ℕ0 → ( 𝐸 + 1 ) ∈ ℕ ) |
174 |
68 173
|
syl |
⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℕ ) |
175 |
|
lbfzo0 |
⊢ ( 0 ∈ ( 0 ..^ ( 𝐸 + 1 ) ) ↔ ( 𝐸 + 1 ) ∈ ℕ ) |
176 |
174 175
|
sylibr |
⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( 𝐸 + 1 ) ) ) |
177 |
58
|
oveq2d |
⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ) ) = ( 0 ..^ ( 𝐸 + 1 ) ) ) |
178 |
176 177
|
eleqtrrd |
⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ) ) ) |
179 |
|
ccatval1 |
⊢ ( ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ∈ Word 𝐷 ∧ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ∈ Word 𝐷 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ) ) ) → ( ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ++ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ‘ 0 ) = ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ‘ 0 ) ) |
180 |
30 32 178 179
|
syl3anc |
⊢ ( 𝜑 → ( ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ++ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ‘ 0 ) = ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ‘ 0 ) ) |
181 |
|
elfzonn0 |
⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 ) |
182 |
51 181
|
syl |
⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 ) |
183 |
|
nn0p1nn |
⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ℕ ) |
184 |
182 183
|
syl |
⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ℕ ) |
185 |
7 184
|
eqeltrid |
⊢ ( 𝜑 → 𝐸 ∈ ℕ ) |
186 |
|
lbfzo0 |
⊢ ( 0 ∈ ( 0 ..^ 𝐸 ) ↔ 𝐸 ∈ ℕ ) |
187 |
185 186
|
sylibr |
⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝐸 ) ) |
188 |
56
|
oveq2d |
⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) = ( 0 ..^ 𝐸 ) ) |
189 |
187 188
|
eleqtrrd |
⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) ) |
190 |
|
ccatval1 |
⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ 〈“ 𝐼 ”〉 ∈ Word 𝐷 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) ) → ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ‘ 0 ) = ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) ) |
191 |
28 15 189 190
|
syl3anc |
⊢ ( 𝜑 → ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ‘ 0 ) = ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) ) |
192 |
|
nn0p1gt0 |
⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 → 0 < ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ) |
193 |
182 192
|
syl |
⊢ ( 𝜑 → 0 < ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ) |
194 |
193 7
|
breqtrrdi |
⊢ ( 𝜑 → 0 < 𝐸 ) |
195 |
194
|
gt0ne0d |
⊢ ( 𝜑 → 𝐸 ≠ 0 ) |
196 |
|
fzne1 |
⊢ ( ( 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐸 ≠ 0 ) → 𝐸 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝑊 ) ) ) |
197 |
54 195 196
|
syl2anc |
⊢ ( 𝜑 → 𝐸 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝑊 ) ) ) |
198 |
|
0p1e1 |
⊢ ( 0 + 1 ) = 1 |
199 |
198
|
oveq1i |
⊢ ( ( 0 + 1 ) ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... ( ♯ ‘ 𝑊 ) ) |
200 |
197 199
|
eleqtrdi |
⊢ ( 𝜑 → 𝐸 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) |
201 |
|
pfxfv0 |
⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
202 |
26 200 201
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
203 |
180 191 202
|
3eqtrd |
⊢ ( 𝜑 → ( ( ( ( 𝑊 prefix 𝐸 ) ++ 〈“ 𝐼 ”〉 ) ++ ( 𝑊 substr 〈 𝐸 , ( ♯ ‘ 𝑊 ) 〉 ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
204 |
172 203
|
eqtrd |
⊢ ( 𝜑 → ( 𝑈 ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
205 |
204
|
adantr |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝑈 ‘ 0 ) = ( 𝑊 ‘ 0 ) ) |
206 |
132 171 205
|
3eqtr4rd |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝑈 ‘ 0 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) ) |
207 |
118 206
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) ) |
208 |
109 207
|
pm2.61dane |
⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) ) |
209 |
101
|
fveq2d |
⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) ) |
210 |
101
|
fveq2d |
⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) ) |
211 |
208 209 210
|
3eqtr3d |
⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) ) |