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 
|- ( ph -> A e. V )
prodpr.b 
|- ( ph -> B e. W )
prodpr.e 
|- ( ph -> E e. CC )
prodpr.f 
|- ( ph -> F e. CC )
prodpr.3 
|- ( ph -> A =/= B )
prodtp.1 
|- ( k = C -> D = G )
prodtp.c 
|- ( ph -> C e. X )
prodtp.g 
|- ( ph -> G e. CC )
prodtp.2 
|- ( ph -> A =/= C )
prodtp.3 
|- ( ph -> B =/= C )
Assertion prodtp 
|- ( ph -> prod_ k e. { A , B , C } D = ( ( E x. F ) x. G ) )

Proof

Step Hyp Ref Expression
1 prodpr.1 
 |-  ( k = A -> D = E )
2 prodpr.2 
 |-  ( k = B -> D = F )
3 prodpr.a 
 |-  ( ph -> A e. V )
4 prodpr.b 
 |-  ( ph -> B e. W )
5 prodpr.e 
 |-  ( ph -> E e. CC )
6 prodpr.f 
 |-  ( ph -> F e. CC )
7 prodpr.3 
 |-  ( ph -> A =/= B )
8 prodtp.1 
 |-  ( k = C -> D = G )
9 prodtp.c 
 |-  ( ph -> C e. X )
10 prodtp.g 
 |-  ( ph -> G e. CC )
11 prodtp.2 
 |-  ( ph -> A =/= C )
12 prodtp.3 
 |-  ( ph -> B =/= C )
13 disjprsn 
 |-  ( ( A =/= C /\ B =/= C ) -> ( { A , B } i^i { C } ) = (/) )
14 11 12 13 syl2anc 
 |-  ( ph -> ( { A , B } i^i { C } ) = (/) )
15 df-tp 
 |-  { A , B , C } = ( { A , B } u. { C } )
16 15 a1i 
 |-  ( ph -> { A , B , C } = ( { A , B } u. { C } ) )
17 tpfi 
 |-  { A , B , C } e. Fin
18 17 a1i 
 |-  ( ph -> { A , B , C } e. Fin )
19 vex 
 |-  k e. _V
20 19 eltp 
 |-  ( k e. { A , B , C } <-> ( k = A \/ k = B \/ k = C ) )
21 1 adantl 
 |-  ( ( ph /\ k = A ) -> D = E )
22 5 adantr 
 |-  ( ( ph /\ k = A ) -> E e. CC )
23 21 22 eqeltrd 
 |-  ( ( ph /\ k = A ) -> D e. CC )
24 23 adantlr 
 |-  ( ( ( ph /\ ( k = A \/ k = B \/ k = C ) ) /\ k = A ) -> D e. CC )
25 2 adantl 
 |-  ( ( ph /\ k = B ) -> D = F )
26 6 adantr 
 |-  ( ( ph /\ k = B ) -> F e. CC )
27 25 26 eqeltrd 
 |-  ( ( ph /\ k = B ) -> D e. CC )
28 27 adantlr 
 |-  ( ( ( ph /\ ( k = A \/ k = B \/ k = C ) ) /\ k = B ) -> D e. CC )
29 8 adantl 
 |-  ( ( ph /\ k = C ) -> D = G )
30 10 adantr 
 |-  ( ( ph /\ k = C ) -> G e. CC )
31 29 30 eqeltrd 
 |-  ( ( ph /\ k = C ) -> D e. CC )
32 31 adantlr 
 |-  ( ( ( ph /\ ( k = A \/ k = B \/ k = C ) ) /\ k = C ) -> D e. CC )
33 simpr 
 |-  ( ( ph /\ ( k = A \/ k = B \/ k = C ) ) -> ( k = A \/ k = B \/ k = C ) )
34 24 28 32 33 mpjao3dan 
 |-  ( ( ph /\ ( k = A \/ k = B \/ k = C ) ) -> D e. CC )
35 20 34 sylan2b 
 |-  ( ( ph /\ k e. { A , B , C } ) -> D e. CC )
36 14 16 18 35 fprodsplit 
 |-  ( ph -> prod_ k e. { A , B , C } D = ( prod_ k e. { A , B } D x. prod_ k e. { C } D ) )
37 1 2 3 4 5 6 7 prodpr 
 |-  ( ph -> prod_ k e. { A , B } D = ( E x. F ) )
38 8 prodsn 
 |-  ( ( C e. X /\ G e. CC ) -> prod_ k e. { C } D = G )
39 9 10 38 syl2anc 
 |-  ( ph -> prod_ k e. { C } D = G )
40 37 39 oveq12d 
 |-  ( ph -> ( prod_ k e. { A , B } D x. prod_ k e. { C } D ) = ( ( E x. F ) x. G ) )
41 36 40 eqtrd 
 |-  ( ph -> prod_ k e. { A , B , C } D = ( ( E x. F ) x. G ) )