prodmolem3

	Ref	Expression
Hypotheses	prodmo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 1))$
	prodmo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	prodmo.3	$⊢ G = (j \in ℕ ⟼ ⦋ f (j) / k ⦌ B)$
	prodmolem3.4	$⊢ H = (j \in ℕ ⟼ ⦋ K (j) / k ⦌ B)$
	prodmolem3.5	$⊢ φ \to (M \in ℕ \land N \in ℕ)$
	prodmolem3.6	$⊢ φ \to f : (1 \dots M) \underset{1-1 onto}{⟶} A$
	prodmolem3.7	$⊢ φ \to K : (1 \dots N) \underset{1-1 onto}{⟶} A$
Assertion	prodmolem3	$⊢ φ \to seq 1 (\times G) (M) = seq 1 (\times H) (N)$

Proof

Step	Hyp	Ref	Expression
1		prodmo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 1))$
2		prodmo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		prodmo.3	$⊢ G = (j \in ℕ ⟼ ⦋ f (j) / k ⦌ B)$
4		prodmolem3.4	$⊢ H = (j \in ℕ ⟼ ⦋ K (j) / k ⦌ B)$
5		prodmolem3.5	$⊢ φ \to (M \in ℕ \land N \in ℕ)$
6		prodmolem3.6	$⊢ φ \to f : (1 \dots M) \underset{1-1 onto}{⟶} A$
7		prodmolem3.7	$⊢ φ \to K : (1 \dots N) \underset{1-1 onto}{⟶} A$
8		mulcl	$⊢ (m \in ℂ \land j \in ℂ) \to m j \in ℂ$
9	8	adantl	$⊢ (φ \land (m \in ℂ \land j \in ℂ)) \to m j \in ℂ$
10		mulcom	$⊢ (m \in ℂ \land j \in ℂ) \to m j = j m$
11	10	adantl	$⊢ (φ \land (m \in ℂ \land j \in ℂ)) \to m j = j m$
12		mulass	$⊢ (m \in ℂ \land j \in ℂ \land z \in ℂ) \to m j z = m j z$
13	12	adantl	$⊢ (φ \land (m \in ℂ \land j \in ℂ \land z \in ℂ)) \to m j z = m j z$
14	5	simpld	$⊢ φ \to M \in ℕ$
15		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
16	14 15	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 1}$
17		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
18		f1ocnv	$⊢ f : (1 \dots M) \underset{1-1 onto}{⟶} A \to f^{-1} : A \underset{1-1 onto}{⟶} (1 \dots M)$
19	6 18	syl	$⊢ φ \to f^{-1} : A \underset{1-1 onto}{⟶} (1 \dots M)$
20		f1oco	$⊢ (f^{-1} : A \underset{1-1 onto}{⟶} (1 \dots M) \land K : (1 \dots N) \underset{1-1 onto}{⟶} A) \to (f^{-1} \circ K) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots M)$
21	19 7 20	syl2anc	$⊢ φ \to (f^{-1} \circ K) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots M)$
22		ovex	$⊢ (1 \dots N) \in V$
23	22	f1oen	$⊢ (f^{-1} \circ K) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots M) \to (1 \dots N) \approx (1 \dots M)$
24	21 23	syl	$⊢ φ \to (1 \dots N) \approx (1 \dots M)$
25		fzfi	$⊢ (1 \dots N) \in Fin$
26		fzfi	$⊢ (1 \dots M) \in Fin$
27		hashen	$⊢ ((1 \dots N) \in Fin \land (1 \dots M) \in Fin) \to (\|(1 \dots N)\| = \|(1 \dots M)\| \leftrightarrow (1 \dots N) \approx (1 \dots M))$
28	25 26 27	mp2an	$⊢ \|(1 \dots N)\| = \|(1 \dots M)\| \leftrightarrow (1 \dots N) \approx (1 \dots M)$
29	24 28	sylibr	$⊢ φ \to \|(1 \dots N)\| = \|(1 \dots M)\|$
30	5	simprd	$⊢ φ \to N \in ℕ$
31	30	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
32		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
33	31 32	syl	$⊢ φ \to \|(1 \dots N)\| = N$
34	14	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
35		hashfz1	$⊢ M \in ℕ_{0} \to \|(1 \dots M)\| = M$
36	34 35	syl	$⊢ φ \to \|(1 \dots M)\| = M$
37	29 33 36	3eqtr3rd	$⊢ φ \to M = N$
38	37	oveq2d	$⊢ φ \to (1 \dots M) = (1 \dots N)$
39	38	f1oeq2d	$⊢ φ \to ((f^{-1} \circ K) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \leftrightarrow (f^{-1} \circ K) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots M))$
40	21 39	mpbird	$⊢ φ \to (f^{-1} \circ K) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M)$
41		fveq2	$⊢ j = m \to f (j) = f (m)$
42	41	csbeq1d	$⊢ j = m \to ⦋ f (j) / k ⦌ B = ⦋ f (m) / k ⦌ B$
43		elfznn	$⊢ m \in (1 \dots M) \to m \in ℕ$
44	43	adantl	$⊢ (φ \land m \in (1 \dots M)) \to m \in ℕ$
45		f1of	$⊢ f : (1 \dots M) \underset{1-1 onto}{⟶} A \to f : (1 \dots M) ⟶ A$
46	6 45	syl	$⊢ φ \to f : (1 \dots M) ⟶ A$
47	46	ffvelcdmda	$⊢ (φ \land m \in (1 \dots M)) \to f (m) \in A$
48	2	ralrimiva	$⊢ φ \to \forall k \in A B \in ℂ$
49	48	adantr	$⊢ (φ \land m \in (1 \dots M)) \to \forall k \in A B \in ℂ$
50		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ f (m) / k ⦌ B$
51	50	nfel1	$⊢ Ⅎ k ⦋ f (m) / k ⦌ B \in ℂ$
52		csbeq1a	$⊢ k = f (m) \to B = ⦋ f (m) / k ⦌ B$
53	52	eleq1d	$⊢ k = f (m) \to (B \in ℂ \leftrightarrow ⦋ f (m) / k ⦌ B \in ℂ)$
54	51 53	rspc	$⊢ f (m) \in A \to (\forall k \in A B \in ℂ \to ⦋ f (m) / k ⦌ B \in ℂ)$
55	47 49 54	sylc	$⊢ (φ \land m \in (1 \dots M)) \to ⦋ f (m) / k ⦌ B \in ℂ$
56	3 42 44 55	fvmptd3	$⊢ (φ \land m \in (1 \dots M)) \to G (m) = ⦋ f (m) / k ⦌ B$
57	56 55	eqeltrd	$⊢ (φ \land m \in (1 \dots M)) \to G (m) \in ℂ$
58	38	f1oeq2d	$⊢ φ \to (K : (1 \dots M) \underset{1-1 onto}{⟶} A \leftrightarrow K : (1 \dots N) \underset{1-1 onto}{⟶} A)$
59	7 58	mpbird	$⊢ φ \to K : (1 \dots M) \underset{1-1 onto}{⟶} A$
60		f1of	$⊢ K : (1 \dots M) \underset{1-1 onto}{⟶} A \to K : (1 \dots M) ⟶ A$
61	59 60	syl	$⊢ φ \to K : (1 \dots M) ⟶ A$
62		fvco3	$⊢ (K : (1 \dots M) ⟶ A \land i \in (1 \dots M)) \to (f^{-1} \circ K) (i) = f^{-1} (K (i))$
63	61 62	sylan	$⊢ (φ \land i \in (1 \dots M)) \to (f^{-1} \circ K) (i) = f^{-1} (K (i))$
64	63	fveq2d	$⊢ (φ \land i \in (1 \dots M)) \to f ((f^{-1} \circ K) (i)) = f (f^{-1} (K (i)))$
65	6	adantr	$⊢ (φ \land i \in (1 \dots M)) \to f : (1 \dots M) \underset{1-1 onto}{⟶} A$
66	61	ffvelcdmda	$⊢ (φ \land i \in (1 \dots M)) \to K (i) \in A$
67		f1ocnvfv2	$⊢ (f : (1 \dots M) \underset{1-1 onto}{⟶} A \land K (i) \in A) \to f (f^{-1} (K (i))) = K (i)$
68	65 66 67	syl2anc	$⊢ (φ \land i \in (1 \dots M)) \to f (f^{-1} (K (i))) = K (i)$
69	64 68	eqtrd	$⊢ (φ \land i \in (1 \dots M)) \to f ((f^{-1} \circ K) (i)) = K (i)$
70	69	csbeq1d	$⊢ (φ \land i \in (1 \dots M)) \to ⦋ f ((f^{-1} \circ K) (i)) / k ⦌ B = ⦋ K (i) / k ⦌ B$
71	70	fveq2d	$⊢ (φ \land i \in (1 \dots M)) \to I (⦋ f ((f^{-1} \circ K) (i)) / k ⦌ B) = I (⦋ K (i) / k ⦌ B)$
72		f1of	$⊢ (f^{-1} \circ K) : (1 \dots M) \underset{1-1 onto}{⟶} (1 \dots M) \to (f^{-1} \circ K) : (1 \dots M) ⟶ (1 \dots M)$
73	40 72	syl	$⊢ φ \to (f^{-1} \circ K) : (1 \dots M) ⟶ (1 \dots M)$
74	73	ffvelcdmda	$⊢ (φ \land i \in (1 \dots M)) \to (f^{-1} \circ K) (i) \in (1 \dots M)$
75		elfznn	$⊢ (f^{-1} \circ K) (i) \in (1 \dots M) \to (f^{-1} \circ K) (i) \in ℕ$
76		fveq2	$⊢ j = (f^{-1} \circ K) (i) \to f (j) = f ((f^{-1} \circ K) (i))$
77	76	csbeq1d	$⊢ j = (f^{-1} \circ K) (i) \to ⦋ f (j) / k ⦌ B = ⦋ f ((f^{-1} \circ K) (i)) / k ⦌ B$
78	77 3	fvmpti	$⊢ (f^{-1} \circ K) (i) \in ℕ \to G ((f^{-1} \circ K) (i)) = I (⦋ f ((f^{-1} \circ K) (i)) / k ⦌ B)$
79	74 75 78	3syl	$⊢ (φ \land i \in (1 \dots M)) \to G ((f^{-1} \circ K) (i)) = I (⦋ f ((f^{-1} \circ K) (i)) / k ⦌ B)$
80		elfznn	$⊢ i \in (1 \dots M) \to i \in ℕ$
81	80	adantl	$⊢ (φ \land i \in (1 \dots M)) \to i \in ℕ$
82		fveq2	$⊢ j = i \to K (j) = K (i)$
83	82	csbeq1d	$⊢ j = i \to ⦋ K (j) / k ⦌ B = ⦋ K (i) / k ⦌ B$
84	83 4	fvmpti	$⊢ i \in ℕ \to H (i) = I (⦋ K (i) / k ⦌ B)$
85	81 84	syl	$⊢ (φ \land i \in (1 \dots M)) \to H (i) = I (⦋ K (i) / k ⦌ B)$
86	71 79 85	3eqtr4rd	$⊢ (φ \land i \in (1 \dots M)) \to H (i) = G ((f^{-1} \circ K) (i))$
87	9 11 13 16 17 40 57 86	seqf1o	$⊢ φ \to seq 1 (\times H) (M) = seq 1 (\times G) (M)$
88	37	fveq2d	$⊢ φ \to seq 1 (\times H) (M) = seq 1 (\times H) (N)$
89	87 88	eqtr3d	$⊢ φ \to seq 1 (\times G) (M) = seq 1 (\times H) (N)$

Metamath Proof Explorer

Theorem prodmolem3

Proof