Step | Hyp | Ref
| Expression |
1 | | cycpmco2.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
2 | | cycpmco2.c |
. . . . . . . 8
⊢ 𝑀 = (toCyc‘𝐷) |
3 | | cycpmco2.s |
. . . . . . . 8
⊢ 𝑆 = (SymGrp‘𝐷) |
4 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘𝑆) |
5 | 2, 3, 4 | tocycf 30953 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
6 | 1, 5 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘𝑆)) |
7 | | cycpmco2.w |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ dom 𝑀) |
8 | 6 | fdmd 6509 |
. . . . . . 7
⊢ (𝜑 → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
9 | 7, 8 | eleqtrd 2835 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
10 | 6, 9 | ffvelrnd 6856 |
. . . . 5
⊢ (𝜑 → (𝑀‘𝑊) ∈ (Base‘𝑆)) |
11 | 3, 4 | symgbasf 18615 |
. . . . 5
⊢ ((𝑀‘𝑊) ∈ (Base‘𝑆) → (𝑀‘𝑊):𝐷⟶𝐷) |
12 | 10, 11 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑀‘𝑊):𝐷⟶𝐷) |
13 | 12 | ffnd 6499 |
. . 3
⊢ (𝜑 → (𝑀‘𝑊) Fn 𝐷) |
14 | | cycpmco2.i |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) |
15 | 14 | eldifad 3853 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝐷) |
16 | | ssrab2 3967 |
. . . . . . . . . . 11
⊢ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ⊆ Word 𝐷 |
17 | 16, 9 | sseldi 3873 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ Word 𝐷) |
18 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
19 | | dmeq 5740 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) |
20 | | eqidd 2739 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) |
21 | 18, 19, 20 | f1eq123d 6604 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) |
22 | 21 | elrab3 3586 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ 𝑊:dom 𝑊–1-1→𝐷)) |
23 | 22 | biimpa 480 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) → 𝑊:dom 𝑊–1-1→𝐷) |
24 | 17, 9, 23 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) |
25 | | f1f 6568 |
. . . . . . . . 9
⊢ (𝑊:dom 𝑊–1-1→𝐷 → 𝑊:dom 𝑊⟶𝐷) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑊:dom 𝑊⟶𝐷) |
27 | 26 | frnd 6506 |
. . . . . . 7
⊢ (𝜑 → ran 𝑊 ⊆ 𝐷) |
28 | | cycpmco2.j |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ran 𝑊) |
29 | 27, 28 | sseldd 3876 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ 𝐷) |
30 | 14 | eldifbd 3854 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝐼 ∈ ran 𝑊) |
31 | | nelne2 3031 |
. . . . . . . 8
⊢ ((𝐽 ∈ ran 𝑊 ∧ ¬ 𝐼 ∈ ran 𝑊) → 𝐽 ≠ 𝐼) |
32 | 28, 30, 31 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ≠ 𝐼) |
33 | 32 | necomd 2989 |
. . . . . 6
⊢ (𝜑 → 𝐼 ≠ 𝐽) |
34 | 2, 1, 15, 29, 33, 3 | cycpm2cl 30956 |
. . . . 5
⊢ (𝜑 → (𝑀‘〈“𝐼𝐽”〉) ∈ (Base‘𝑆)) |
35 | 3, 4 | symgbasf 18615 |
. . . . 5
⊢ ((𝑀‘〈“𝐼𝐽”〉) ∈ (Base‘𝑆) → (𝑀‘〈“𝐼𝐽”〉):𝐷⟶𝐷) |
36 | 34, 35 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑀‘〈“𝐼𝐽”〉):𝐷⟶𝐷) |
37 | 36 | ffnd 6499 |
. . 3
⊢ (𝜑 → (𝑀‘〈“𝐼𝐽”〉) Fn 𝐷) |
38 | 36 | frnd 6506 |
. . 3
⊢ (𝜑 → ran (𝑀‘〈“𝐼𝐽”〉) ⊆ 𝐷) |
39 | | fnco 6447 |
. . 3
⊢ (((𝑀‘𝑊) Fn 𝐷 ∧ (𝑀‘〈“𝐼𝐽”〉) Fn 𝐷 ∧ ran (𝑀‘〈“𝐼𝐽”〉) ⊆ 𝐷) → ((𝑀‘𝑊) ∘ (𝑀‘〈“𝐼𝐽”〉)) Fn 𝐷) |
40 | 13, 37, 38, 39 | syl3anc 1372 |
. 2
⊢ (𝜑 → ((𝑀‘𝑊) ∘ (𝑀‘〈“𝐼𝐽”〉)) Fn 𝐷) |
41 | | cycpmco2.1 |
. . . . . 6
⊢ 𝑈 = (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) |
42 | 15 | s1cld 14039 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐼”〉 ∈ Word 𝐷) |
43 | | splcl 14196 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) ∈ Word 𝐷) |
44 | 17, 42, 43 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) ∈ Word 𝐷) |
45 | 41, 44 | eqeltrid 2837 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ Word 𝐷) |
46 | | cycpmco2.e |
. . . . . 6
⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) |
47 | 2, 3, 1, 7, 14, 28, 46, 41 | cycpmco2f1 30960 |
. . . . 5
⊢ (𝜑 → 𝑈:dom 𝑈–1-1→𝐷) |
48 | 2, 1, 45, 47, 3 | cycpmcl 30952 |
. . . 4
⊢ (𝜑 → (𝑀‘𝑈) ∈ (Base‘𝑆)) |
49 | 3, 4 | symgbasf 18615 |
. . . 4
⊢ ((𝑀‘𝑈) ∈ (Base‘𝑆) → (𝑀‘𝑈):𝐷⟶𝐷) |
50 | 48, 49 | syl 17 |
. . 3
⊢ (𝜑 → (𝑀‘𝑈):𝐷⟶𝐷) |
51 | 50 | ffnd 6499 |
. 2
⊢ (𝜑 → (𝑀‘𝑈) Fn 𝐷) |
52 | | fvco3 6761 |
. . . 4
⊢ (((𝑀‘〈“𝐼𝐽”〉):𝐷⟶𝐷 ∧ 𝑖 ∈ 𝐷) → (((𝑀‘𝑊) ∘ (𝑀‘〈“𝐼𝐽”〉))‘𝑖) = ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖))) |
53 | 36, 52 | sylan 583 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐷) → (((𝑀‘𝑊) ∘ (𝑀‘〈“𝐼𝐽”〉))‘𝑖) = ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖))) |
54 | 2, 1, 15, 29, 33, 3 | cyc2fv2 30958 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀‘〈“𝐼𝐽”〉)‘𝐽) = 𝐼) |
55 | 54 | fveq2d 6672 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝐽)) = ((𝑀‘𝑊)‘𝐼)) |
56 | 2, 3, 1, 7, 14, 28, 46, 41 | cycpmco2lem2 30963 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑈‘𝐸) = 𝐼) |
57 | | f1cnv 6635 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊:dom 𝑊–1-1→𝐷 → ◡𝑊:ran 𝑊–1-1-onto→dom
𝑊) |
58 | | f1of 6612 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝑊:ran 𝑊–1-1-onto→dom
𝑊 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
59 | 24, 57, 58 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ◡𝑊:ran 𝑊⟶dom 𝑊) |
60 | 59, 28 | ffvelrnd 6856 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ dom 𝑊) |
61 | | wrddm 13955 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word 𝐷 → dom 𝑊 = (0..^(♯‘𝑊))) |
62 | 17, 61 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑊 = (0..^(♯‘𝑊))) |
63 | 60, 62 | eleqtrd 2835 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊))) |
64 | | lencl 13967 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑊 ∈ Word 𝐷 → (♯‘𝑊) ∈
ℕ0) |
65 | 17, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘𝑊) ∈
ℕ0) |
66 | 65 | nn0cnd 12031 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘𝑊) ∈
ℂ) |
67 | | 1cnd 10707 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℂ) |
68 | | ovexd 7199 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ V) |
69 | 46, 68 | eqeltrid 2837 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐸 ∈ V) |
70 | | splval 14195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ dom 𝑀 ∧ (𝐸 ∈ V ∧ 𝐸 ∈ V ∧ 〈“𝐼”〉 ∈ Word 𝐷)) → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
71 | 7, 69, 69, 42, 70 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑊 splice 〈𝐸, 𝐸, 〈“𝐼”〉〉) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
72 | 41, 71 | syl5eq 2785 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑈 = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) |
73 | 72 | fveq2d 6672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (♯‘𝑈) = (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) |
74 | | pfxcl 14121 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 prefix 𝐸) ∈ Word 𝐷) |
75 | 17, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑊 prefix 𝐸) ∈ Word 𝐷) |
76 | | ccatcl 14008 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷) → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
77 | 75, 42, 76 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷) |
78 | | swrdcl 14089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ Word 𝐷 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
79 | 17, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) |
80 | | ccatlen 14009 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷 ∧ (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷) → (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) |
81 | 77, 79, 80 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (♯‘(((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)))) |
82 | | ccatws1len 14056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 prefix 𝐸) ∈ Word 𝐷 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = ((♯‘(𝑊 prefix 𝐸)) + 1)) |
83 | 17, 74, 82 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = ((♯‘(𝑊 prefix 𝐸)) + 1)) |
84 | | fzofzp1 13218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
85 | 63, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((◡𝑊‘𝐽) + 1) ∈ (0...(♯‘𝑊))) |
86 | 46, 85 | eqeltrid 2837 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐸 ∈ (0...(♯‘𝑊))) |
87 | | pfxlen 14127 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐸)) = 𝐸) |
88 | 17, 86, 87 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (♯‘(𝑊 prefix 𝐸)) = 𝐸) |
89 | 88 | oveq1d 7179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((♯‘(𝑊 prefix 𝐸)) + 1) = (𝐸 + 1)) |
90 | 83, 89 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) = (𝐸 + 1)) |
91 | | nn0fz0 13089 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑊)
∈ ℕ0 ↔ (♯‘𝑊) ∈ (0...(♯‘𝑊))) |
92 | 65, 91 | sylib 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (♯‘𝑊) ∈
(0...(♯‘𝑊))) |
93 | | swrdlen 14091 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊)) ∧ (♯‘𝑊) ∈
(0...(♯‘𝑊)))
→ (♯‘(𝑊
substr 〈𝐸,
(♯‘𝑊)〉)) =
((♯‘𝑊) −
𝐸)) |
94 | 17, 86, 92, 93 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉)) = ((♯‘𝑊) − 𝐸)) |
95 | 90, 94 | oveq12d 7182 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)) + (♯‘(𝑊 substr 〈𝐸, (♯‘𝑊)〉))) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) |
96 | 73, 81, 95 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (♯‘𝑈) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) |
97 | | fz0ssnn0 13086 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(0...(♯‘𝑊)) ⊆
ℕ0 |
98 | 97, 86 | sseldi 3873 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐸 ∈
ℕ0) |
99 | 98 | nn0zd 12159 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐸 ∈ ℤ) |
100 | 99 | peano2zd 12164 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐸 + 1) ∈ ℤ) |
101 | 100 | zcnd 12162 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐸 + 1) ∈ ℂ) |
102 | 98 | nn0cnd 12031 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐸 ∈ ℂ) |
103 | 101, 66, 102 | addsubassd 11088 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + 1) + ((♯‘𝑊) − 𝐸))) |
104 | 102, 67, 66 | addassd 10734 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐸 + 1) + (♯‘𝑊)) = (𝐸 + (1 + (♯‘𝑊)))) |
105 | 104 | oveq1d 7179 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐸 + 1) + (♯‘𝑊)) − 𝐸) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸)) |
106 | 96, 103, 105 | 3eqtr2d 2779 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (♯‘𝑈) = ((𝐸 + (1 + (♯‘𝑊))) − 𝐸)) |
107 | 67, 66 | addcld 10731 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1 + (♯‘𝑊)) ∈
ℂ) |
108 | 102, 107 | pncan2d 11070 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐸 + (1 + (♯‘𝑊))) − 𝐸) = (1 + (♯‘𝑊))) |
109 | 67, 66 | addcomd 10913 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 + (♯‘𝑊)) = ((♯‘𝑊) + 1)) |
110 | 106, 108,
109 | 3eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘𝑈) = ((♯‘𝑊) + 1)) |
111 | 66, 67, 110 | mvrraddd 11123 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((♯‘𝑈) − 1) =
(♯‘𝑊)) |
112 | 111 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0..^((♯‘𝑈) − 1)) =
(0..^(♯‘𝑊))) |
113 | 63, 112 | eleqtrrd 2836 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^((♯‘𝑈) − 1))) |
114 | 2, 1, 45, 47, 113 | cycpmfv1 30949 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘(◡𝑊‘𝐽))) = (𝑈‘((◡𝑊‘𝐽) + 1))) |
115 | 46 | fveq2i 6671 |
. . . . . . . . . . 11
⊢ (𝑈‘𝐸) = (𝑈‘((◡𝑊‘𝐽) + 1)) |
116 | 114, 115 | eqtr4di 2791 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘(◡𝑊‘𝐽))) = (𝑈‘𝐸)) |
117 | 2, 1, 17, 24, 15, 30 | cycpmfv3 30951 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀‘𝑊)‘𝐼) = 𝐼) |
118 | 56, 116, 117 | 3eqtr4d 2783 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘(◡𝑊‘𝐽))) = ((𝑀‘𝑊)‘𝐼)) |
119 | 72 | fveq1d 6670 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑈‘(◡𝑊‘𝐽)) = ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘(◡𝑊‘𝐽))) |
120 | | fzossfzop1 13199 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 ∈ ℕ0
→ (0..^𝐸) ⊆
(0..^(𝐸 +
1))) |
121 | 98, 120 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0..^𝐸) ⊆ (0..^(𝐸 + 1))) |
122 | | elfzonn0 13166 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝑊‘𝐽) ∈ (0..^(♯‘𝑊)) → (◡𝑊‘𝐽) ∈
ℕ0) |
123 | | fzonn0p1 13198 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝑊‘𝐽) ∈ ℕ0 → (◡𝑊‘𝐽) ∈ (0..^((◡𝑊‘𝐽) + 1))) |
124 | 63, 122, 123 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^((◡𝑊‘𝐽) + 1))) |
125 | 46 | oveq2i 7175 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝐸) =
(0..^((◡𝑊‘𝐽) + 1)) |
126 | 124, 125 | eleqtrrdi 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^𝐸)) |
127 | 121, 126 | sseldd 3876 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(𝐸 + 1))) |
128 | 90 | oveq2d 7180 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(0..^(♯‘((𝑊
prefix 𝐸) ++
〈“𝐼”〉))) = (0..^(𝐸 + 1))) |
129 | 127, 128 | eleqtrrd 2836 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)))) |
130 | | ccatval1 14012 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ∈ Word 𝐷 ∧ (𝑊 substr 〈𝐸, (♯‘𝑊)〉) ∈ Word 𝐷 ∧ (◡𝑊‘𝐽) ∈ (0..^(♯‘((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)))) → ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘(◡𝑊‘𝐽)) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘(◡𝑊‘𝐽))) |
131 | 77, 79, 129, 130 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝑊 prefix 𝐸) ++ 〈“𝐼”〉) ++ (𝑊 substr 〈𝐸, (♯‘𝑊)〉))‘(◡𝑊‘𝐽)) = (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘(◡𝑊‘𝐽))) |
132 | 88 | oveq2d 7180 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0..^(♯‘(𝑊 prefix 𝐸))) = (0..^𝐸)) |
133 | 126, 132 | eleqtrrd 2836 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝑊‘𝐽) ∈ (0..^(♯‘(𝑊 prefix 𝐸)))) |
134 | | ccatval1 14012 |
. . . . . . . . . . . . 13
⊢ (((𝑊 prefix 𝐸) ∈ Word 𝐷 ∧ 〈“𝐼”〉 ∈ Word 𝐷 ∧ (◡𝑊‘𝐽) ∈ (0..^(♯‘(𝑊 prefix 𝐸)))) → (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘(◡𝑊‘𝐽)) = ((𝑊 prefix 𝐸)‘(◡𝑊‘𝐽))) |
135 | 75, 42, 133, 134 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑊 prefix 𝐸) ++ 〈“𝐼”〉)‘(◡𝑊‘𝐽)) = ((𝑊 prefix 𝐸)‘(◡𝑊‘𝐽))) |
136 | 119, 131,
135 | 3eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑈‘(◡𝑊‘𝐽)) = ((𝑊 prefix 𝐸)‘(◡𝑊‘𝐽))) |
137 | | pfxfv 14126 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ (0...(♯‘𝑊)) ∧ (◡𝑊‘𝐽) ∈ (0..^𝐸)) → ((𝑊 prefix 𝐸)‘(◡𝑊‘𝐽)) = (𝑊‘(◡𝑊‘𝐽))) |
138 | 17, 86, 126, 137 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑊 prefix 𝐸)‘(◡𝑊‘𝐽)) = (𝑊‘(◡𝑊‘𝐽))) |
139 | | f1f1orn 6623 |
. . . . . . . . . . . . 13
⊢ (𝑊:dom 𝑊–1-1→𝐷 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) |
140 | 24, 139 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊:dom 𝑊–1-1-onto→ran
𝑊) |
141 | | f1ocnvfv2 7039 |
. . . . . . . . . . . 12
⊢ ((𝑊:dom 𝑊–1-1-onto→ran
𝑊 ∧ 𝐽 ∈ ran 𝑊) → (𝑊‘(◡𝑊‘𝐽)) = 𝐽) |
142 | 140, 28, 141 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑊‘(◡𝑊‘𝐽)) = 𝐽) |
143 | 136, 138,
142 | 3eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑈‘(◡𝑊‘𝐽)) = 𝐽) |
144 | 143 | fveq2d 6672 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀‘𝑈)‘(𝑈‘(◡𝑊‘𝐽))) = ((𝑀‘𝑈)‘𝐽)) |
145 | 55, 118, 144 | 3eqtr2d 2779 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝐽)) = ((𝑀‘𝑈)‘𝐽)) |
146 | 145 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 = 𝐽) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝐽)) = ((𝑀‘𝑈)‘𝐽)) |
147 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 = 𝐽) → 𝑖 = 𝐽) |
148 | 147 | fveq2d 6672 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 = 𝐽) → ((𝑀‘〈“𝐼𝐽”〉)‘𝑖) = ((𝑀‘〈“𝐼𝐽”〉)‘𝐽)) |
149 | 148 | fveq2d 6672 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 = 𝐽) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝐽))) |
150 | 147 | fveq2d 6672 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 = 𝐽) → ((𝑀‘𝑈)‘𝑖) = ((𝑀‘𝑈)‘𝐽)) |
151 | 146, 149,
150 | 3eqtr4d 2783 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 = 𝐽) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑈)‘𝑖)) |
152 | 1 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → 𝐷 ∈ 𝑉) |
153 | 15, 29 | s2cld 14315 |
. . . . . . . . . 10
⊢ (𝜑 → 〈“𝐼𝐽”〉 ∈ Word 𝐷) |
154 | 153 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → 〈“𝐼𝐽”〉 ∈ Word 𝐷) |
155 | 15, 29, 33 | s2f1 30786 |
. . . . . . . . . 10
⊢ (𝜑 → 〈“𝐼𝐽”〉:dom 〈“𝐼𝐽”〉–1-1→𝐷) |
156 | 155 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → 〈“𝐼𝐽”〉:dom 〈“𝐼𝐽”〉–1-1→𝐷) |
157 | 27 | sselda 3875 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → 𝑖 ∈ 𝐷) |
158 | 157 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → 𝑖 ∈ 𝐷) |
159 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → 𝑖 ∈ ran 𝑊) |
160 | 30 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → ¬ 𝐼 ∈ ran 𝑊) |
161 | | nelne2 3031 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ran 𝑊 ∧ ¬ 𝐼 ∈ ran 𝑊) → 𝑖 ≠ 𝐼) |
162 | 159, 160,
161 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → 𝑖 ≠ 𝐼) |
163 | 162 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → 𝑖 ≠ 𝐼) |
164 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → 𝑖 ≠ 𝐽) |
165 | 163, 164 | nelprd 4544 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → ¬ 𝑖 ∈ {𝐼, 𝐽}) |
166 | 15, 29 | s2rn 30785 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 〈“𝐼𝐽”〉 = {𝐼, 𝐽}) |
167 | 166 | eleq2d 2818 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑖 ∈ ran 〈“𝐼𝐽”〉 ↔ 𝑖 ∈ {𝐼, 𝐽})) |
168 | 167 | notbid 321 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝑖 ∈ ran 〈“𝐼𝐽”〉 ↔ ¬ 𝑖 ∈ {𝐼, 𝐽})) |
169 | 168 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → (¬ 𝑖 ∈ ran 〈“𝐼𝐽”〉 ↔ ¬ 𝑖 ∈ {𝐼, 𝐽})) |
170 | 165, 169 | mpbird 260 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → ¬ 𝑖 ∈ ran 〈“𝐼𝐽”〉) |
171 | 2, 152, 154, 156, 158, 170 | cycpmfv3 30951 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → ((𝑀‘〈“𝐼𝐽”〉)‘𝑖) = 𝑖) |
172 | 171 | fveq2d 6672 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑊)‘𝑖)) |
173 | 1 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (0..^𝐸)) → 𝐷 ∈ 𝑉) |
174 | 7 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (0..^𝐸)) → 𝑊 ∈ dom 𝑀) |
175 | 14 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (0..^𝐸)) → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) |
176 | 28 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (0..^𝐸)) → 𝐽 ∈ ran 𝑊) |
177 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (0..^𝐸)) → 𝑖 ∈ ran 𝑊) |
178 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (0..^𝐸)) → 𝑖 ≠ 𝐽) |
179 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (0..^𝐸)) → (◡𝑈‘𝑖) ∈ (0..^𝐸)) |
180 | 2, 3, 173, 174, 175, 176, 46, 41, 177, 178, 179 | cycpmco2lem7 30968 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (0..^𝐸)) → ((𝑀‘𝑈)‘𝑖) = ((𝑀‘𝑊)‘𝑖)) |
181 | 1 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) → 𝐷 ∈ 𝑉) |
182 | 7 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) → 𝑊 ∈ dom 𝑀) |
183 | 14 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) |
184 | 28 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) → 𝐽 ∈ ran 𝑊) |
185 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) → 𝑖 ∈ ran 𝑊) |
186 | 162 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) → 𝑖 ≠ 𝐼) |
187 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) → (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) |
188 | 2, 3, 181, 182, 183, 184, 46, 41, 185, 186, 187 | cycpmco2lem6 30967 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) → ((𝑀‘𝑈)‘𝑖) = ((𝑀‘𝑊)‘𝑖)) |
189 | 1 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)) → 𝐷 ∈ 𝑉) |
190 | 7 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)) → 𝑊 ∈ dom 𝑀) |
191 | 14 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)) → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) |
192 | 28 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)) → 𝐽 ∈ ran 𝑊) |
193 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)) → 𝑖 ∈ ran 𝑊) |
194 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)) → (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)) |
195 | 2, 3, 189, 190, 191, 192, 46, 41, 193, 194 | cycpmco2lem5 30966 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) ∧ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)) → ((𝑀‘𝑈)‘𝑖) = ((𝑀‘𝑊)‘𝑖)) |
196 | | f1f1orn 6623 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈:dom 𝑈–1-1→𝐷 → 𝑈:dom 𝑈–1-1-onto→ran
𝑈) |
197 | 47, 196 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈:dom 𝑈–1-1-onto→ran
𝑈) |
198 | | ssun1 4060 |
. . . . . . . . . . . . . . . . 17
⊢ ran 𝑊 ⊆ (ran 𝑊 ∪ {𝐼}) |
199 | 2, 3, 1, 7, 14, 28, 46, 41 | cycpmco2rn 30961 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝑈 = (ran 𝑊 ∪ {𝐼})) |
200 | 198, 199 | sseqtrrid 3928 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran 𝑊 ⊆ ran 𝑈) |
201 | 200 | sselda 3875 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → 𝑖 ∈ ran 𝑈) |
202 | | f1ocnvdm 7046 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈:dom 𝑈–1-1-onto→ran
𝑈 ∧ 𝑖 ∈ ran 𝑈) → (◡𝑈‘𝑖) ∈ dom 𝑈) |
203 | 197, 201,
202 | syl2an2r 685 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → (◡𝑈‘𝑖) ∈ dom 𝑈) |
204 | | wrddm 13955 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ Word 𝐷 → dom 𝑈 = (0..^(♯‘𝑈))) |
205 | 45, 204 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝑈 = (0..^(♯‘𝑈))) |
206 | 205 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → dom 𝑈 = (0..^(♯‘𝑈))) |
207 | 203, 206 | eleqtrd 2835 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → (◡𝑈‘𝑖) ∈ (0..^(♯‘𝑈))) |
208 | 65 | nn0zd 12159 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (♯‘𝑊) ∈
ℤ) |
209 | 208 | peano2zd 12164 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((♯‘𝑊) + 1) ∈
ℤ) |
210 | 110, 209 | eqeltrd 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘𝑈) ∈
ℤ) |
211 | | fzoval 13123 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝑈)
∈ ℤ → (0..^(♯‘𝑈)) = (0...((♯‘𝑈) − 1))) |
212 | 210, 211 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0..^(♯‘𝑈)) = (0...((♯‘𝑈) − 1))) |
213 | 212 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → (0..^(♯‘𝑈)) = (0...((♯‘𝑈) − 1))) |
214 | 207, 213 | eleqtrd 2835 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → (◡𝑈‘𝑖) ∈ (0...((♯‘𝑈) − 1))) |
215 | | elfzr 13234 |
. . . . . . . . . . . 12
⊢ ((◡𝑈‘𝑖) ∈ (0...((♯‘𝑈) − 1)) → ((◡𝑈‘𝑖) ∈ (0..^((♯‘𝑈) − 1)) ∨ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1))) |
216 | 214, 215 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → ((◡𝑈‘𝑖) ∈ (0..^((♯‘𝑈) − 1)) ∨ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1))) |
217 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ (◡𝑈‘𝑖) ∈ (0..^((♯‘𝑈) − 1))) → (◡𝑈‘𝑖) ∈ (0..^((♯‘𝑈) − 1))) |
218 | 99 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ (◡𝑈‘𝑖) ∈ (0..^((♯‘𝑈) − 1))) → 𝐸 ∈
ℤ) |
219 | | fzospliti 13153 |
. . . . . . . . . . . . . 14
⊢ (((◡𝑈‘𝑖) ∈ (0..^((♯‘𝑈) − 1)) ∧ 𝐸 ∈ ℤ) → ((◡𝑈‘𝑖) ∈ (0..^𝐸) ∨ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1)))) |
220 | 217, 218,
219 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ (◡𝑈‘𝑖) ∈ (0..^((♯‘𝑈) − 1))) → ((◡𝑈‘𝑖) ∈ (0..^𝐸) ∨ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1)))) |
221 | 220 | ex 416 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → ((◡𝑈‘𝑖) ∈ (0..^((♯‘𝑈) − 1)) → ((◡𝑈‘𝑖) ∈ (0..^𝐸) ∨ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))))) |
222 | 221 | orim1d 965 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → (((◡𝑈‘𝑖) ∈ (0..^((♯‘𝑈) − 1)) ∨ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)) → (((◡𝑈‘𝑖) ∈ (0..^𝐸) ∨ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) ∨ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)))) |
223 | 216, 222 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → (((◡𝑈‘𝑖) ∈ (0..^𝐸) ∨ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) ∨ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1))) |
224 | | df-3or 1089 |
. . . . . . . . . 10
⊢ (((◡𝑈‘𝑖) ∈ (0..^𝐸) ∨ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1)) ∨ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1)) ↔ (((◡𝑈‘𝑖) ∈ (0..^𝐸) ∨ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1))) ∨ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1))) |
225 | 223, 224 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → ((◡𝑈‘𝑖) ∈ (0..^𝐸) ∨ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1)) ∨ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1))) |
226 | 225 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → ((◡𝑈‘𝑖) ∈ (0..^𝐸) ∨ (◡𝑈‘𝑖) ∈ (𝐸..^((♯‘𝑈) − 1)) ∨ (◡𝑈‘𝑖) = ((♯‘𝑈) − 1))) |
227 | 180, 188,
195, 226 | mpjao3dan 1432 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → ((𝑀‘𝑈)‘𝑖) = ((𝑀‘𝑊)‘𝑖)) |
228 | 172, 227 | eqtr4d 2776 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ran 𝑊) ∧ 𝑖 ≠ 𝐽) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑈)‘𝑖)) |
229 | 151, 228 | pm2.61dane 3021 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ran 𝑊) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑈)‘𝑖)) |
230 | 229 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 ∈ ran 𝑊) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑈)‘𝑖)) |
231 | 2, 3, 1, 7, 14, 28, 46, 41 | cycpmco2lem4 30965 |
. . . . . . . 8
⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝐼)) = ((𝑀‘𝑈)‘𝐼)) |
232 | 231 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 = 𝐼) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝐼)) = ((𝑀‘𝑈)‘𝐼)) |
233 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 = 𝐼) → 𝑖 = 𝐼) |
234 | 233 | fveq2d 6672 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 = 𝐼) → ((𝑀‘〈“𝐼𝐽”〉)‘𝑖) = ((𝑀‘〈“𝐼𝐽”〉)‘𝐼)) |
235 | 234 | fveq2d 6672 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 = 𝐼) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝐼))) |
236 | 233 | fveq2d 6672 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 = 𝐼) → ((𝑀‘𝑈)‘𝑖) = ((𝑀‘𝑈)‘𝐼)) |
237 | 232, 235,
236 | 3eqtr4d 2783 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 = 𝐼) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑈)‘𝑖)) |
238 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 𝐷 ∈ 𝑉) |
239 | 17 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 𝑊 ∈ Word 𝐷) |
240 | 24 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 𝑊:dom 𝑊–1-1→𝐷) |
241 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 𝑖 ∈ (𝐷 ∖ ran 𝑊)) |
242 | 241 | eldifad 3853 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 𝑖 ∈ 𝐷) |
243 | 241 | eldifbd 3854 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ¬ 𝑖 ∈ ran 𝑊) |
244 | 2, 238, 239, 240, 242, 243 | cycpmfv3 30951 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ((𝑀‘𝑊)‘𝑖) = 𝑖) |
245 | 153 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 〈“𝐼𝐽”〉 ∈ Word 𝐷) |
246 | 155 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 〈“𝐼𝐽”〉:dom 〈“𝐼𝐽”〉–1-1→𝐷) |
247 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 𝑖 ≠ 𝐼) |
248 | | eldifn 4016 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝐷 ∖ ran 𝑊) → ¬ 𝑖 ∈ ran 𝑊) |
249 | | nelne2 3031 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ ran 𝑊 ∧ ¬ 𝑖 ∈ ran 𝑊) → 𝐽 ≠ 𝑖) |
250 | 28, 248, 249 | syl2an 599 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) → 𝐽 ≠ 𝑖) |
251 | 250 | necomd 2989 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) → 𝑖 ≠ 𝐽) |
252 | 251 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 𝑖 ≠ 𝐽) |
253 | 247, 252 | nelprd 4544 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ¬ 𝑖 ∈ {𝐼, 𝐽}) |
254 | 168 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → (¬ 𝑖 ∈ ran 〈“𝐼𝐽”〉 ↔ ¬ 𝑖 ∈ {𝐼, 𝐽})) |
255 | 253, 254 | mpbird 260 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ¬ 𝑖 ∈ ran 〈“𝐼𝐽”〉) |
256 | 2, 238, 245, 246, 242, 255 | cycpmfv3 30951 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ((𝑀‘〈“𝐼𝐽”〉)‘𝑖) = 𝑖) |
257 | 256 | fveq2d 6672 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑊)‘𝑖)) |
258 | 45 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 𝑈 ∈ Word 𝐷) |
259 | 47 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → 𝑈:dom 𝑈–1-1→𝐷) |
260 | 199 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ran 𝑈 = (ran 𝑊 ∪ {𝐼})) |
261 | | nelsn 4553 |
. . . . . . . . . 10
⊢ (𝑖 ≠ 𝐼 → ¬ 𝑖 ∈ {𝐼}) |
262 | 261 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ¬ 𝑖 ∈ {𝐼}) |
263 | | nelun 30425 |
. . . . . . . . . 10
⊢ (ran
𝑈 = (ran 𝑊 ∪ {𝐼}) → (¬ 𝑖 ∈ ran 𝑈 ↔ (¬ 𝑖 ∈ ran 𝑊 ∧ ¬ 𝑖 ∈ {𝐼}))) |
264 | 263 | biimpar 481 |
. . . . . . . . 9
⊢ ((ran
𝑈 = (ran 𝑊 ∪ {𝐼}) ∧ (¬ 𝑖 ∈ ran 𝑊 ∧ ¬ 𝑖 ∈ {𝐼})) → ¬ 𝑖 ∈ ran 𝑈) |
265 | 260, 243,
262, 264 | syl12anc 836 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ¬ 𝑖 ∈ ran 𝑈) |
266 | 2, 238, 258, 259, 242, 265 | cycpmfv3 30951 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ((𝑀‘𝑈)‘𝑖) = 𝑖) |
267 | 244, 257,
266 | 3eqtr4d 2783 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) ∧ 𝑖 ≠ 𝐼) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑈)‘𝑖)) |
268 | 237, 267 | pm2.61dane 3021 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑈)‘𝑖)) |
269 | 268 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 ∈ (𝐷 ∖ ran 𝑊)) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑈)‘𝑖)) |
270 | | undif 4368 |
. . . . . . . 8
⊢ (ran
𝑊 ⊆ 𝐷 ↔ (ran 𝑊 ∪ (𝐷 ∖ ran 𝑊)) = 𝐷) |
271 | 27, 270 | sylib 221 |
. . . . . . 7
⊢ (𝜑 → (ran 𝑊 ∪ (𝐷 ∖ ran 𝑊)) = 𝐷) |
272 | 271 | eleq2d 2818 |
. . . . . 6
⊢ (𝜑 → (𝑖 ∈ (ran 𝑊 ∪ (𝐷 ∖ ran 𝑊)) ↔ 𝑖 ∈ 𝐷)) |
273 | | elun 4037 |
. . . . . 6
⊢ (𝑖 ∈ (ran 𝑊 ∪ (𝐷 ∖ ran 𝑊)) ↔ (𝑖 ∈ ran 𝑊 ∨ 𝑖 ∈ (𝐷 ∖ ran 𝑊))) |
274 | 272, 273 | bitr3di 289 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ 𝐷 ↔ (𝑖 ∈ ran 𝑊 ∨ 𝑖 ∈ (𝐷 ∖ ran 𝑊)))) |
275 | 274 | biimpa 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐷) → (𝑖 ∈ ran 𝑊 ∨ 𝑖 ∈ (𝐷 ∖ ran 𝑊))) |
276 | 230, 269,
275 | mpjaodan 958 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐷) → ((𝑀‘𝑊)‘((𝑀‘〈“𝐼𝐽”〉)‘𝑖)) = ((𝑀‘𝑈)‘𝑖)) |
277 | 53, 276 | eqtrd 2773 |
. 2
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐷) → (((𝑀‘𝑊) ∘ (𝑀‘〈“𝐼𝐽”〉))‘𝑖) = ((𝑀‘𝑈)‘𝑖)) |
278 | 40, 51, 277 | eqfnfvd 6806 |
1
⊢ (𝜑 → ((𝑀‘𝑊) ∘ (𝑀‘〈“𝐼𝐽”〉)) = (𝑀‘𝑈)) |