Metamath Proof Explorer

Theorem cbvproddavw2

Description: Change bound variable and the set of integers in a product. Deduction form. (Contributed by GG, 14-Aug-2025)

Ref Expression
Hypotheses cbvproddavw2.1 
|- ( ph -> A = B )
cbvproddavw2.2 
|- ( ( ph /\ j = k ) -> C = D )
Assertion cbvproddavw2 
|- ( ph -> prod_ j e. A C = prod_ k e. B D )

Proof

Step Hyp Ref Expression
1 cbvproddavw2.1 
 |-  ( ph -> A = B )
2 cbvproddavw2.2 
 |-  ( ( ph /\ j = k ) -> C = D )
3 1 sseq1d 
 |-  ( ph -> ( A C_ ( ZZ>= ` m ) <-> B C_ ( ZZ>= ` m ) ) )
4 simpr 
 |-  ( ( ph /\ j = k ) -> j = k )
5 1 adantr 
 |-  ( ( ph /\ j = k ) -> A = B )
6 4 5 eleq12d 
 |-  ( ( ph /\ j = k ) -> ( j e. A <-> k e. B ) )
7 6 2 ifbieq1d 
 |-  ( ( ph /\ j = k ) -> if ( j e. A , C , 1 ) = if ( k e. B , D , 1 ) )
8 7 cbvmptdavw 
 |-  ( ph -> ( j e. ZZ |-> if ( j e. A , C , 1 ) ) = ( k e. ZZ |-> if ( k e. B , D , 1 ) ) )
9 8 seqeq3d 
 |-  ( ph -> seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) = seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) )
10 9 breq1d 
 |-  ( ph -> ( seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> y <-> seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> y ) )
11 10 anbi2d 
 |-  ( ph -> ( ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> y ) <-> ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> y ) ) )
12 11 exbidv 
 |-  ( ph -> ( E. y ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> y ) <-> E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> y ) ) )
13 12 rexbidv 
 |-  ( ph -> ( E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> y ) <-> E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> y ) ) )
14 8 seqeq3d 
 |-  ( ph -> seq m ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) = seq m ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) )
15 14 breq1d 
 |-  ( ph -> ( seq m ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> x <-> seq m ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> x ) )
16 3 13 15 3anbi123d 
 |-  ( ph -> ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> x ) <-> ( B C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> x ) ) )
17 16 rexbidv 
 |-  ( ph -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> x ) <-> E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> x ) ) )
18 1 f1oeq3d 
 |-  ( ph -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... m ) -1-1-onto-> B ) )
19 2 cbvcsbdavw 
 |-  ( ph -> [_ ( f ` n ) / j ]_ C = [_ ( f ` n ) / k ]_ D )
20 19 mpteq2dv 
 |-  ( ph -> ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) )
21 20 seqeq3d 
 |-  ( ph -> seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) = seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) )
22 21 fveq1d 
 |-  ( ph -> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) )
23 22 eqeq2d 
 |-  ( ph -> ( x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) <-> x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) )
24 18 23 anbi12d 
 |-  ( ph -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) )
25 24 exbidv 
 |-  ( ph -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) )
26 25 rexbidv 
 |-  ( ph -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) )
27 17 26 orbi12d 
 |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) ) <-> ( E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) ) )
28 27 iotabidv 
 |-  ( ph -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) ) ) = ( iota x ( E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) ) )
29 df-prod 
 |-  prod_ j e. A C = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) ) ) )
30 df-prod 
 |-  prod_ k e. B D = ( iota x ( E. m e. ZZ ( B C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) ) ) )
31 28 29 30 3eqtr4g 
 |-  ( ph -> prod_ j e. A C = prod_ k e. B D )