| Step | Hyp | Ref
| Expression |
| 1 | | 1arithidom.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ Word 𝑃) |
| 2 | | ccatws1len 14658 |
. . . . . 6
⊢ (𝐹 ∈ Word 𝑃 → (♯‘(𝐹 ++ 〈“𝑄”〉)) = ((♯‘𝐹) + 1)) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘(𝐹 ++ 〈“𝑄”〉)) =
((♯‘𝐹) +
1)) |
| 4 | | 1arithidomlem.15 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) = (𝐷 ∘f · (𝐹 ∘ 𝐶))) |
| 5 | 4 | dmeqd 5916 |
. . . . . . . . 9
⊢ (𝜑 → dom ((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) = dom (𝐷 ∘f · (𝐹 ∘ 𝐶))) |
| 6 | | 1arithidomlem.9 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) |
| 7 | | f1of 6848 |
. . . . . . . . . . . . 13
⊢ (𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) → 𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻))) |
| 8 | | iswrdi 14556 |
. . . . . . . . . . . . 13
⊢ (𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)) → 𝑆 ∈ Word (0..^(♯‘𝐻))) |
| 9 | 6, 7, 8 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Word (0..^(♯‘𝐻))) |
| 10 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐻) = (♯‘𝐻)) |
| 11 | | 1arithidomlem.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐻 ∈ Word 𝑃) |
| 12 | 10, 11 | wrdfd 32918 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻:(0..^(♯‘𝐻))⟶𝑃) |
| 13 | | wrdco 14870 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word
(0..^(♯‘𝐻))
∧ 𝐻:(0..^(♯‘𝐻))⟶𝑃) → (𝐻 ∘ 𝑆) ∈ Word 𝑃) |
| 14 | 9, 12, 13 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐻 ∘ 𝑆) ∈ Word 𝑃) |
| 15 | | 1arithidomlem.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ (0..^(♯‘𝐻))) |
| 16 | | elfzo0 13740 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈
(0..^(♯‘𝐻))
↔ (𝐾 ∈
ℕ0 ∧ (♯‘𝐻) ∈ ℕ ∧ 𝐾 < (♯‘𝐻))) |
| 17 | 16 | simp2bi 1147 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈
(0..^(♯‘𝐻))
→ (♯‘𝐻)
∈ ℕ) |
| 18 | | nnm1nn0 12567 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐻)
∈ ℕ → ((♯‘𝐻) − 1) ∈
ℕ0) |
| 19 | 15, 17, 18 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝐻) − 1) ∈
ℕ0) |
| 20 | | lenco 14871 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Word
(0..^(♯‘𝐻))
∧ 𝐻:(0..^(♯‘𝐻))⟶𝑃) → (♯‘(𝐻 ∘ 𝑆)) = (♯‘𝑆)) |
| 21 | 9, 12, 20 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝐻 ∘ 𝑆)) = (♯‘𝑆)) |
| 22 | | lencl 14571 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ Word
(0..^(♯‘𝐻))
→ (♯‘𝑆)
∈ ℕ0) |
| 23 | 9, 22 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝑆) ∈
ℕ0) |
| 24 | 21, 23 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝐻 ∘ 𝑆)) ∈
ℕ0) |
| 25 | | lencl 14571 |
. . . . . . . . . . . . . . . 16
⊢ (𝐻 ∈ Word 𝑃 → (♯‘𝐻) ∈
ℕ0) |
| 26 | 11, 25 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘𝐻) ∈
ℕ0) |
| 27 | 26 | nn0red 12588 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘𝐻) ∈
ℝ) |
| 28 | 27 | lem1d 12201 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((♯‘𝐻) − 1) ≤
(♯‘𝐻)) |
| 29 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻))) |
| 30 | | ffn 6736 |
. . . . . . . . . . . . . . 15
⊢ (𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻)) → 𝑆 Fn (0..^(♯‘𝐻))) |
| 31 | | hashfn 14414 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 Fn (0..^(♯‘𝐻)) → (♯‘𝑆) =
(♯‘(0..^(♯‘𝐻)))) |
| 32 | 29, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘𝑆) =
(♯‘(0..^(♯‘𝐻)))) |
| 33 | | hashfzo0 14469 |
. . . . . . . . . . . . . . 15
⊢
((♯‘𝐻)
∈ ℕ0 → (♯‘(0..^(♯‘𝐻))) = (♯‘𝐻)) |
| 34 | 11, 25, 33 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(♯‘(0..^(♯‘𝐻))) = (♯‘𝐻)) |
| 35 | 21, 32, 34 | 3eqtrrd 2782 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐻) = (♯‘(𝐻 ∘ 𝑆))) |
| 36 | 28, 35 | breqtrd 5169 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝐻) − 1) ≤
(♯‘(𝐻 ∘
𝑆))) |
| 37 | | elfz2nn0 13658 |
. . . . . . . . . . . 12
⊢
(((♯‘𝐻)
− 1) ∈ (0...(♯‘(𝐻 ∘ 𝑆))) ↔ (((♯‘𝐻) − 1) ∈
ℕ0 ∧ (♯‘(𝐻 ∘ 𝑆)) ∈ ℕ0 ∧
((♯‘𝐻) −
1) ≤ (♯‘(𝐻
∘ 𝑆)))) |
| 38 | 19, 24, 36, 37 | syl3anbrc 1344 |
. . . . . . . . . . 11
⊢ (𝜑 → ((♯‘𝐻) − 1) ∈
(0...(♯‘(𝐻
∘ 𝑆)))) |
| 39 | | pfxfn 14719 |
. . . . . . . . . . 11
⊢ (((𝐻 ∘ 𝑆) ∈ Word 𝑃 ∧ ((♯‘𝐻) − 1) ∈
(0...(♯‘(𝐻
∘ 𝑆)))) →
((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) Fn
(0..^((♯‘𝐻)
− 1))) |
| 40 | 14, 38, 39 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) Fn (0..^((♯‘𝐻) − 1))) |
| 41 | 40 | fndmd 6673 |
. . . . . . . . 9
⊢ (𝜑 → dom ((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) = (0..^((♯‘𝐻) − 1))) |
| 42 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 43 | | 1arithidom.t |
. . . . . . . . . . . 12
⊢ · =
(.r‘𝑅) |
| 44 | | 1arithidom.r |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ IDomn) |
| 45 | 44 | idomringd 20728 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃)) → 𝑅 ∈ Ring) |
| 47 | | 1arithidom.u |
. . . . . . . . . . . . . 14
⊢ 𝑈 = (Unit‘𝑅) |
| 48 | 42, 47 | unitcl 20375 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑈 → 𝑥 ∈ (Base‘𝑅)) |
| 49 | 48 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃)) → 𝑥 ∈ (Base‘𝑅)) |
| 50 | | 1arithidom.i |
. . . . . . . . . . . . 13
⊢ 𝑃 = (RPrime‘𝑅) |
| 51 | 44 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃)) → 𝑅 ∈ IDomn) |
| 52 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃)) → 𝑦 ∈ 𝑃) |
| 53 | 42, 50, 51, 52 | rprmcl 33546 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃)) → 𝑦 ∈ (Base‘𝑅)) |
| 54 | 42, 43, 46, 49, 53 | ringcld 20257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑃)) → (𝑥 · 𝑦) ∈ (Base‘𝑅)) |
| 55 | | 1arithidomlem.13 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈ (𝑈 ↑m
(0..^(♯‘𝐹)))) |
| 56 | | elmapi 8889 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ (𝑈 ↑m
(0..^(♯‘𝐹)))
→ 𝐷:(0..^(♯‘𝐹))⟶𝑈) |
| 57 | 55, 56 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷:(0..^(♯‘𝐹))⟶𝑈) |
| 58 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘𝐹) = (♯‘𝐹)) |
| 59 | 58, 1 | wrdfd 32918 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))⟶𝑃) |
| 60 | | 1arithidomlem.14 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹))) |
| 61 | | f1of 6848 |
. . . . . . . . . . . . 13
⊢ (𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) → 𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐹))) |
| 62 | 60, 61 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐹))) |
| 63 | 59, 62 | fcod 6761 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 ∘ 𝐶):(0..^(♯‘𝐹))⟶𝑃) |
| 64 | | ovexd 7466 |
. . . . . . . . . . 11
⊢ (𝜑 → (0..^(♯‘𝐹)) ∈ V) |
| 65 | | inidm 4227 |
. . . . . . . . . . 11
⊢
((0..^(♯‘𝐹)) ∩ (0..^(♯‘𝐹))) = (0..^(♯‘𝐹)) |
| 66 | 54, 57, 63, 64, 64, 65 | off 7715 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 ∘f · (𝐹 ∘ 𝐶)):(0..^(♯‘𝐹))⟶(Base‘𝑅)) |
| 67 | 66 | fdmd 6746 |
. . . . . . . . 9
⊢ (𝜑 → dom (𝐷 ∘f · (𝐹 ∘ 𝐶)) = (0..^(♯‘𝐹))) |
| 68 | 5, 41, 67 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (𝜑 → (0..^((♯‘𝐻) − 1)) =
(0..^(♯‘𝐹))) |
| 69 | | lencl 14571 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word 𝑃 → (♯‘𝐹) ∈
ℕ0) |
| 70 | 1, 69 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐹) ∈
ℕ0) |
| 71 | 19, 70 | fzo0opth 32807 |
. . . . . . . 8
⊢ (𝜑 →
((0..^((♯‘𝐻)
− 1)) = (0..^(♯‘𝐹)) ↔ ((♯‘𝐻) − 1) = (♯‘𝐹))) |
| 72 | 68, 71 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → ((♯‘𝐻) − 1) =
(♯‘𝐹)) |
| 73 | 72 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → (((♯‘𝐻) − 1) + 1) =
((♯‘𝐹) +
1)) |
| 74 | 15, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐻) ∈
ℕ) |
| 75 | 74 | nncnd 12282 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐻) ∈
ℂ) |
| 76 | | npcan1 11688 |
. . . . . . 7
⊢
((♯‘𝐻)
∈ ℂ → (((♯‘𝐻) − 1) + 1) = (♯‘𝐻)) |
| 77 | 75, 76 | syl 17 |
. . . . . 6
⊢ (𝜑 → (((♯‘𝐻) − 1) + 1) =
(♯‘𝐻)) |
| 78 | 73, 77 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → ((♯‘𝐹) + 1) = (♯‘𝐻)) |
| 79 | 3, 78 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (♯‘(𝐹 ++ 〈“𝑄”〉)) =
(♯‘𝐻)) |
| 80 | 79 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (0..^(♯‘(𝐹 ++ 〈“𝑄”〉))) =
(0..^(♯‘𝐻))) |
| 81 | | eqid 2737 |
. . . . . 6
⊢
(♯‘𝐶) =
(♯‘𝐶) |
| 82 | | eqid 2737 |
. . . . . 6
⊢
(0..^((♯‘𝐶) + 1)) = (0..^((♯‘𝐶) + 1)) |
| 83 | | f1ofn 6849 |
. . . . . . . . . 10
⊢ (𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)) → 𝐶 Fn (0..^(♯‘𝐹))) |
| 84 | | hashfn 14414 |
. . . . . . . . . 10
⊢ (𝐶 Fn (0..^(♯‘𝐹)) → (♯‘𝐶) =
(♯‘(0..^(♯‘𝐹)))) |
| 85 | 60, 83, 84 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐶) =
(♯‘(0..^(♯‘𝐹)))) |
| 86 | | hashfzo0 14469 |
. . . . . . . . . 10
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘(0..^(♯‘𝐹))) = (♯‘𝐹)) |
| 87 | 70, 86 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(♯‘(0..^(♯‘𝐹))) = (♯‘𝐹)) |
| 88 | 85, 87 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐶) = (♯‘𝐹)) |
| 89 | 88 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (0..^(♯‘𝐶)) = (0..^(♯‘𝐹))) |
| 90 | | f1oeq23 6839 |
. . . . . . . 8
⊢
(((0..^(♯‘𝐶)) = (0..^(♯‘𝐹)) ∧ (0..^(♯‘𝐶)) = (0..^(♯‘𝐹))) → (𝐶:(0..^(♯‘𝐶))–1-1-onto→(0..^(♯‘𝐶)) ↔ 𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹)))) |
| 91 | 90 | biimpar 477 |
. . . . . . 7
⊢
((((0..^(♯‘𝐶)) = (0..^(♯‘𝐹)) ∧ (0..^(♯‘𝐶)) = (0..^(♯‘𝐹))) ∧ 𝐶:(0..^(♯‘𝐹))–1-1-onto→(0..^(♯‘𝐹))) → 𝐶:(0..^(♯‘𝐶))–1-1-onto→(0..^(♯‘𝐶))) |
| 92 | 89, 89, 60, 91 | syl21anc 838 |
. . . . . 6
⊢ (𝜑 → 𝐶:(0..^(♯‘𝐶))–1-1-onto→(0..^(♯‘𝐶))) |
| 93 | 81, 82, 92 | ccatws1f1o 32936 |
. . . . 5
⊢ (𝜑 → (𝐶 ++ 〈“(♯‘𝐶)”〉):(0..^((♯‘𝐶) + 1))–1-1-onto→(0..^((♯‘𝐶) + 1))) |
| 94 | 88 | s1eqd 14639 |
. . . . . . 7
⊢ (𝜑 →
〈“(♯‘𝐶)”〉 =
〈“(♯‘𝐹)”〉) |
| 95 | 94 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (𝐶 ++ 〈“(♯‘𝐶)”〉) = (𝐶 ++
〈“(♯‘𝐹)”〉)) |
| 96 | 88 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘𝐶) + 1) = ((♯‘𝐹) + 1)) |
| 97 | 96, 78 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → ((♯‘𝐶) + 1) = (♯‘𝐻)) |
| 98 | 97 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (0..^((♯‘𝐶) + 1)) =
(0..^(♯‘𝐻))) |
| 99 | 95, 98, 98 | f1oeq123d 6842 |
. . . . 5
⊢ (𝜑 → ((𝐶 ++ 〈“(♯‘𝐶)”〉):(0..^((♯‘𝐶) + 1))–1-1-onto→(0..^((♯‘𝐶) + 1)) ↔ (𝐶 ++ 〈“(♯‘𝐹)”〉):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))) |
| 100 | 93, 99 | mpbid 232 |
. . . 4
⊢ (𝜑 → (𝐶 ++ 〈“(♯‘𝐹)”〉):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) |
| 101 | | f1ocnv 6860 |
. . . . 5
⊢ (𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) → ◡𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) |
| 102 | 6, 101 | syl 17 |
. . . 4
⊢ (𝜑 → ◡𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) |
| 103 | | f1oco 6871 |
. . . 4
⊢ (((𝐶 ++
〈“(♯‘𝐹)”〉):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) ∧ ◡𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) → ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) |
| 104 | 100, 102,
103 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) |
| 105 | | f1oeq23 6839 |
. . . 4
⊢
(((0..^(♯‘(𝐹 ++ 〈“𝑄”〉))) = (0..^(♯‘𝐻)) ∧
(0..^(♯‘(𝐹 ++
〈“𝑄”〉))) = (0..^(♯‘𝐻))) → (((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆):(0..^(♯‘(𝐹 ++ 〈“𝑄”〉)))–1-1-onto→(0..^(♯‘(𝐹 ++ 〈“𝑄”〉))) ↔ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)))) |
| 106 | 105 | biimpar 477 |
. . 3
⊢
((((0..^(♯‘(𝐹 ++ 〈“𝑄”〉))) = (0..^(♯‘𝐻)) ∧
(0..^(♯‘(𝐹 ++
〈“𝑄”〉))) = (0..^(♯‘𝐻))) ∧ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆):(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻))) → ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆):(0..^(♯‘(𝐹 ++ 〈“𝑄”〉)))–1-1-onto→(0..^(♯‘(𝐹 ++ 〈“𝑄”〉)))) |
| 107 | 80, 80, 104, 106 | syl21anc 838 |
. 2
⊢ (𝜑 → ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆):(0..^(♯‘(𝐹 ++ 〈“𝑄”〉)))–1-1-onto→(0..^(♯‘(𝐹 ++ 〈“𝑄”〉)))) |
| 108 | | f1ofo 6855 |
. . . 4
⊢ (𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) → 𝑆:(0..^(♯‘𝐻))–onto→(0..^(♯‘𝐻))) |
| 109 | 6, 108 | syl 17 |
. . 3
⊢ (𝜑 → 𝑆:(0..^(♯‘𝐻))–onto→(0..^(♯‘𝐻))) |
| 110 | 12 | ffnd 6737 |
. . 3
⊢ (𝜑 → 𝐻 Fn (0..^(♯‘𝐻))) |
| 111 | | iswrdi 14556 |
. . . . . . . . . . 11
⊢ (𝐷:(0..^(♯‘𝐹))⟶𝑈 → 𝐷 ∈ Word 𝑈) |
| 112 | 57, 111 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ Word 𝑈) |
| 113 | | ccatws1len 14658 |
. . . . . . . . . 10
⊢ (𝐷 ∈ Word 𝑈 → (♯‘(𝐷 ++ 〈“𝑇”〉)) = ((♯‘𝐷) + 1)) |
| 114 | 112, 113 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(𝐷 ++ 〈“𝑇”〉)) =
((♯‘𝐷) +
1)) |
| 115 | | elmapfn 8905 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ (𝑈 ↑m
(0..^(♯‘𝐹)))
→ 𝐷 Fn
(0..^(♯‘𝐹))) |
| 116 | | hashfn 14414 |
. . . . . . . . . . . 12
⊢ (𝐷 Fn (0..^(♯‘𝐹)) → (♯‘𝐷) =
(♯‘(0..^(♯‘𝐹)))) |
| 117 | 55, 115, 116 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐷) =
(♯‘(0..^(♯‘𝐹)))) |
| 118 | 117, 87 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐷) = (♯‘𝐹)) |
| 119 | 118 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘𝐷) + 1) = ((♯‘𝐹) + 1)) |
| 120 | 114, 119,
78 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(𝐷 ++ 〈“𝑇”〉)) =
(♯‘𝐻)) |
| 121 | 120 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (0..^(♯‘(𝐷 ++ 〈“𝑇”〉))) =
(0..^(♯‘𝐻))) |
| 122 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(𝐷 ++ 〈“𝑇”〉)) =
(♯‘(𝐷 ++
〈“𝑇”〉))) |
| 123 | | 1arithidomlem.7 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ 𝑈) |
| 124 | | ccatws1cl 14654 |
. . . . . . . . 9
⊢ ((𝐷 ∈ Word 𝑈 ∧ 𝑇 ∈ 𝑈) → (𝐷 ++ 〈“𝑇”〉) ∈ Word 𝑈) |
| 125 | 112, 123,
124 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 ++ 〈“𝑇”〉) ∈ Word 𝑈) |
| 126 | 122, 125 | wrdfd 32918 |
. . . . . . 7
⊢ (𝜑 → (𝐷 ++ 〈“𝑇”〉):(0..^(♯‘(𝐷 ++ 〈“𝑇”〉)))⟶𝑈) |
| 127 | 121, 126 | feq2dd 32632 |
. . . . . 6
⊢ (𝜑 → (𝐷 ++ 〈“𝑇”〉):(0..^(♯‘𝐻))⟶𝑈) |
| 128 | 127 | ffnd 6737 |
. . . . 5
⊢ (𝜑 → (𝐷 ++ 〈“𝑇”〉) Fn (0..^(♯‘𝐻))) |
| 129 | | f1of 6848 |
. . . . . 6
⊢ (◡𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) → ◡𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻))) |
| 130 | 6, 101, 129 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ◡𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻))) |
| 131 | | fnfco 6773 |
. . . . 5
⊢ (((𝐷 ++ 〈“𝑇”〉) Fn
(0..^(♯‘𝐻))
∧ ◡𝑆:(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻))) → ((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) Fn (0..^(♯‘𝐻))) |
| 132 | 128, 130,
131 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) Fn (0..^(♯‘𝐻))) |
| 133 | 78 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → (0..^((♯‘𝐹) + 1)) =
(0..^(♯‘𝐻))) |
| 134 | 3 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘𝐹) + 1) = (♯‘(𝐹 ++ 〈“𝑄”〉))) |
| 135 | | 1arithidomlem.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ 𝑃) |
| 136 | | ccatws1cl 14654 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word 𝑃 ∧ 𝑄 ∈ 𝑃) → (𝐹 ++ 〈“𝑄”〉) ∈ Word 𝑃) |
| 137 | 1, 135, 136 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ++ 〈“𝑄”〉) ∈ Word 𝑃) |
| 138 | 134, 137 | wrdfd 32918 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ++ 〈“𝑄”〉):(0..^((♯‘𝐹) + 1))⟶𝑃) |
| 139 | 133, 138 | feq2dd 32632 |
. . . . . 6
⊢ (𝜑 → (𝐹 ++ 〈“𝑄”〉):(0..^(♯‘𝐻))⟶𝑃) |
| 140 | 139 | ffnd 6737 |
. . . . 5
⊢ (𝜑 → (𝐹 ++ 〈“𝑄”〉) Fn (0..^(♯‘𝐻))) |
| 141 | | fzossfzop1 13782 |
. . . . . . . . . . . 12
⊢
((♯‘𝐹)
∈ ℕ0 → (0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1))) |
| 142 | 70, 141 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (0..^(♯‘𝐹)) ⊆
(0..^((♯‘𝐹) +
1))) |
| 143 | | sswrd 14560 |
. . . . . . . . . . 11
⊢
((0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1)) → Word
(0..^(♯‘𝐹))
⊆ Word (0..^((♯‘𝐹) + 1))) |
| 144 | 142, 143 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Word
(0..^(♯‘𝐹))
⊆ Word (0..^((♯‘𝐹) + 1))) |
| 145 | | iswrdi 14556 |
. . . . . . . . . . 11
⊢ (𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐹)) → 𝐶 ∈ Word (0..^(♯‘𝐹))) |
| 146 | 62, 145 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ Word (0..^(♯‘𝐹))) |
| 147 | 144, 146 | sseldd 3984 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ Word (0..^((♯‘𝐹) + 1))) |
| 148 | | ccatws1len 14658 |
. . . . . . . . 9
⊢ (𝐶 ∈ Word
(0..^((♯‘𝐹) +
1)) → (♯‘(𝐶 ++ 〈“(♯‘𝐹)”〉)) =
((♯‘𝐶) +
1)) |
| 149 | 147, 148 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(𝐶 ++
〈“(♯‘𝐹)”〉)) = ((♯‘𝐶) + 1)) |
| 150 | 149, 96, 78 | 3eqtrrd 2782 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐻) = (♯‘(𝐶 ++
〈“(♯‘𝐹)”〉))) |
| 151 | 142, 133 | sseqtrd 4020 |
. . . . . . . . . 10
⊢ (𝜑 → (0..^(♯‘𝐹)) ⊆
(0..^(♯‘𝐻))) |
| 152 | 62, 151 | fssd 6753 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐻))) |
| 153 | | iswrdi 14556 |
. . . . . . . . 9
⊢ (𝐶:(0..^(♯‘𝐹))⟶(0..^(♯‘𝐻)) → 𝐶 ∈ Word (0..^(♯‘𝐻))) |
| 154 | 152, 153 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ Word (0..^(♯‘𝐻))) |
| 155 | | fzonn0p1 13781 |
. . . . . . . . . 10
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ (0..^((♯‘𝐹) + 1))) |
| 156 | 70, 155 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1))) |
| 157 | 156, 133 | eleqtrd 2843 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐹) ∈
(0..^(♯‘𝐻))) |
| 158 | | ccatws1cl 14654 |
. . . . . . . 8
⊢ ((𝐶 ∈ Word
(0..^(♯‘𝐻))
∧ (♯‘𝐹)
∈ (0..^(♯‘𝐻))) → (𝐶 ++ 〈“(♯‘𝐹)”〉) ∈ Word
(0..^(♯‘𝐻))) |
| 159 | 154, 157,
158 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ++ 〈“(♯‘𝐹)”〉) ∈ Word
(0..^(♯‘𝐻))) |
| 160 | 150, 159 | wrdfd 32918 |
. . . . . 6
⊢ (𝜑 → (𝐶 ++ 〈“(♯‘𝐹)”〉):(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻))) |
| 161 | 160, 130 | fcod 6761 |
. . . . 5
⊢ (𝜑 → ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆):(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻))) |
| 162 | | fnfco 6773 |
. . . . 5
⊢ (((𝐹 ++ 〈“𝑄”〉) Fn
(0..^(♯‘𝐻))
∧ ((𝐶 ++
〈“(♯‘𝐹)”〉) ∘ ◡𝑆):(0..^(♯‘𝐻))⟶(0..^(♯‘𝐻))) → ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆)) Fn (0..^(♯‘𝐻))) |
| 163 | 140, 161,
162 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆)) Fn (0..^(♯‘𝐻))) |
| 164 | | ovexd 7466 |
. . . 4
⊢ (𝜑 → (0..^(♯‘𝐻)) ∈ V) |
| 165 | | inidm 4227 |
. . . 4
⊢
((0..^(♯‘𝐻)) ∩ (0..^(♯‘𝐻))) = (0..^(♯‘𝐻)) |
| 166 | 132, 163,
164, 164, 165 | offn 7710 |
. . 3
⊢ (𝜑 → (((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))) Fn (0..^(♯‘𝐻))) |
| 167 | | 1arithidomlem.10 |
. . . 4
⊢ (𝜑 → (𝐻 ∘ 𝑆) = (((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) ++ 〈“(𝐻‘𝐾)”〉)) |
| 168 | | eqid 2737 |
. . . . . . . . 9
⊢
(♯‘𝐹) =
(♯‘𝐹) |
| 169 | 168, 1, 135, 60 | ccatws1f1olast 32937 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++ 〈“(♯‘𝐹)”〉)) = ((𝐹 ∘ 𝐶) ++ 〈“𝑄”〉)) |
| 170 | 169 | oveq2d 7447 |
. . . . . . 7
⊢ (𝜑 → ((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))) = ((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ∘ 𝐶) ++ 〈“𝑄”〉))) |
| 171 | 123 | s1cld 14641 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝑇”〉 ∈ Word 𝑈) |
| 172 | | iswrdi 14556 |
. . . . . . . . 9
⊢ ((𝐹 ∘ 𝐶):(0..^(♯‘𝐹))⟶𝑃 → (𝐹 ∘ 𝐶) ∈ Word 𝑃) |
| 173 | 63, 172 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∘ 𝐶) ∈ Word 𝑃) |
| 174 | 135 | s1cld 14641 |
. . . . . . . 8
⊢ (𝜑 → 〈“𝑄”〉 ∈ Word 𝑃) |
| 175 | | lenco 14871 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Word
(0..^(♯‘𝐹))
∧ 𝐹:(0..^(♯‘𝐹))⟶𝑃) → (♯‘(𝐹 ∘ 𝐶)) = (♯‘𝐶)) |
| 176 | 146, 59, 175 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(𝐹 ∘ 𝐶)) = (♯‘𝐶)) |
| 177 | 85, 176, 117 | 3eqtr4rd 2788 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝐷) = (♯‘(𝐹 ∘ 𝐶))) |
| 178 | | s1len 14644 |
. . . . . . . . . 10
⊢
(♯‘〈“𝑇”〉) = 1 |
| 179 | | s1len 14644 |
. . . . . . . . . 10
⊢
(♯‘〈“𝑄”〉) = 1 |
| 180 | 178, 179 | eqtr4i 2768 |
. . . . . . . . 9
⊢
(♯‘〈“𝑇”〉) =
(♯‘〈“𝑄”〉) |
| 181 | 180 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 →
(♯‘〈“𝑇”〉) =
(♯‘〈“𝑄”〉)) |
| 182 | 112, 171,
173, 174, 177, 181 | ofccat 15008 |
. . . . . . 7
⊢ (𝜑 → ((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ∘ 𝐶) ++ 〈“𝑄”〉)) = ((𝐷 ∘f · (𝐹 ∘ 𝐶)) ++ (〈“𝑇”〉 ∘f ·
〈“𝑄”〉))) |
| 183 | 170, 182 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → ((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))) = ((𝐷 ∘f · (𝐹 ∘ 𝐶)) ++ (〈“𝑇”〉 ∘f ·
〈“𝑄”〉))) |
| 184 | 139, 160 | fcod 6761 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++ 〈“(♯‘𝐹)”〉)):(0..^(♯‘𝐻))⟶𝑃) |
| 185 | 184 | ffnd 6737 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++ 〈“(♯‘𝐹)”〉)) Fn
(0..^(♯‘𝐻))) |
| 186 | 128, 185,
130, 164, 164, 164, 165 | ofco 7722 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))) ∘ ◡𝑆) = (((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · (((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉)) ∘ ◡𝑆))) |
| 187 | 186 | coeq1d 5872 |
. . . . . . . 8
⊢ (𝜑 → ((((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))) ∘ ◡𝑆) ∘ 𝑆) = ((((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · (((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉)) ∘ ◡𝑆)) ∘ 𝑆)) |
| 188 | | coass 6285 |
. . . . . . . 8
⊢ ((((𝐷 ++ 〈“𝑇”〉)
∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++ 〈“(♯‘𝐹)”〉))) ∘ ◡𝑆) ∘ 𝑆) = (((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))) ∘ (◡𝑆 ∘ 𝑆)) |
| 189 | 187, 188 | eqtr3di 2792 |
. . . . . . 7
⊢ (𝜑 → ((((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · (((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉)) ∘ ◡𝑆)) ∘ 𝑆) = (((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))) ∘ (◡𝑆 ∘ 𝑆))) |
| 190 | | f1of1 6847 |
. . . . . . . . . 10
⊢ (𝑆:(0..^(♯‘𝐻))–1-1-onto→(0..^(♯‘𝐻)) → 𝑆:(0..^(♯‘𝐻))–1-1→(0..^(♯‘𝐻))) |
| 191 | 6, 190 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆:(0..^(♯‘𝐻))–1-1→(0..^(♯‘𝐻))) |
| 192 | | f1cocnv1 6878 |
. . . . . . . . 9
⊢ (𝑆:(0..^(♯‘𝐻))–1-1→(0..^(♯‘𝐻)) → (◡𝑆 ∘ 𝑆) = ( I ↾ (0..^(♯‘𝐻)))) |
| 193 | 191, 192 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (◡𝑆 ∘ 𝑆) = ( I ↾ (0..^(♯‘𝐻)))) |
| 194 | 193 | coeq2d 5873 |
. . . . . . 7
⊢ (𝜑 → (((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))) ∘ (◡𝑆 ∘ 𝑆)) = (((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))) ∘ ( I ↾
(0..^(♯‘𝐻))))) |
| 195 | 54, 127, 184, 164, 164, 165 | off 7715 |
. . . . . . . 8
⊢ (𝜑 → ((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))):(0..^(♯‘𝐻))⟶(Base‘𝑅)) |
| 196 | | fcoi1 6782 |
. . . . . . . 8
⊢ (((𝐷 ++ 〈“𝑇”〉)
∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++ 〈“(♯‘𝐹)”〉))):(0..^(♯‘𝐻))⟶(Base‘𝑅) → (((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))) ∘ ( I ↾
(0..^(♯‘𝐻)))) =
((𝐷 ++ 〈“𝑇”〉)
∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++ 〈“(♯‘𝐹)”〉)))) |
| 197 | 195, 196 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉))) ∘ ( I ↾
(0..^(♯‘𝐻)))) =
((𝐷 ++ 〈“𝑇”〉)
∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++ 〈“(♯‘𝐹)”〉)))) |
| 198 | 189, 194,
197 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → ((((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · (((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉)) ∘ ◡𝑆)) ∘ 𝑆) = ((𝐷 ++ 〈“𝑇”〉) ∘f ·
((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉)))) |
| 199 | | ofs1 15009 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝑈 ∧ 𝑄 ∈ 𝑃) → (〈“𝑇”〉 ∘f ·
〈“𝑄”〉) = 〈“(𝑇 · 𝑄)”〉) |
| 200 | 123, 135,
199 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (〈“𝑇”〉
∘f · 〈“𝑄”〉) =
〈“(𝑇 · 𝑄)”〉) |
| 201 | | 1arithidomlem.8 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 · 𝑄) = (𝐻‘𝐾)) |
| 202 | 201 | s1eqd 14639 |
. . . . . . . 8
⊢ (𝜑 → 〈“(𝑇 · 𝑄)”〉 = 〈“(𝐻‘𝐾)”〉) |
| 203 | 200, 202 | eqtr2d 2778 |
. . . . . . 7
⊢ (𝜑 → 〈“(𝐻‘𝐾)”〉 = (〈“𝑇”〉
∘f · 〈“𝑄”〉)) |
| 204 | 4, 203 | oveq12d 7449 |
. . . . . 6
⊢ (𝜑 → (((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) ++ 〈“(𝐻‘𝐾)”〉) = ((𝐷 ∘f · (𝐹 ∘ 𝐶)) ++ (〈“𝑇”〉 ∘f ·
〈“𝑄”〉))) |
| 205 | 183, 198,
204 | 3eqtr4rd 2788 |
. . . . 5
⊢ (𝜑 → (((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) ++ 〈“(𝐻‘𝐾)”〉) = ((((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · (((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉)) ∘ ◡𝑆)) ∘ 𝑆)) |
| 206 | | coass 6285 |
. . . . . . 7
⊢ (((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉)) ∘ ◡𝑆) = ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆)) |
| 207 | 206 | oveq2i 7442 |
. . . . . 6
⊢ (((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · (((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉)) ∘ ◡𝑆)) = (((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))) |
| 208 | 207 | coeq1i 5870 |
. . . . 5
⊢ ((((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · (((𝐹 ++ 〈“𝑄”〉) ∘ (𝐶 ++
〈“(♯‘𝐹)”〉)) ∘ ◡𝑆)) ∘ 𝑆) = ((((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))) ∘ 𝑆) |
| 209 | 205, 208 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → (((𝐻 ∘ 𝑆) prefix ((♯‘𝐻) − 1)) ++ 〈“(𝐻‘𝐾)”〉) = ((((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))) ∘ 𝑆)) |
| 210 | 167, 209 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (𝐻 ∘ 𝑆) = ((((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))) ∘ 𝑆)) |
| 211 | | cocan2 7312 |
. . . 4
⊢ ((𝑆:(0..^(♯‘𝐻))–onto→(0..^(♯‘𝐻)) ∧ 𝐻 Fn (0..^(♯‘𝐻)) ∧ (((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))) Fn (0..^(♯‘𝐻))) → ((𝐻 ∘ 𝑆) = ((((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))) ∘ 𝑆) ↔ 𝐻 = (((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))))) |
| 212 | 211 | biimpa 476 |
. . 3
⊢ (((𝑆:(0..^(♯‘𝐻))–onto→(0..^(♯‘𝐻)) ∧ 𝐻 Fn (0..^(♯‘𝐻)) ∧ (((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))) Fn (0..^(♯‘𝐻))) ∧ (𝐻 ∘ 𝑆) = ((((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))) ∘ 𝑆)) → 𝐻 = (((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆)))) |
| 213 | 109, 110,
166, 210, 212 | syl31anc 1375 |
. 2
⊢ (𝜑 → 𝐻 = (((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆)))) |
| 214 | 107, 213 | jca 511 |
1
⊢ (𝜑 → (((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆):(0..^(♯‘(𝐹 ++ 〈“𝑄”〉)))–1-1-onto→(0..^(♯‘(𝐹 ++ 〈“𝑄”〉))) ∧ 𝐻 = (((𝐷 ++ 〈“𝑇”〉) ∘ ◡𝑆) ∘f · ((𝐹 ++ 〈“𝑄”〉) ∘ ((𝐶 ++ 〈“(♯‘𝐹)”〉) ∘ ◡𝑆))))) |