Metamath Proof Explorer


Theorem fprodcl2lem

Description: Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017)

Ref Expression
Hypotheses fprodcllem.1
|- ( ph -> S C_ CC )
fprodcllem.2
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
fprodcllem.3
|- ( ph -> A e. Fin )
fprodcllem.4
|- ( ( ph /\ k e. A ) -> B e. S )
fprodcl2lem.5
|- ( ph -> A =/= (/) )
Assertion fprodcl2lem
|- ( ph -> prod_ k e. A B e. S )

Proof

Step Hyp Ref Expression
1 fprodcllem.1
 |-  ( ph -> S C_ CC )
2 fprodcllem.2
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
3 fprodcllem.3
 |-  ( ph -> A e. Fin )
4 fprodcllem.4
 |-  ( ( ph /\ k e. A ) -> B e. S )
5 fprodcl2lem.5
 |-  ( ph -> A =/= (/) )
6 5 a1d
 |-  ( ph -> ( -. prod_ k e. A B e. S -> A =/= (/) ) )
7 6 necon4bd
 |-  ( ph -> ( A = (/) -> prod_ k e. A B e. S ) )
8 prodfc
 |-  prod_ m e. A ( ( k e. A |-> B ) ` m ) = prod_ k e. A B
9 fveq2
 |-  ( m = ( f ` x ) -> ( ( k e. A |-> B ) ` m ) = ( ( k e. A |-> B ) ` ( f ` x ) ) )
10 simprl
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN )
11 simprr
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
12 1 adantr
 |-  ( ( ph /\ k e. A ) -> S C_ CC )
13 12 4 sseldd
 |-  ( ( ph /\ k e. A ) -> B e. CC )
14 13 fmpttd
 |-  ( ph -> ( k e. A |-> B ) : A --> CC )
15 14 ffvelrnda
 |-  ( ( ph /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC )
16 15 adantlr
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC )
17 f1of
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A )
18 17 ad2antll
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) --> A )
19 fvco3
 |-  ( ( f : ( 1 ... ( # ` A ) ) --> A /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) = ( ( k e. A |-> B ) ` ( f ` x ) ) )
20 18 19 sylan
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) = ( ( k e. A |-> B ) ` ( f ` x ) ) )
21 9 10 11 16 20 fprod
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> B ) ` m ) = ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) )
22 8 21 eqtr3id
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A B = ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) )
23 nnuz
 |-  NN = ( ZZ>= ` 1 )
24 10 23 eleqtrdi
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. ( ZZ>= ` 1 ) )
25 4 fmpttd
 |-  ( ph -> ( k e. A |-> B ) : A --> S )
26 fco
 |-  ( ( ( k e. A |-> B ) : A --> S /\ f : ( 1 ... ( # ` A ) ) --> A ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> S )
27 25 18 26 syl2an2r
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> S )
28 27 ffvelrnda
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ x e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` x ) e. S )
29 2 adantlr
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
30 24 28 29 seqcl
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) e. S )
31 22 30 eqeltrd
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A B e. S )
32 31 expr
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A B e. S ) )
33 32 exlimdv
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A B e. S ) )
34 33 expimpd
 |-  ( ph -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> prod_ k e. A B e. S ) )
35 fz1f1o
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
36 3 35 syl
 |-  ( ph -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
37 7 34 36 mpjaod
 |-  ( ph -> prod_ k e. A B e. S )