prodsnf

Description: A product of a singleton is the term. A version of prodsn using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	prodsnf.1	$⊢ \underline{Ⅎ} k B$
	prodsnf.2	$⊢ k = M \to A = B$
Assertion	prodsnf	$⊢ (M \in V \land B \in ℂ) \to \prod_{k \in \{M\}} A = B$

Proof

Step	Hyp	Ref	Expression
1		prodsnf.1	$⊢ \underline{Ⅎ} k B$
2		prodsnf.2	$⊢ k = M \to A = B$
3		nfcv	$⊢ \underline{Ⅎ} m A$
4		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ A$
5		csbeq1a	$⊢ k = m \to A = ⦋ m / k ⦌ A$
6	3 4 5	cbvprodi	$⊢ \prod_{k \in \{M\}} A = \prod_{m \in \{M\}} ⦋ m / k ⦌ A$
7		csbeq1	$⊢ m = \{⟨1, M⟩\} (n) \to ⦋ m / k ⦌ A = ⦋ \{⟨1, M⟩\} (n) / k ⦌ A$
8		1nn	$⊢ 1 \in ℕ$
9	8	a1i	$⊢ (M \in V \land B \in ℂ) \to 1 \in ℕ$
10		1z	$⊢ 1 \in ℤ$
11		f1osng	$⊢ (1 \in ℤ \land M \in V) \to \{⟨1, M⟩\} : \{1\} \underset{1-1 onto}{⟶} \{M\}$
12		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
13	10 12	ax-mp	$⊢ (1 \dots 1) = \{1\}$
14		f1oeq2	$⊢ (1 \dots 1) = \{1\} \to (\{⟨1, M⟩\} : (1 \dots 1) \underset{1-1 onto}{⟶} \{M\} \leftrightarrow \{⟨1, M⟩\} : \{1\} \underset{1-1 onto}{⟶} \{M\})$
15	13 14	ax-mp	$⊢ \{⟨1, M⟩\} : (1 \dots 1) \underset{1-1 onto}{⟶} \{M\} \leftrightarrow \{⟨1, M⟩\} : \{1\} \underset{1-1 onto}{⟶} \{M\}$
16	11 15	sylibr	$⊢ (1 \in ℤ \land M \in V) \to \{⟨1, M⟩\} : (1 \dots 1) \underset{1-1 onto}{⟶} \{M\}$
17	10 16	mpan	$⊢ M \in V \to \{⟨1, M⟩\} : (1 \dots 1) \underset{1-1 onto}{⟶} \{M\}$
18	17	adantr	$⊢ (M \in V \land B \in ℂ) \to \{⟨1, M⟩\} : (1 \dots 1) \underset{1-1 onto}{⟶} \{M\}$
19		velsn	$⊢ m \in \{M\} \leftrightarrow m = M$
20		csbeq1	$⊢ m = M \to ⦋ m / k ⦌ A = ⦋ M / k ⦌ A$
21	1	a1i	$⊢ M \in V \to \underline{Ⅎ} k B$
22	21 2	csbiegf	$⊢ M \in V \to ⦋ M / k ⦌ A = B$
23	22	adantr	$⊢ (M \in V \land B \in ℂ) \to ⦋ M / k ⦌ A = B$
24	20 23	sylan9eqr	$⊢ ((M \in V \land B \in ℂ) \land m = M) \to ⦋ m / k ⦌ A = B$
25	19 24	sylan2b	$⊢ ((M \in V \land B \in ℂ) \land m \in \{M\}) \to ⦋ m / k ⦌ A = B$
26		simplr	$⊢ ((M \in V \land B \in ℂ) \land m \in \{M\}) \to B \in ℂ$
27	25 26	eqeltrd	$⊢ ((M \in V \land B \in ℂ) \land m \in \{M\}) \to ⦋ m / k ⦌ A \in ℂ$
28	13	eleq2i	$⊢ n \in (1 \dots 1) \leftrightarrow n \in \{1\}$
29		velsn	$⊢ n \in \{1\} \leftrightarrow n = 1$
30	28 29	bitri	$⊢ n \in (1 \dots 1) \leftrightarrow n = 1$
31		fvsng	$⊢ (1 \in ℤ \land M \in V) \to \{⟨1, M⟩\} (1) = M$
32	10 31	mpan	$⊢ M \in V \to \{⟨1, M⟩\} (1) = M$
33	32	adantr	$⊢ (M \in V \land B \in ℂ) \to \{⟨1, M⟩\} (1) = M$
34	33	csbeq1d	$⊢ (M \in V \land B \in ℂ) \to ⦋ \{⟨1, M⟩\} (1) / k ⦌ A = ⦋ M / k ⦌ A$
35		simpr	$⊢ (M \in V \land B \in ℂ) \to B \in ℂ$
36		fvsng	$⊢ (1 \in ℤ \land B \in ℂ) \to \{⟨1, B⟩\} (1) = B$
37	10 35 36	sylancr	$⊢ (M \in V \land B \in ℂ) \to \{⟨1, B⟩\} (1) = B$
38	23 34 37	3eqtr4rd	$⊢ (M \in V \land B \in ℂ) \to \{⟨1, B⟩\} (1) = ⦋ \{⟨1, M⟩\} (1) / k ⦌ A$
39		fveq2	$⊢ n = 1 \to \{⟨1, B⟩\} (n) = \{⟨1, B⟩\} (1)$
40		fveq2	$⊢ n = 1 \to \{⟨1, M⟩\} (n) = \{⟨1, M⟩\} (1)$
41	40	csbeq1d	$⊢ n = 1 \to ⦋ \{⟨1, M⟩\} (n) / k ⦌ A = ⦋ \{⟨1, M⟩\} (1) / k ⦌ A$
42	39 41	eqeq12d	$⊢ n = 1 \to (\{⟨1, B⟩\} (n) = ⦋ \{⟨1, M⟩\} (n) / k ⦌ A \leftrightarrow \{⟨1, B⟩\} (1) = ⦋ \{⟨1, M⟩\} (1) / k ⦌ A)$
43	38 42	syl5ibrcom	$⊢ (M \in V \land B \in ℂ) \to (n = 1 \to \{⟨1, B⟩\} (n) = ⦋ \{⟨1, M⟩\} (n) / k ⦌ A)$
44	43	imp	$⊢ ((M \in V \land B \in ℂ) \land n = 1) \to \{⟨1, B⟩\} (n) = ⦋ \{⟨1, M⟩\} (n) / k ⦌ A$
45	30 44	sylan2b	$⊢ ((M \in V \land B \in ℂ) \land n \in (1 \dots 1)) \to \{⟨1, B⟩\} (n) = ⦋ \{⟨1, M⟩\} (n) / k ⦌ A$
46	7 9 18 27 45	fprod	$⊢ (M \in V \land B \in ℂ) \to \prod_{m \in \{M\}} ⦋ m / k ⦌ A = seq 1 (\times \{⟨1, B⟩\}) (1)$
47	6 46	eqtrid	$⊢ (M \in V \land B \in ℂ) \to \prod_{k \in \{M\}} A = seq 1 (\times \{⟨1, B⟩\}) (1)$
48	10 37	seq1i	$⊢ (M \in V \land B \in ℂ) \to seq 1 (\times \{⟨1, B⟩\}) (1) = B$
49	47 48	eqtrd	$⊢ (M \in V \land B \in ℂ) \to \prod_{k \in \{M\}} A = B$

Metamath Proof Explorer

Theorem prodsnf

Proof