This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ k = A → D = E
prodpr.2 ⊢ k = B → D = F
prodpr.a ⊢ φ → A ∈ V
prodpr.b ⊢ φ → B ∈ W
prodpr.e ⊢ φ → E ∈ ℂ
prodpr.f ⊢ φ → F ∈ ℂ
prodpr.3 ⊢ φ → A ≠ B
Assertion prodpr ⊢ φ → ∏ k ∈ A B D = E ⁢ F

Proof

Step Hyp Ref Expression
1 prodpr.1 ⊢ k = A → D = E
2 prodpr.2 ⊢ k = B → D = F
3 prodpr.a ⊢ φ → A ∈ V
4 prodpr.b ⊢ φ → B ∈ W
5 prodpr.e ⊢ φ → E ∈ ℂ
6 prodpr.f ⊢ φ → F ∈ ℂ
7 prodpr.3 ⊢ φ → A ≠ B
8 disjsn2 ⊢ A ≠ B → A ∩ B = ∅
9 7 8 syl ⊢ φ → A ∩ B = ∅
10 df-pr ⊢ A B = A ∪ B
11 10 a1i ⊢ φ → A B = A ∪ B
12 prfi ⊢ A B ∈ Fin
13 12 a1i ⊢ φ → A B ∈ Fin
14 vex ⊢ k ∈ V
15 14 elpr ⊢ k ∈ A B ↔ k = A ∨ k = B
16 1 adantl ⊢ φ ∧ k = A → D = E
17 5 adantr ⊢ φ ∧ k = A → E ∈ ℂ
18 16 17 eqeltrd ⊢ φ ∧ k = A → D ∈ ℂ
19 2 adantl ⊢ φ ∧ k = B → D = F
20 6 adantr ⊢ φ ∧ k = B → F ∈ ℂ
21 19 20 eqeltrd ⊢ φ ∧ k = B → D ∈ ℂ
22 18 21 jaodan ⊢ φ ∧ k = A ∨ k = B → D ∈ ℂ
23 15 22 sylan2b ⊢ φ ∧ k ∈ A B → D ∈ ℂ
24 9 11 13 23 fprodsplit ⊢ φ → ∏ k ∈ A B D = ∏ k ∈ A D ⁢ ∏ k ∈ B D
25 1 prodsn ⊢ A ∈ V ∧ E ∈ ℂ → ∏ k ∈ A D = E
26 3 5 25 syl2anc ⊢ φ → ∏ k ∈ A D = E
27 2 prodsn ⊢ B ∈ W ∧ F ∈ ℂ → ∏ k ∈ B D = F
28 4 6 27 syl2anc ⊢ φ → ∏ k ∈ B D = F
29 26 28 oveq12d ⊢ φ → ∏ k ∈ A D ⁢ ∏ k ∈ B D = E ⁢ F
30 24 29 eqtrd ⊢ φ → ∏ k ∈ A B D = E ⁢ F