prodpr

Description: A product over a pair 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	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion	prodpr	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐷 = ( 𝐸 · 𝐹 ) )

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		disjsn2	⊢ ( 𝐴 ≠ 𝐵 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
9	7 8	syl	⊢ ( 𝜑 → ( { 𝐴 } ∩ { 𝐵 } ) = ∅ )
10		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
11	10	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } ) )
12		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
13	12	a1i	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ Fin )
14		vex	⊢ 𝑘 ∈ V
15	14	elpr	⊢ ( 𝑘 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) )
16	1	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐷 = 𝐸 )
17	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐸 ∈ ℂ )
18	16 17	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐴 ) → 𝐷 ∈ ℂ )
19	2	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐷 = 𝐹 )
20	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐹 ∈ ℂ )
21	19 20	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐵 ) → 𝐷 ∈ ℂ )
22	18 21	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝐴 ∨ 𝑘 = 𝐵 ) ) → 𝐷 ∈ ℂ )
23	15 22	sylan2b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝐴 , 𝐵 } ) → 𝐷 ∈ ℂ )
24	9 11 13 23	fprodsplit	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐷 = ( ∏ 𝑘 ∈ { 𝐴 } 𝐷 · ∏ 𝑘 ∈ { 𝐵 } 𝐷 ) )
25	1	prodsn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐸 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝐴 } 𝐷 = 𝐸 )
26	3 5 25	syl2anc	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐴 } 𝐷 = 𝐸 )
27	2	prodsn	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐹 ∈ ℂ ) → ∏ 𝑘 ∈ { 𝐵 } 𝐷 = 𝐹 )
28	4 6 27	syl2anc	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐵 } 𝐷 = 𝐹 )
29	26 28	oveq12d	⊢ ( 𝜑 → ( ∏ 𝑘 ∈ { 𝐴 } 𝐷 · ∏ 𝑘 ∈ { 𝐵 } 𝐷 ) = ( 𝐸 · 𝐹 ) )
30	24 29	eqtrd	⊢ ( 𝜑 → ∏ 𝑘 ∈ { 𝐴 , 𝐵 } 𝐷 = ( 𝐸 · 𝐹 ) )

Metamath Proof Explorer

Theorem prodpr

Proof