Metamath Proof Explorer

Theorem fprod

Description: The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017)

Ref Expression
Hypotheses fprod.1 
|- ( k = ( F ` n ) -> B = C )
fprod.2 
|- ( ph -> M e. NN )
fprod.3 
|- ( ph -> F : ( 1 ... M ) -1-1-onto-> A )
fprod.4 
|- ( ( ph /\ k e. A ) -> B e. CC )
fprod.5 
|- ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )
Assertion fprod 
|- ( ph -> prod_ k e. A B = ( seq 1 ( x. , G ) ` M ) )

Proof

Step Hyp Ref Expression
1 fprod.1 
 |-  ( k = ( F ` n ) -> B = C )
2 fprod.2 
 |-  ( ph -> M e. NN )
3 fprod.3 
 |-  ( ph -> F : ( 1 ... M ) -1-1-onto-> A )
4 fprod.4 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
5 fprod.5 
 |-  ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )
6 df-prod 
 |-  prod_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
7 fvex 
 |-  ( seq 1 ( x. , G ) ` M ) e. _V
8 nfcv 
 |-  F/_ j if ( k e. A , B , 1 )
9 nfv 
 |-  F/ k j e. A
10 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
11 nfcv 
 |-  F/_ k 1
12 9 10 11 nfif 
 |-  F/_ k if ( j e. A , [_ j / k ]_ B , 1 )
13 eleq1w 
 |-  ( k = j -> ( k e. A <-> j e. A ) )
14 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
15 13 14 ifbieq1d 
 |-  ( k = j -> if ( k e. A , B , 1 ) = if ( j e. A , [_ j / k ]_ B , 1 ) )
16 8 12 15 cbvmpt 
 |-  ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( j e. ZZ |-> if ( j e. A , [_ j / k ]_ B , 1 ) )
17 4 ralrimiva 
 |-  ( ph -> A. k e. A B e. CC )
18 10 nfel1 
 |-  F/ k [_ j / k ]_ B e. CC
19 14 eleq1d 
 |-  ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )
20 18 19 rspc 
 |-  ( j e. A -> ( A. k e. A B e. CC -> [_ j / k ]_ B e. CC ) )
21 17 20 mpan9 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
22 fveq2 
 |-  ( n = i -> ( f ` n ) = ( f ` i ) )
23 22 csbeq1d 
 |-  ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / k ]_ B )
24 csbcow 
 |-  [_ ( f ` i ) / j ]_ [_ j / k ]_ B = [_ ( f ` i ) / k ]_ B
25 23 24 eqtr4di 
 |-  ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / j ]_ [_ j / k ]_ B )
26 25 cbvmptv 
 |-  ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( i e. NN |-> [_ ( f ` i ) / j ]_ [_ j / k ]_ B )
27 16 21 26 prodmo 
 |-  ( ph -> E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
28 f1of 
 |-  ( F : ( 1 ... M ) -1-1-onto-> A -> F : ( 1 ... M ) --> A )
29 3 28 syl 
 |-  ( ph -> F : ( 1 ... M ) --> A )
30 ovex 
 |-  ( 1 ... M ) e. _V
31 fex 
 |-  ( ( F : ( 1 ... M ) --> A /\ ( 1 ... M ) e. _V ) -> F e. _V )
32 29 30 31 sylancl 
 |-  ( ph -> F e. _V )
33 nnuz 
 |-  NN = ( ZZ>= ` 1 )
34 2 33 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
35 elfznn 
 |-  ( n e. ( 1 ... M ) -> n e. NN )
36 fvex 
 |-  ( G ` n ) e. _V
37 5 36 eqeltrrdi 
 |-  ( ( ph /\ n e. ( 1 ... M ) ) -> C e. _V )
38 eqid 
 |-  ( n e. NN |-> C ) = ( n e. NN |-> C )
39 38 fvmpt2 
 |-  ( ( n e. NN /\ C e. _V ) -> ( ( n e. NN |-> C ) ` n ) = C )
40 35 37 39 syl2an2 
 |-  ( ( ph /\ n e. ( 1 ... M ) ) -> ( ( n e. NN |-> C ) ` n ) = C )
41 5 40 eqtr4d 
 |-  ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = ( ( n e. NN |-> C ) ` n ) )
42 41 ralrimiva 
 |-  ( ph -> A. n e. ( 1 ... M ) ( G ` n ) = ( ( n e. NN |-> C ) ` n ) )
43 nffvmpt1 
 |-  F/_ n ( ( n e. NN |-> C ) ` k )
44 43 nfeq2 
 |-  F/ n ( G ` k ) = ( ( n e. NN |-> C ) ` k )
45 fveq2 
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
46 fveq2 
 |-  ( n = k -> ( ( n e. NN |-> C ) ` n ) = ( ( n e. NN |-> C ) ` k ) )
47 45 46 eqeq12d 
 |-  ( n = k -> ( ( G ` n ) = ( ( n e. NN |-> C ) ` n ) <-> ( G ` k ) = ( ( n e. NN |-> C ) ` k ) ) )
48 44 47 rspc 
 |-  ( k e. ( 1 ... M ) -> ( A. n e. ( 1 ... M ) ( G ` n ) = ( ( n e. NN |-> C ) ` n ) -> ( G ` k ) = ( ( n e. NN |-> C ) ` k ) ) )
49 42 48 mpan9 
 |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( G ` k ) = ( ( n e. NN |-> C ) ` k ) )
50 34 49 seqfveq 
 |-  ( ph -> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> C ) ) ` M ) )
