fprodconst

Description: The product of constant terms ( k is not free in B ). (Contributed by Scott Fenton, 12-Jan-2018)

		Ref	Expression
	Assertion	fprodconst	$⊢ (A \in Fin \land B \in ℂ) \to \prod_{k \in A} B = B^{\|A\|}$

Proof

Step	Hyp	Ref	Expression
1		exp0	$⊢ B \in ℂ \to B^{0} = 1$
2	1	eqcomd	$⊢ B \in ℂ \to 1 = B^{0}$
3		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} B = \prod_{k \in \emptyset} B$
4		prod0	$⊢ \prod_{k \in \emptyset} B = 1$
5	3 4	eqtrdi	$⊢ A = \emptyset \to \prod_{k \in A} B = 1$
6		fveq2	$⊢ A = \emptyset \to \|A\| = \|\emptyset\|$
7		hash0	$⊢ \|\emptyset\| = 0$
8	6 7	eqtrdi	$⊢ A = \emptyset \to \|A\| = 0$
9	8	oveq2d	$⊢ A = \emptyset \to B^{\|A\|} = B^{0}$
10	5 9	eqeq12d	$⊢ A = \emptyset \to (\prod_{k \in A} B = B^{\|A\|} \leftrightarrow 1 = B^{0})$
11	2 10	syl5ibrcom	$⊢ B \in ℂ \to (A = \emptyset \to \prod_{k \in A} B = B^{\|A\|})$
12	11	adantl	$⊢ (A \in Fin \land B \in ℂ) \to (A = \emptyset \to \prod_{k \in A} B = B^{\|A\|})$
13		eqidd	$⊢ k = f (n) \to B = B$
14		simprl	$⊢ ((A \in Fin \land B \in ℂ) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
15		simprr	$⊢ ((A \in Fin \land B \in ℂ) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
16		simpllr	$⊢ (((A \in Fin \land B \in ℂ) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land k \in A) \to B \in ℂ$
17		simpllr	$⊢ (((A \in Fin \land B \in ℂ) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to B \in ℂ$
18		elfznn	$⊢ n \in (1 \dots \|A\|) \to n \in ℕ$
19	18	adantl	$⊢ (((A \in Fin \land B \in ℂ) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to n \in ℕ$
20		fvconst2g	$⊢ (B \in ℂ \land n \in ℕ) \to (ℕ \times \{B\}) (n) = B$
21	17 19 20	syl2anc	$⊢ (((A \in Fin \land B \in ℂ) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to (ℕ \times \{B\}) (n) = B$
22	13 14 15 16 21	fprod	$⊢ ((A \in Fin \land B \in ℂ) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{k \in A} B = seq 1 (\times (ℕ \times \{B\})) (\|A\|)$
23		expnnval	$⊢ (B \in ℂ \land \|A\| \in ℕ) \to B^{\|A\|} = seq 1 (\times (ℕ \times \{B\})) (\|A\|)$
24	23	ad2ant2lr	$⊢ ((A \in Fin \land B \in ℂ) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to B^{\|A\|} = seq 1 (\times (ℕ \times \{B\})) (\|A\|)$
25	22 24	eqtr4d	$⊢ ((A \in Fin \land B \in ℂ) \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{k \in A} B = B^{\|A\|}$
26	25	expr	$⊢ ((A \in Fin \land B \in ℂ) \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} B = B^{\|A\|})$
27	26	exlimdv	$⊢ ((A \in Fin \land B \in ℂ) \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} B = B^{\|A\|})$
28	27	expimpd	$⊢ (A \in Fin \land B \in ℂ) \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \prod_{k \in A} B = B^{\|A\|})$
29		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
30	29	adantr	$⊢ (A \in Fin \land B \in ℂ) \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
31	12 28 30	mpjaod	$⊢ (A \in Fin \land B \in ℂ) \to \prod_{k \in A} B = B^{\|A\|}$

Metamath Proof Explorer

Theorem fprodconst

Proof