Metamath Proof Explorer

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 ⊢ 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
prodtp.1 ⊢ k = C → D = G
prodtp.c ⊢ φ → C ∈ X
prodtp.g ⊢ φ → G ∈ ℂ
prodtp.2 ⊢ φ → A ≠ C
prodtp.3 ⊢ φ → B ≠ C
Assertion prodtp ⊢ φ → ∏ k ∈ A B C D = E ⁢ F ⁢ G

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 prodtp.1 ⊢ k = C → D = G
9 prodtp.c ⊢ φ → C ∈ X
10 prodtp.g ⊢ φ → G ∈ ℂ
11 prodtp.2 ⊢ φ → A ≠ C
12 prodtp.3 ⊢ φ → B ≠ C
13 disjprsn ⊢ A ≠ C ∧ B ≠ C → A B ∩ C = ∅
14 11 12 13 syl2anc ⊢ φ → A B ∩ C = ∅
15 df-tp ⊢ A B C = A B ∪ C
16 15 a1i ⊢ φ → A B C = A B ∪ C
17 tpfi ⊢ A B C ∈ Fin
18 17 a1i ⊢ φ → A B C ∈ Fin
19 vex ⊢ k ∈ V
20 19 eltp ⊢ k ∈ A B C ↔ k = A ∨ k = B ∨ k = C
21 1 adantl ⊢ φ ∧ k = A → D = E
22 5 adantr ⊢ φ ∧ k = A → E ∈ ℂ
23 21 22 eqeltrd ⊢ φ ∧ k = A → D ∈ ℂ
24 23 adantlr ⊢ φ ∧ k = A ∨ k = B ∨ k = C ∧ k = A → D ∈ ℂ
25 2 adantl ⊢ φ ∧ k = B → D = F
26 6 adantr ⊢ φ ∧ k = B → F ∈ ℂ
27 25 26 eqeltrd ⊢ φ ∧ k = B → D ∈ ℂ
28 27 adantlr ⊢ φ ∧ k = A ∨ k = B ∨ k = C ∧ k = B → D ∈ ℂ
29 8 adantl ⊢ φ ∧ k = C → D = G
30 10 adantr ⊢ φ ∧ k = C → G ∈ ℂ
31 29 30 eqeltrd ⊢ φ ∧ k = C → D ∈ ℂ
32 31 adantlr ⊢ φ ∧ k = A ∨ k = B ∨ k = C ∧ k = C → D ∈ ℂ
33 simpr ⊢ φ ∧ k = A ∨ k = B ∨ k = C → k = A ∨ k = B ∨ k = C
34 24 28 32 33 mpjao3dan ⊢ φ ∧ k = A ∨ k = B ∨ k = C → D ∈ ℂ
35 20 34 sylan2b ⊢ φ ∧ k ∈ A B C → D ∈ ℂ
36 14 16 18 35 fprodsplit ⊢ φ → ∏ k ∈ A B C D = ∏ k ∈ A B D ⁢ ∏ k ∈ C D
37 1 2 3 4 5 6 7 prodpr ⊢ φ → ∏ k ∈ A B D = E ⁢ F
38 8 prodsn ⊢ C ∈ X ∧ G ∈ ℂ → ∏ k ∈ C D = G
39 9 10 38 syl2anc ⊢ φ → ∏ k ∈ C D = G
40 37 39 oveq12d ⊢ φ → ∏ k ∈ A B D ⁢ ∏ k ∈ C D = E ⁢ F ⁢ G
41 36 40 eqtrd ⊢ φ → ∏ k ∈ A B C D = E ⁢ F ⁢ G