prodtp

Description: A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022)

	Ref	Expression
Hypotheses	prodpr.1	$⊢ k = A \to D = E$
	prodpr.2	$⊢ k = B \to D = F$
	prodpr.a	$⊢ φ \to A \in V$
	prodpr.b	$⊢ φ \to B \in W$
	prodpr.e	$⊢ φ \to E \in ℂ$
	prodpr.f	$⊢ φ \to F \in ℂ$
	prodpr.3	$⊢ φ \to A \neq B$
	prodtp.1	$⊢ k = C \to D = G$
	prodtp.c	$⊢ φ \to C \in X$
	prodtp.g	$⊢ φ \to G \in ℂ$
	prodtp.2	$⊢ φ \to A \neq C$
	prodtp.3	$⊢ φ \to B \neq C$
Assertion	prodtp	$⊢ φ \to \prod_{k \in \{A, B, C\}} D = E F G$

Proof

Step	Hyp	Ref	Expression
1		prodpr.1	$⊢ k = A \to D = E$
2		prodpr.2	$⊢ k = B \to D = F$
3		prodpr.a	$⊢ φ \to A \in V$
4		prodpr.b	$⊢ φ \to B \in W$
5		prodpr.e	$⊢ φ \to E \in ℂ$
6		prodpr.f	$⊢ φ \to F \in ℂ$
7		prodpr.3	$⊢ φ \to A \neq B$
8		prodtp.1	$⊢ k = C \to D = G$
9		prodtp.c	$⊢ φ \to C \in X$
10		prodtp.g	$⊢ φ \to G \in ℂ$
11		prodtp.2	$⊢ φ \to A \neq C$
12		prodtp.3	$⊢ φ \to B \neq C$
13		disjprsn	$⊢ (A \neq C \land B \neq C) \to \{A, B\} \cap \{C\} = \emptyset$
14	11 12 13	syl2anc	$⊢ φ \to \{A, B\} \cap \{C\} = \emptyset$
15		df-tp	$⊢ \{A, B, C\} = \{A, B\} \cup \{C\}$
16	15	a1i	$⊢ φ \to \{A, B, C\} = \{A, B\} \cup \{C\}$
17		tpfi	$⊢ \{A, B, C\} \in Fin$
18	17	a1i	$⊢ φ \to \{A, B, C\} \in Fin$
19		vex	$⊢ k \in V$
20	19	eltp	$⊢ k \in \{A, B, C\} \leftrightarrow (k = A \lor k = B \lor k = C)$
21	1	adantl	$⊢ (φ \land k = A) \to D = E$
22	5	adantr	$⊢ (φ \land k = A) \to E \in ℂ$
23	21 22	eqeltrd	$⊢ (φ \land k = A) \to D \in ℂ$
24	23	adantlr	$⊢ ((φ \land (k = A \lor k = B \lor k = C)) \land k = A) \to D \in ℂ$
25	2	adantl	$⊢ (φ \land k = B) \to D = F$
26	6	adantr	$⊢ (φ \land k = B) \to F \in ℂ$
27	25 26	eqeltrd	$⊢ (φ \land k = B) \to D \in ℂ$
28	27	adantlr	$⊢ ((φ \land (k = A \lor k = B \lor k = C)) \land k = B) \to D \in ℂ$
29	8	adantl	$⊢ (φ \land k = C) \to D = G$
30	10	adantr	$⊢ (φ \land k = C) \to G \in ℂ$
31	29 30	eqeltrd	$⊢ (φ \land k = C) \to D \in ℂ$
32	31	adantlr	$⊢ ((φ \land (k = A \lor k = B \lor k = C)) \land k = C) \to D \in ℂ$
33		simpr	$⊢ (φ \land (k = A \lor k = B \lor k = C)) \to (k = A \lor k = B \lor k = C)$
34	24 28 32 33	mpjao3dan	$⊢ (φ \land (k = A \lor k = B \lor k = C)) \to D \in ℂ$
35	20 34	sylan2b	$⊢ (φ \land k \in \{A, B, C\}) \to D \in ℂ$
36	14 16 18 35	fprodsplit	$⊢ φ \to \prod_{k \in \{A, B, C\}} D = \prod_{k \in \{A, B\}} D \prod_{k \in \{C\}} D$
37	1 2 3 4 5 6 7	prodpr	$⊢ φ \to \prod_{k \in \{A, B\}} D = E F$
38	8	prodsn	$⊢ (C \in X \land G \in ℂ) \to \prod_{k \in \{C\}} D = G$
39	9 10 38	syl2anc	$⊢ φ \to \prod_{k \in \{C\}} D = G$
40	37 39	oveq12d	$⊢ φ \to \prod_{k \in \{A, B\}} D \prod_{k \in \{C\}} D = E F G$
41	36 40	eqtrd	$⊢ φ \to \prod_{k \in \{A, B, C\}} D = E F G$

Metamath Proof Explorer

Theorem prodtp

Proof