summolem3

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

Proof

Step	Hyp	Ref	Expression
1		summo.1	$⊢ F = (k \in ℤ ⟼ if (k \in A, B, 0))$
2		summo.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		summo.3	$⊢ G = (n \in ℕ ⟼ ⦋ f (n) / k ⦌ B)$
4		summolem3.4	$⊢ H = (n \in ℕ ⟼ ⦋ K (n) / k ⦌ B)$
5		summolem3.5	$⊢ φ \to (M \in ℕ \land N \in ℕ)$
6		summolem3.6	$⊢ φ \to f : (1 \dots M) \underset{1-1 onto}{⟶} A$
7		summolem3.7	$⊢ φ \to K : (1 \dots N) \underset{1-1 onto}{⟶} A$
8		addcl	$⊢ (m \in ℂ \land j \in ℂ) \to m + j \in ℂ$
9	8	adantl	$⊢ (φ \land (m \in ℂ \land j \in ℂ)) \to m + j \in ℂ$
10		addcom	$⊢ (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		addass	$⊢ (m \in ℂ \land j \in ℂ \land y \in ℂ) \to m + j + y = m + j + y$
13	12	adantl	$⊢ (φ \land (m \in ℂ \land j \in ℂ \land y \in ℂ)) \to m + j + y = m + j + y$
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		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
32		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
33	30 31 32	3syl	$⊢ φ \to \|(1 \dots N)\| = N$
34		nnnn0	$⊢ M \in ℕ \to M \in ℕ_{0}$
35		hashfz1	$⊢ M \in ℕ_{0} \to \|(1 \dots M)\| = M$
36	14 34 35	3syl	$⊢ φ \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	$⊢ n = m \to f (n) = f (m)$
42	41	csbeq1d	$⊢ n = m \to ⦋ f (n) / 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	eqtr2d	$⊢ (φ \land i \in (1 \dots M)) \to K (i) = f ((f^{-1} \circ K) (i))$
70	69	csbeq1d	$⊢ (φ \land i \in (1 \dots M)) \to ⦋ K (i) / k ⦌ B = ⦋ f ((f^{-1} \circ K) (i)) / k ⦌ B$
71	70	fveq2d	$⊢ (φ \land i \in (1 \dots M)) \to I (⦋ K (i) / k ⦌ B) = I (⦋ f ((f^{-1} \circ K) (i)) / k ⦌ B)$
72		elfznn	$⊢ i \in (1 \dots M) \to i \in ℕ$
73	72	adantl	$⊢ (φ \land i \in (1 \dots M)) \to i \in ℕ$
74		fveq2	$⊢ n = i \to K (n) = K (i)$
75	74	csbeq1d	$⊢ n = i \to ⦋ K (n) / k ⦌ B = ⦋ K (i) / k ⦌ B$
76	75 4	fvmpti	$⊢ i \in ℕ \to H (i) = I (⦋ K (i) / k ⦌ B)$
77	73 76	syl	$⊢ (φ \land i \in (1 \dots M)) \to H (i) = I (⦋ K (i) / k ⦌ B)$
78		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)$
79	40 78	syl	$⊢ φ \to (f^{-1} \circ K) : (1 \dots M) ⟶ (1 \dots M)$
80	79	ffvelcdmda	$⊢ (φ \land i \in (1 \dots M)) \to (f^{-1} \circ K) (i) \in (1 \dots M)$
81		elfznn	$⊢ (f^{-1} \circ K) (i) \in (1 \dots M) \to (f^{-1} \circ K) (i) \in ℕ$
82		fveq2	$⊢ n = (f^{-1} \circ K) (i) \to f (n) = f ((f^{-1} \circ K) (i))$
83	82	csbeq1d	$⊢ n = (f^{-1} \circ K) (i) \to ⦋ f (n) / k ⦌ B = ⦋ f ((f^{-1} \circ K) (i)) / k ⦌ B$
84	83 3	fvmpti	$⊢ (f^{-1} \circ K) (i) \in ℕ \to G ((f^{-1} \circ K) (i)) = I (⦋ f ((f^{-1} \circ K) (i)) / k ⦌ B)$
85	80 81 84	3syl	$⊢ (φ \land i \in (1 \dots M)) \to G ((f^{-1} \circ K) (i)) = I (⦋ f ((f^{-1} \circ K) (i)) / k ⦌ B)$
86	71 77 85	3eqtr4d	$⊢ (φ \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 (+ H) (M) = seq 1 (+ G) (M)$
88	37	fveq2d	$⊢ φ \to seq 1 (+ H) (M) = seq 1 (+ H) (N)$
89	87 88	eqtr3d	$⊢ φ \to seq 1 (+ G) (M) = seq 1 (+ H) (N)$

Metamath Proof Explorer

Theorem summolem3

Proof