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 
|- ( 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 )
Assertion prodpr 
|- ( ph -> prod_ k e. { A , B } D = ( E x. F ) )

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 disjsn2 
 |-  ( A =/= B -> ( { A } i^i { B } ) = (/) )
9 7 8 syl 
 |-  ( ph -> ( { A } i^i { B } ) = (/) )
10 df-pr 
 |-  { A , B } = ( { A } u. { B } )
11 10 a1i 
 |-  ( ph -> { A , B } = ( { A } u. { B } ) )
12 prfi 
 |-  { A , B } e. Fin
13 12 a1i 
 |-  ( ph -> { A , B } e. Fin )
14 vex 
 |-  k e. _V
15 14 elpr 
 |-  ( k e. { A , B } <-> ( k = A \/ k = B ) )
16 1 adantl 
 |-  ( ( ph /\ k = A ) -> D = E )
17 5 adantr 
 |-  ( ( ph /\ k = A ) -> E e. CC )
18 16 17 eqeltrd 
 |-  ( ( ph /\ k = A ) -> D e. CC )
19 2 adantl 
 |-  ( ( ph /\ k = B ) -> D = F )
20 6 adantr 
 |-  ( ( ph /\ k = B ) -> F e. CC )
21 19 20 eqeltrd 
 |-  ( ( ph /\ k = B ) -> D e. CC )
22 18 21 jaodan 
 |-  ( ( ph /\ ( k = A \/ k = B ) ) -> D e. CC )
23 15 22 sylan2b 
 |-  ( ( ph /\ k e. { A , B } ) -> D e. CC )
24 9 11 13 23 fprodsplit 
 |-  ( ph -> prod_ k e. { A , B } D = ( prod_ k e. { A } D x. prod_ k e. { B } D ) )
25 1 prodsn 
 |-  ( ( A e. V /\ E e. CC ) -> prod_ k e. { A } D = E )
26 3 5 25 syl2anc 
 |-  ( ph -> prod_ k e. { A } D = E )
27 2 prodsn 
 |-  ( ( B e. W /\ F e. CC ) -> prod_ k e. { B } D = F )
28 4 6 27 syl2anc 
 |-  ( ph -> prod_ k e. { B } D = F )
29 26 28 oveq12d 
 |-  ( ph -> ( prod_ k e. { A } D x. prod_ k e. { B } D ) = ( E x. F ) )
30 24 29 eqtrd 
 |-  ( ph -> prod_ k e. { A , B } D = ( E x. F ) )