Theorem prodmolem3

Description: Lemma for prodmo . (Contributed by Scott Fenton, 4-Dec-2017)

	Ref	Expression
Hypotheses	prodmo.1	⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
	prodmo.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	prodmo.3	⊢ 𝐺 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
	prodmolem3.4	⊢ 𝐻 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝐾 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
	prodmolem3.5	⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
	prodmolem3.6	⊢ ( 𝜑 → 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 )
	prodmolem3.7	⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 )
Assertion	prodmolem3	⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐻 ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		prodmo.1	⊢ 𝐹 = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
2		prodmo.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3		prodmo.3	⊢ 𝐺 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
4		prodmolem3.4	⊢ 𝐻 = ( 𝑗 ∈ ℕ ↦ ⦋ ( 𝐾 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 )
5		prodmolem3.5	⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) )
6		prodmolem3.6	⊢ ( 𝜑 → 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 )
7		prodmolem3.7	⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 )
8		mulcl	⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑚 · 𝑗 ) ∈ ℂ )
9	8	adantl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) ) → ( 𝑚 · 𝑗 ) ∈ ℂ )
10		mulcom	⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑚 · 𝑗 ) = ( 𝑗 · 𝑚 ) )
11	10	adantl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ) ) → ( 𝑚 · 𝑗 ) = ( 𝑗 · 𝑚 ) )
12		mulass	⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑚 · 𝑗 ) · 𝑧 ) = ( 𝑚 · ( 𝑗 · 𝑧 ) ) )
13	12	adantl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℂ ∧ 𝑗 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑚 · 𝑗 ) · 𝑧 ) = ( 𝑚 · ( 𝑗 · 𝑧 ) ) )
14	5	simpld	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
15		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
16	14 15	eleqtrdi	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
17		ssidd	⊢ ( 𝜑 → ℂ ⊆ ℂ )
18		f1ocnv	⊢ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐴 –1-1-onto→ ( 1 ... 𝑀 ) )
19	6 18	syl	⊢ ( 𝜑 → ◡ 𝑓 : 𝐴 –1-1-onto→ ( 1 ... 𝑀 ) )
20		f1oco	⊢ ( ( ◡ 𝑓 : 𝐴 –1-1-onto→ ( 1 ... 𝑀 ) ∧ 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 ) → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) )
21	19 7 20	syl2anc	⊢ ( 𝜑 → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) )
22		ovex	⊢ ( 1 ... 𝑁 ) ∈ V
23	22	f1oen	⊢ ( ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) → ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) )
24	21 23	syl	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) )
25		fzfi	⊢ ( 1 ... 𝑁 ) ∈ Fin
26		fzfi	⊢ ( 1 ... 𝑀 ) ∈ Fin
27		hashen	⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( 1 ... 𝑀 ) ∈ Fin ) → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ ( 1 ... 𝑀 ) ) ↔ ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) ) )
28	25 26 27	mp2an	⊢ ( ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ ( 1 ... 𝑀 ) ) ↔ ( 1 ... 𝑁 ) ≈ ( 1 ... 𝑀 ) )
29	24 28	sylibr	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = ( ♯ ‘ ( 1 ... 𝑀 ) ) )
30	5	simprd	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
31	30	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
32		hashfz1	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
33	31 32	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
34	14	nnnn0d	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
35		hashfz1	⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
36	34 35	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
37	29 33 36	3eqtr3rd	⊢ ( 𝜑 → 𝑀 = 𝑁 )
38	37	oveq2d	⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( 1 ... 𝑁 ) )
39	38	f1oeq2d	⊢ ( 𝜑 → ( ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) ↔ ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑀 ) ) )
40	21 39	mpbird	⊢ ( 𝜑 → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) )
41		fveq2	⊢ ( 𝑗 = 𝑚 → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ 𝑚 ) )
42	41	csbeq1d	⊢ ( 𝑗 = 𝑚 → ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 )
43		elfznn	⊢ ( 𝑚 ∈ ( 1 ... 𝑀 ) → 𝑚 ∈ ℕ )
44	43	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → 𝑚 ∈ ℕ )
45		f1of	⊢ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
46	6 45	syl	⊢ ( 𝜑 → 𝑓 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
47	46	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 )
48	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
49	48	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
50		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵
51	50	nfel1	⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ
52		csbeq1a	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑚 ) → 𝐵 = ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 )
53	52	eleq1d	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑚 ) → ( 𝐵 ∈ ℂ ↔ ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
54	51 53	rspc	⊢ ( ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
55	47 49 54	sylc	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ )
56	3 42 44 55	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑚 ) = ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 )
57	56 55	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑚 ) ∈ ℂ )
58	38	f1oeq2d	⊢ ( 𝜑 → ( 𝐾 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ↔ 𝐾 : ( 1 ... 𝑁 ) –1-1-onto→ 𝐴 ) )
59	7 58	mpbird	⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 )
60		f1of	⊢ ( 𝐾 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 → 𝐾 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
61	59 60	syl	⊢ ( 𝜑 → 𝐾 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
62		fvco3	⊢ ( ( 𝐾 : ( 1 ... 𝑀 ) ⟶ 𝐴 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) = ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) )
63	61 62	sylan	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) = ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) )
64	63	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) = ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) ) )
65	6	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 )
66	61	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐾 ‘ 𝑖 ) ∈ 𝐴 )
67		f1ocnvfv2	⊢ ( ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ∧ ( 𝐾 ‘ 𝑖 ) ∈ 𝐴 ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ 𝑖 ) )
68	65 66 67	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ ( 𝐾 ‘ 𝑖 ) ) ) = ( 𝐾 ‘ 𝑖 ) )
69	64 68	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) = ( 𝐾 ‘ 𝑖 ) )
70	69	csbeq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 )
71	70	fveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( I ‘ ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 ) = ( I ‘ ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) )
72		f1of	⊢ ( ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) –1-1-onto→ ( 1 ... 𝑀 ) → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
73	40 72	syl	⊢ ( 𝜑 → ( ◡ 𝑓 ∘ 𝐾 ) : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
74	73	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ( 1 ... 𝑀 ) )
75		elfznn	⊢ ( ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ( 1 ... 𝑀 ) → ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ℕ )
76		fveq2	⊢ ( 𝑗 = ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) )
77	76	csbeq1d	⊢ ( 𝑗 = ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) → ⦋ ( 𝑓 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 )
78	77 3	fvmpti	⊢ ( ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ∈ ℕ → ( 𝐺 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) = ( I ‘ ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 ) )
79	74 75 78	3syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) = ( I ‘ ⦋ ( 𝑓 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) / 𝑘 ⦌ 𝐵 ) )
80		elfznn	⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ℕ )
81	80	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑖 ∈ ℕ )
82		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝐾 ‘ 𝑗 ) = ( 𝐾 ‘ 𝑖 ) )
83	82	csbeq1d	⊢ ( 𝑗 = 𝑖 → ⦋ ( 𝐾 ‘ 𝑗 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 )
84	83 4	fvmpti	⊢ ( 𝑖 ∈ ℕ → ( 𝐻 ‘ 𝑖 ) = ( I ‘ ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) )
85	81 84	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐻 ‘ 𝑖 ) = ( I ‘ ⦋ ( 𝐾 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 ) )
86	71 79 85	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐻 ‘ 𝑖 ) = ( 𝐺 ‘ ( ( ◡ 𝑓 ∘ 𝐾 ) ‘ 𝑖 ) ) )
87	9 11 13 16 17 40 57 86	seqf1o	⊢ ( 𝜑 → ( seq 1 ( · , 𝐻 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
88	37	fveq2d	⊢ ( 𝜑 → ( seq 1 ( · , 𝐻 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐻 ) ‘ 𝑁 ) )
89	87 88	eqtr3d	⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , 𝐻 ) ‘ 𝑁 ) )