Theorem 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	⊢ ( 𝑘 = 𝐴 → 𝐷 = 𝐸 )
	prodpr.2	⊢ ( 𝑘 = 𝐵 → 𝐷 = 𝐹 )
	prodpr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	prodpr.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	prodpr.e	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
	prodpr.f	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
	prodpr.3	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	prodtp.1	⊢ ( 𝑘 = 𝐶 → 𝐷 = 𝐺 )
	prodtp.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	prodtp.g	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
	prodtp.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
	prodtp.3	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion	prodtp	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝐷 = ( ( 𝐸 · 𝐹 ) · 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		prodpr.1	⊢ ( 𝑘 = 𝐴 → 𝐷 = 𝐸 )
2		prodpr.2	⊢ ( 𝑘 = 𝐵 → 𝐷 = 𝐹 )
3		prodpr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		prodpr.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5		prodpr.e	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
6		prodpr.f	⊢ ( 𝜑 → 𝐹 ∈ ℂ )
7		prodpr.3	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
8		prodtp.1	⊢ ( 𝑘 = 𝐶 → 𝐷 = 𝐺 )
9		prodtp.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
10		prodtp.g	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
11		prodtp.2	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
12		prodtp.3	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
13		disjprsn	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ )
14	11 12 13	syl2anc	⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∩ { 𝐶 } ) = ∅ )
15		df-tp	⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
16	15	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) )
17		tpfi	⊢ { 𝐴 , 𝐵 , 𝐶 } ∈ Fin
18	17	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ∈ Fin )
19		vex	⊢ 𝑘 ∈ V
20	19	eltp	⊢ ( 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ∨ 𝑘 = 𝐶 ) )
21	1	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐷 = 𝐸 )
22	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐸 ∈ ℂ )
23	21 22	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐷 ∈ ℂ )
24	23	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ∨ 𝑘 = 𝐶 ) ) ∧ 𝑘 = 𝐴 ) → 𝐷 ∈ ℂ )
25	2	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐷 = 𝐹 )
26	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐹 ∈ ℂ )
27	25 26	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐷 ∈ ℂ )
28	27	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ∨ 𝑘 = 𝐶 ) ) ∧ 𝑘 = 𝐵 ) → 𝐷 ∈ ℂ )
29	8	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐶 ) → 𝐷 = 𝐺 )
30	10	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐶 ) → 𝐺 ∈ ℂ )
31	29 30	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐶 ) → 𝐷 ∈ ℂ )
32	31	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ∨ 𝑘 = 𝐶 ) ) ∧ 𝑘 = 𝐶 ) → 𝐷 ∈ ℂ )
33		simpr	⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ∨ 𝑘 = 𝐶 ) ) → ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ∨ 𝑘 = 𝐶 ) )
34	24 28 32 33	mpjao3dan	⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ∨ 𝑘 = 𝐶 ) ) → 𝐷 ∈ ℂ )
35	20 34	sylan2b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } ) → 𝐷 ∈ ℂ )
36	14 16 18 35	fprodsplit	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝐷 = ( ∏ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐷 · ∏ 𝑘 ∈ { 𝐶 } 𝐷 ) )
37	1 2 3 4 5 6 7	prodpr	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐷 = ( 𝐸 · 𝐹 ) )
38	8	prodsn	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐺 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝐶 } 𝐷 = 𝐺 )
39	9 10 38	syl2anc	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐶 } 𝐷 = 𝐺 )
40	37 39	oveq12d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐷 · ∏ 𝑘 ∈ { 𝐶 } 𝐷 ) = ( ( 𝐸 · 𝐹 ) · 𝐺 ) )
41	36 40	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐴 , 𝐵 , 𝐶 } 𝐷 = ( ( 𝐸 · 𝐹 ) · 𝐺 ) )