| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mulcl 11239 | . . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 · 𝑗) ∈ ℂ) | 
| 2 | 1 | adantl 481 | . . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 · 𝑗) ∈ ℂ) | 
| 3 |  | mulcom 11241 | . . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ) → (𝑚 · 𝑗) = (𝑗 · 𝑚)) | 
| 4 | 3 | adantl 481 | . . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ)) → (𝑚 · 𝑗) = (𝑗 · 𝑚)) | 
| 5 |  | mulass 11243 | . . . 4
⊢ ((𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑚 · 𝑗) · 𝑧) = (𝑚 · (𝑗 · 𝑧))) | 
| 6 | 5 | adantl 481 | . . 3
⊢ ((𝜑 ∧ (𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑚 · 𝑗) · 𝑧) = (𝑚 · (𝑗 · 𝑧))) | 
| 7 |  | prodmolem3.5 | . . . . 5
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) | 
| 8 | 7 | simpld 494 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 9 |  | nnuz 12921 | . . . 4
⊢ ℕ =
(ℤ≥‘1) | 
| 10 | 8, 9 | eleqtrdi 2851 | . . 3
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) | 
| 11 |  | ssidd 4007 | . . 3
⊢ (𝜑 → ℂ ⊆
ℂ) | 
| 12 |  | prodmolem3.6 | . . . . . 6
⊢ (𝜑 → 𝑓:(1...𝑀)–1-1-onto→𝐴) | 
| 13 |  | f1ocnv 6860 | . . . . . 6
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→(1...𝑀)) | 
| 14 | 12, 13 | syl 17 | . . . . 5
⊢ (𝜑 → ◡𝑓:𝐴–1-1-onto→(1...𝑀)) | 
| 15 |  | prodmolem3.7 | . . . . 5
⊢ (𝜑 → 𝐾:(1...𝑁)–1-1-onto→𝐴) | 
| 16 |  | f1oco 6871 | . . . . 5
⊢ ((◡𝑓:𝐴–1-1-onto→(1...𝑀) ∧ 𝐾:(1...𝑁)–1-1-onto→𝐴) → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) | 
| 17 | 14, 15, 16 | syl2anc 584 | . . . 4
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀)) | 
| 18 |  | ovex 7464 | . . . . . . . . . 10
⊢
(1...𝑁) ∈
V | 
| 19 | 18 | f1oen 9013 | . . . . . . . . 9
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀) → (1...𝑁) ≈ (1...𝑀)) | 
| 20 | 17, 19 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (1...𝑁) ≈ (1...𝑀)) | 
| 21 |  | fzfi 14013 | . . . . . . . . 9
⊢
(1...𝑁) ∈
Fin | 
| 22 |  | fzfi 14013 | . . . . . . . . 9
⊢
(1...𝑀) ∈
Fin | 
| 23 |  | hashen 14386 | . . . . . . . . 9
⊢
(((1...𝑁) ∈ Fin
∧ (1...𝑀) ∈ Fin)
→ ((♯‘(1...𝑁)) = (♯‘(1...𝑀)) ↔ (1...𝑁) ≈ (1...𝑀))) | 
| 24 | 21, 22, 23 | mp2an 692 | . . . . . . . 8
⊢
((♯‘(1...𝑁)) = (♯‘(1...𝑀)) ↔ (1...𝑁) ≈ (1...𝑀)) | 
| 25 | 20, 24 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑁)) = (♯‘(1...𝑀))) | 
| 26 | 7 | simprd 495 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 27 | 26 | nnnn0d 12587 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 28 |  | hashfz1 14385 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) | 
| 29 | 27, 28 | syl 17 | . . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁) | 
| 30 | 8 | nnnn0d 12587 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 31 |  | hashfz1 14385 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) | 
| 32 | 30, 31 | syl 17 | . . . . . . 7
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) | 
| 33 | 25, 29, 32 | 3eqtr3rd 2786 | . . . . . 6
⊢ (𝜑 → 𝑀 = 𝑁) | 
| 34 | 33 | oveq2d 7447 | . . . . 5
⊢ (𝜑 → (1...𝑀) = (1...𝑁)) | 
| 35 | 34 | f1oeq2d 6844 | . . . 4
⊢ (𝜑 → ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) ↔ (◡𝑓 ∘ 𝐾):(1...𝑁)–1-1-onto→(1...𝑀))) | 
| 36 | 17, 35 | mpbird 257 | . . 3
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀)) | 
| 37 |  | prodmo.3 | . . . . 5
⊢ 𝐺 = (𝑗 ∈ ℕ ↦ ⦋(𝑓‘𝑗) / 𝑘⦌𝐵) | 
| 38 |  | fveq2 6906 | . . . . . 6
⊢ (𝑗 = 𝑚 → (𝑓‘𝑗) = (𝑓‘𝑚)) | 
| 39 | 38 | csbeq1d 3903 | . . . . 5
⊢ (𝑗 = 𝑚 → ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) | 
| 40 |  | elfznn 13593 | . . . . . 6
⊢ (𝑚 ∈ (1...𝑀) → 𝑚 ∈ ℕ) | 
| 41 | 40 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → 𝑚 ∈ ℕ) | 
| 42 |  | f1of 6848 | . . . . . . . 8
⊢ (𝑓:(1...𝑀)–1-1-onto→𝐴 → 𝑓:(1...𝑀)⟶𝐴) | 
| 43 | 12, 42 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑓:(1...𝑀)⟶𝐴) | 
| 44 | 43 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝑓‘𝑚) ∈ 𝐴) | 
| 45 |  | prodmo.2 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 46 | 45 | ralrimiva 3146 | . . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) | 
| 47 | 46 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) | 
| 48 |  | nfcsb1v 3923 | . . . . . . . 8
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 | 
| 49 | 48 | nfel1 2922 | . . . . . . 7
⊢
Ⅎ𝑘⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ | 
| 50 |  | csbeq1a 3913 | . . . . . . . 8
⊢ (𝑘 = (𝑓‘𝑚) → 𝐵 = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) | 
| 51 | 50 | eleq1d 2826 | . . . . . . 7
⊢ (𝑘 = (𝑓‘𝑚) → (𝐵 ∈ ℂ ↔ ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) | 
| 52 | 49, 51 | rspc 3610 | . . . . . 6
⊢ ((𝑓‘𝑚) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ)) | 
| 53 | 44, 47, 52 | sylc 65 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → ⦋(𝑓‘𝑚) / 𝑘⦌𝐵 ∈ ℂ) | 
| 54 | 37, 39, 41, 53 | fvmptd3 7039 | . . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) = ⦋(𝑓‘𝑚) / 𝑘⦌𝐵) | 
| 55 | 54, 53 | eqeltrd 2841 | . . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝑀)) → (𝐺‘𝑚) ∈ ℂ) | 
| 56 | 34 | f1oeq2d 6844 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐾:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐾:(1...𝑁)–1-1-onto→𝐴)) | 
| 57 | 15, 56 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾:(1...𝑀)–1-1-onto→𝐴) | 
| 58 |  | f1of 6848 | . . . . . . . . . 10
⊢ (𝐾:(1...𝑀)–1-1-onto→𝐴 → 𝐾:(1...𝑀)⟶𝐴) | 
| 59 | 57, 58 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐾:(1...𝑀)⟶𝐴) | 
| 60 |  | fvco3 7008 | . . . . . . . . 9
⊢ ((𝐾:(1...𝑀)⟶𝐴 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) | 
| 61 | 59, 60 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) = (◡𝑓‘(𝐾‘𝑖))) | 
| 62 | 61 | fveq2d 6910 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝑓‘(◡𝑓‘(𝐾‘𝑖)))) | 
| 63 | 12 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑓:(1...𝑀)–1-1-onto→𝐴) | 
| 64 | 59 | ffvelcdmda 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝐴) | 
| 65 |  | f1ocnvfv2 7297 | . . . . . . . 8
⊢ ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (𝐾‘𝑖) ∈ 𝐴) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) | 
| 66 | 63, 64, 65 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘(◡𝑓‘(𝐾‘𝑖))) = (𝐾‘𝑖)) | 
| 67 | 62, 66 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) = (𝐾‘𝑖)) | 
| 68 | 67 | csbeq1d 3903 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) | 
| 69 | 68 | fveq2d 6910 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) | 
| 70 |  | f1of 6848 | . . . . . . 7
⊢ ((◡𝑓 ∘ 𝐾):(1...𝑀)–1-1-onto→(1...𝑀) → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) | 
| 71 | 36, 70 | syl 17 | . . . . . 6
⊢ (𝜑 → (◡𝑓 ∘ 𝐾):(1...𝑀)⟶(1...𝑀)) | 
| 72 | 71 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀)) | 
| 73 |  | elfznn 13593 | . . . . 5
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ (1...𝑀) → ((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ) | 
| 74 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑗 = ((◡𝑓 ∘ 𝐾)‘𝑖) → (𝑓‘𝑗) = (𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖))) | 
| 75 | 74 | csbeq1d 3903 | . . . . . 6
⊢ (𝑗 = ((◡𝑓 ∘ 𝐾)‘𝑖) → ⦋(𝑓‘𝑗) / 𝑘⦌𝐵 = ⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵) | 
| 76 | 75, 37 | fvmpti 7015 | . . . . 5
⊢ (((◡𝑓 ∘ 𝐾)‘𝑖) ∈ ℕ → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) | 
| 77 | 72, 73, 76 | 3syl 18 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖)) = ( I ‘⦋(𝑓‘((◡𝑓 ∘ 𝐾)‘𝑖)) / 𝑘⦌𝐵)) | 
| 78 |  | elfznn 13593 | . . . . . 6
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ) | 
| 79 | 78 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ ℕ) | 
| 80 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑗 = 𝑖 → (𝐾‘𝑗) = (𝐾‘𝑖)) | 
| 81 | 80 | csbeq1d 3903 | . . . . . 6
⊢ (𝑗 = 𝑖 → ⦋(𝐾‘𝑗) / 𝑘⦌𝐵 = ⦋(𝐾‘𝑖) / 𝑘⦌𝐵) | 
| 82 |  | prodmolem3.4 | . . . . . 6
⊢ 𝐻 = (𝑗 ∈ ℕ ↦ ⦋(𝐾‘𝑗) / 𝑘⦌𝐵) | 
| 83 | 81, 82 | fvmpti 7015 | . . . . 5
⊢ (𝑖 ∈ ℕ → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) | 
| 84 | 79, 83 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = ( I ‘⦋(𝐾‘𝑖) / 𝑘⦌𝐵)) | 
| 85 | 69, 77, 84 | 3eqtr4rd 2788 | . . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐻‘𝑖) = (𝐺‘((◡𝑓 ∘ 𝐾)‘𝑖))) | 
| 86 | 2, 4, 6, 10, 11, 36, 55, 85 | seqf1o 14084 | . 2
⊢ (𝜑 → (seq1( · , 𝐻)‘𝑀) = (seq1( · , 𝐺)‘𝑀)) | 
| 87 | 33 | fveq2d 6910 | . 2
⊢ (𝜑 → (seq1( · , 𝐻)‘𝑀) = (seq1( · , 𝐻)‘𝑁)) | 
| 88 | 86, 87 | eqtr3d 2779 | 1
⊢ (𝜑 → (seq1( · , 𝐺)‘𝑀) = (seq1( · , 𝐻)‘𝑁)) |