prodsn

Description: A product of a singleton is the term. (Contributed by Scott Fenton, 14-Dec-2017)

		Ref	Expression
	Hypothesis	prodsn.1	$⊢ k = M \to A = B$
	Assertion	prodsn	$⊢ (M \in V \land B \in ℂ) \to \prod_{k \in \{M\}} A = B$

Proof

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

Metamath Proof Explorer

Theorem prodsn

Proof