51 3 50 jca 
 |-  ( ph -> ( F : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> C ) ) ` M ) ) )
52 f1oeq1 
 |-  ( f = F -> ( f : ( 1 ... M ) -1-1-onto-> A <-> F : ( 1 ... M ) -1-1-onto-> A ) )
53 fveq1 
 |-  ( f = F -> ( f ` n ) = ( F ` n ) )
54 53 csbeq1d 
 |-  ( f = F -> [_ ( f ` n ) / k ]_ B = [_ ( F ` n ) / k ]_ B )
55 fvex 
 |-  ( F ` n ) e. _V
56 55 1 csbie 
 |-  [_ ( F ` n ) / k ]_ B = C
57 54 56 eqtrdi 
 |-  ( f = F -> [_ ( f ` n ) / k ]_ B = C )
58 57 mpteq2dv 
 |-  ( f = F -> ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( n e. NN |-> C ) )
59 58 seqeq3d 
 |-  ( f = F -> seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) = seq 1 ( x. , ( n e. NN |-> C ) ) )
60 59 fveq1d 
 |-  ( f = F -> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> C ) ) ` M ) )
61 60 eqeq2d 
 |-  ( f = F -> ( ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) <-> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> C ) ) ` M ) ) )
62 52 61 anbi12d 
 |-  ( f = F -> ( ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) <-> ( F : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> C ) ) ` M ) ) ) )
63 32 51 62 spcedv 
 |-  ( ph -> E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) )
64 oveq2 
 |-  ( m = M -> ( 1 ... m ) = ( 1 ... M ) )
65 64 f1oeq2d 
 |-  ( m = M -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... M ) -1-1-onto-> A ) )
66 fveq2 
 |-  ( m = M -> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) )
67 66 eqeq2d 
 |-  ( m = M -> ( ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) <-> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) )
68 65 67 anbi12d 
 |-  ( m = M -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) ) )
69 68 exbidv 
 |-  ( m = M -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) ) )
70 69 rspcev 
 |-  ( ( M e. NN /\ E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) ) -> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
71 2 63 70 syl2anc 
 |-  ( ph -> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
72 71 olcd 
 |-  ( ph -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
73 breq2 
 |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x <-> seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) )
74 73 3anbi3d 
 |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) <-> ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) ) )
75 74 rexbidv 
 |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) <-> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) ) )
76 eqeq1 
 |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) <-> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
77 76 anbi2d 
 |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
78 77 exbidv 
 |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
79 78 rexbidv 
 |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
80 75 79 orbi12d 
 |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) )
81 80 moi2 
 |-  ( ( ( ( seq 1 ( x. , G ) ` M ) e. _V /\ E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) /\ ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( x. , G ) ` M ) )
82 7 81 mpanl1 
 |-  ( ( E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( x. , G ) ` M ) )
83 82 ancom2s 
 |-  ( ( E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( x. , G ) ` M ) )
84 83 expr 
 |-  ( ( E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) -> x = ( seq 1 ( x. , G ) ` M ) ) )
85 27 72 84 syl2anc 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) -> x = ( seq 1 ( x. , G ) ` M ) ) )
86 72 80 syl5ibrcom 
 |-  ( ph -> ( x = ( seq 1 ( x. , G ) ` M ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) )
87 85 86 impbid 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> x = ( seq 1 ( x. , G ) ` M ) ) )
88 87 adantr 
 |-  ( ( ph /\ ( seq 1 ( x. , G ) ` M ) e. _V ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> x = ( seq 1 ( x. , G ) ` M ) ) )
89 88 iota5 
 |-  ( ( ph /\ ( seq 1 ( x. , G ) ` M ) e. _V ) -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) = ( seq 1 ( x. , G ) ` M ) )
90 7 89 mpan2 
 |-  ( ph -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) = ( seq 1 ( x. , G ) ` M ) )
91 6 90 eqtrid 
 |-  ( ph -> prod_ k e. A B = ( seq 1 ( x. , G ) ` M ) )