fprodexp

Description: Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodexp.kph	$⊢ Ⅎ k φ$
	fprodexp.n	$⊢ φ \to N \in ℕ_{0}$
	fprodexp.a	$⊢ φ \to A \in Fin$
	fprodexp.b	$⊢ (φ \land k \in A) \to B \in ℂ$
Assertion	fprodexp	$⊢ φ \to \prod_{k \in A} B^{N} = {\prod_{k \in A} B}^{N}$

Proof

Step	Hyp	Ref	Expression
1		fprodexp.kph	$⊢ Ⅎ k φ$
2		fprodexp.n	$⊢ φ \to N \in ℕ_{0}$
3		fprodexp.a	$⊢ φ \to A \in Fin$
4		fprodexp.b	$⊢ (φ \land k \in A) \to B \in ℂ$
5		prodeq1	$⊢ x = \emptyset \to \prod_{k \in x} B^{N} = \prod_{k \in \emptyset} B^{N}$
6		prodeq1	$⊢ x = \emptyset \to \prod_{k \in x} B = \prod_{k \in \emptyset} B$
7	6	oveq1d	$⊢ x = \emptyset \to {\prod_{k \in x} B}^{N} = {\prod_{k \in \emptyset} B}^{N}$
8	5 7	eqeq12d	$⊢ x = \emptyset \to (\prod_{k \in x} B^{N} = {\prod_{k \in x} B}^{N} \leftrightarrow \prod_{k \in \emptyset} B^{N} = {\prod_{k \in \emptyset} B}^{N})$
9		prodeq1	$⊢ x = y \to \prod_{k \in x} B^{N} = \prod_{k \in y} B^{N}$
10		prodeq1	$⊢ x = y \to \prod_{k \in x} B = \prod_{k \in y} B$
11	10	oveq1d	$⊢ x = y \to {\prod_{k \in x} B}^{N} = {\prod_{k \in y} B}^{N}$
12	9 11	eqeq12d	$⊢ x = y \to (\prod_{k \in x} B^{N} = {\prod_{k \in x} B}^{N} \leftrightarrow \prod_{k \in y} B^{N} = {\prod_{k \in y} B}^{N})$
13		prodeq1	$⊢ x = y \cup \{z\} \to \prod_{k \in x} B^{N} = \prod_{k \in y \cup \{z\}} B^{N}$
14		prodeq1	$⊢ x = y \cup \{z\} \to \prod_{k \in x} B = \prod_{k \in y \cup \{z\}} B$
15	14	oveq1d	$⊢ x = y \cup \{z\} \to {\prod_{k \in x} B}^{N} = {\prod_{k \in y \cup \{z\}} B}^{N}$
16	13 15	eqeq12d	$⊢ x = y \cup \{z\} \to (\prod_{k \in x} B^{N} = {\prod_{k \in x} B}^{N} \leftrightarrow \prod_{k \in y \cup \{z\}} B^{N} = {\prod_{k \in y \cup \{z\}} B}^{N})$
17		prodeq1	$⊢ x = A \to \prod_{k \in x} B^{N} = \prod_{k \in A} B^{N}$
18		prodeq1	$⊢ x = A \to \prod_{k \in x} B = \prod_{k \in A} B$
19	18	oveq1d	$⊢ x = A \to {\prod_{k \in x} B}^{N} = {\prod_{k \in A} B}^{N}$
20	17 19	eqeq12d	$⊢ x = A \to (\prod_{k \in x} B^{N} = {\prod_{k \in x} B}^{N} \leftrightarrow \prod_{k \in A} B^{N} = {\prod_{k \in A} B}^{N})$
21	2	nn0zd	$⊢ φ \to N \in ℤ$
22		1exp	$⊢ N \in ℤ \to 1^{N} = 1$
23	21 22	syl	$⊢ φ \to 1^{N} = 1$
24	23	eqcomd	$⊢ φ \to 1 = 1^{N}$
25		prod0	$⊢ \prod_{k \in \emptyset} B^{N} = 1$
26	25	a1i	$⊢ φ \to \prod_{k \in \emptyset} B^{N} = 1$
27		prod0	$⊢ \prod_{k \in \emptyset} B = 1$
28	27	oveq1i	$⊢ {\prod_{k \in \emptyset} B}^{N} = 1^{N}$
29	28	a1i	$⊢ φ \to {\prod_{k \in \emptyset} B}^{N} = 1^{N}$
30	24 26 29	3eqtr4d	$⊢ φ \to \prod_{k \in \emptyset} B^{N} = {\prod_{k \in \emptyset} B}^{N}$
31		nfv	$⊢ Ⅎ k (y \subseteq A \land z \in (A ∖ y))$
32	1 31	nfan	$⊢ Ⅎ k (φ \land (y \subseteq A \land z \in (A ∖ y)))$
33	3	adantr	$⊢ (φ \land y \subseteq A) \to A \in Fin$
34		simpr	$⊢ (φ \land y \subseteq A) \to y \subseteq A$
35		ssfi	$⊢ (A \in Fin \land y \subseteq A) \to y \in Fin$
36	33 34 35	syl2anc	$⊢ (φ \land y \subseteq A) \to y \in Fin$
37	36	adantrr	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to y \in Fin$
38		simpll	$⊢ ((φ \land y \subseteq A) \land k \in y) \to φ$
39	34	sselda	$⊢ ((φ \land y \subseteq A) \land k \in y) \to k \in A$
40	38 39 4	syl2anc	$⊢ ((φ \land y \subseteq A) \land k \in y) \to B \in ℂ$
41	40	adantlrr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in y) \to B \in ℂ$
42	32 37 41	fprodclf	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \prod_{k \in y} B \in ℂ$
43		simpl	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to φ$
44		simprr	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to z \in (A ∖ y)$
45	44	eldifad	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to z \in A$
46		nfv	$⊢ Ⅎ k z \in A$
47	1 46	nfan	$⊢ Ⅎ k (φ \land z \in A)$
48		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ z / k ⦌ B$
49	48	nfel1	$⊢ Ⅎ k ⦋ z / k ⦌ B \in ℂ$
50	47 49	nfim	$⊢ Ⅎ k ((φ \land z \in A) \to ⦋ z / k ⦌ B \in ℂ)$
51		eleq1w	$⊢ k = z \to (k \in A \leftrightarrow z \in A)$
52	51	anbi2d	$⊢ k = z \to ((φ \land k \in A) \leftrightarrow (φ \land z \in A))$
53		csbeq1a	$⊢ k = z \to B = ⦋ z / k ⦌ B$
54	53	eleq1d	$⊢ k = z \to (B \in ℂ \leftrightarrow ⦋ z / k ⦌ B \in ℂ)$
55	52 54	imbi12d	$⊢ k = z \to (((φ \land k \in A) \to B \in ℂ) \leftrightarrow ((φ \land z \in A) \to ⦋ z / k ⦌ B \in ℂ))$
56	50 55 4	chvarfv	$⊢ (φ \land z \in A) \to ⦋ z / k ⦌ B \in ℂ$
57	43 45 56	syl2anc	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to ⦋ z / k ⦌ B \in ℂ$
58	2	adantr	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to N \in ℕ_{0}$
59		mulexp	$⊢ (\prod_{k \in y} B \in ℂ \land ⦋ z / k ⦌ B \in ℂ \land N \in ℕ_{0}) \to {\prod_{k \in y} B ⦋ z / k ⦌ B}^{N} = {\prod_{k \in y} B}^{N} {⦋ z / k ⦌ B}^{N}$
60	42 57 58 59	syl3anc	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to {\prod_{k \in y} B ⦋ z / k ⦌ B}^{N} = {\prod_{k \in y} B}^{N} {⦋ z / k ⦌ B}^{N}$
61	60	eqcomd	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to {\prod_{k \in y} B}^{N} {⦋ z / k ⦌ B}^{N} = {\prod_{k \in y} B ⦋ z / k ⦌ B}^{N}$
62	61	adantr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \prod_{k \in y} B^{N} = {\prod_{k \in y} B}^{N}) \to {\prod_{k \in y} B}^{N} {⦋ z / k ⦌ B}^{N} = {\prod_{k \in y} B ⦋ z / k ⦌ B}^{N}$
63		nfcv	$⊢ \underline{Ⅎ} k^$
64		nfcv	$⊢ \underline{Ⅎ} k N$
65	48 63 64	nfov	$⊢ \underline{Ⅎ} k {⦋ z / k ⦌ B}^{N}$
66	44	eldifbd	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \neg z \in y$
67	2	ad2antrr	$⊢ ((φ \land y \subseteq A) \land k \in y) \to N \in ℕ_{0}$
68	40 67	expcld	$⊢ ((φ \land y \subseteq A) \land k \in y) \to B^{N} \in ℂ$
69	68	adantlrr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land k \in y) \to B^{N} \in ℂ$
70	53	oveq1d	$⊢ k = z \to B^{N} = {⦋ z / k ⦌ B}^{N}$
71	57 58	expcld	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to {⦋ z / k ⦌ B}^{N} \in ℂ$
72	32 65 37 44 66 69 70 71	fprodsplitsn	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \prod_{k \in y \cup \{z\}} B^{N} = \prod_{k \in y} B^{N} {⦋ z / k ⦌ B}^{N}$
73	72	adantr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \prod_{k \in y} B^{N} = {\prod_{k \in y} B}^{N}) \to \prod_{k \in y \cup \{z\}} B^{N} = \prod_{k \in y} B^{N} {⦋ z / k ⦌ B}^{N}$
74		oveq1	$⊢ \prod_{k \in y} B^{N} = {\prod_{k \in y} B}^{N} \to \prod_{k \in y} B^{N} {⦋ z / k ⦌ B}^{N} = {\prod_{k \in y} B}^{N} {⦋ z / k ⦌ B}^{N}$
75	74	adantl	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \prod_{k \in y} B^{N} = {\prod_{k \in y} B}^{N}) \to \prod_{k \in y} B^{N} {⦋ z / k ⦌ B}^{N} = {\prod_{k \in y} B}^{N} {⦋ z / k ⦌ B}^{N}$
76	73 75	eqtrd	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \prod_{k \in y} B^{N} = {\prod_{k \in y} B}^{N}) \to \prod_{k \in y \cup \{z\}} B^{N} = {\prod_{k \in y} B}^{N} {⦋ z / k ⦌ B}^{N}$
77	32 48 37 44 66 41 53 57	fprodsplitsn	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to \prod_{k \in y \cup \{z\}} B = \prod_{k \in y} B ⦋ z / k ⦌ B$
78	77	adantr	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \prod_{k \in y} B^{N} = {\prod_{k \in y} B}^{N}) \to \prod_{k \in y \cup \{z\}} B = \prod_{k \in y} B ⦋ z / k ⦌ B$
79	78	oveq1d	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \prod_{k \in y} B^{N} = {\prod_{k \in y} B}^{N}) \to {\prod_{k \in y \cup \{z\}} B}^{N} = {\prod_{k \in y} B ⦋ z / k ⦌ B}^{N}$
80	62 76 79	3eqtr4d	$⊢ ((φ \land (y \subseteq A \land z \in (A ∖ y))) \land \prod_{k \in y} B^{N} = {\prod_{k \in y} B}^{N}) \to \prod_{k \in y \cup \{z\}} B^{N} = {\prod_{k \in y \cup \{z\}} B}^{N}$
81	80	ex	$⊢ (φ \land (y \subseteq A \land z \in (A ∖ y))) \to (\prod_{k \in y} B^{N} = {\prod_{k \in y} B}^{N} \to \prod_{k \in y \cup \{z\}} B^{N} = {\prod_{k \in y \cup \{z\}} B}^{N})$
82	8 12 16 20 30 81 3	findcard2d	$⊢ φ \to \prod_{k \in A} B^{N} = {\prod_{k \in A} B}^{N}$

Metamath Proof Explorer

Theorem fprodexp

Proof