Metamath Proof Explorer

Theorem cbvprodvw2

Description: Change bound variable and the set of integers in a product, using implicit substitution. (Contributed by GG, 1-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 cbvprodvw2.1 
 |-  A = B
2 cbvprodvw2.2 
 |-  ( j = k -> C = D )
3 1 sseq1i 
 |-  ( A C_ ( ZZ>= ` m ) <-> B C_ ( ZZ>= ` m ) )
4 1 eleq2i 
 |-  ( j e. A <-> j e. B )
5 eleq1w 
 |-  ( j = k -> ( j e. B <-> k e. B ) )
6 4 5 bitrid 
 |-  ( j = k -> ( j e. A <-> k e. B ) )
7 6 2 ifbieq1d 
 |-  ( j = k -> if ( j e. A , C , 1 ) = if ( k e. B , D , 1 ) )
8 7 cbvmptv 
 |-  ( j e. ZZ |-> if ( j e. A , C , 1 ) ) = ( k e. ZZ |-> if ( k e. B , D , 1 ) )
9 seqeq3 
 |-  ( ( j e. ZZ |-> if ( j e. A , C , 1 ) ) = ( k e. ZZ |-> if ( k e. B , D , 1 ) ) -> 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 8 9 ax-mp 
 |-  seq n ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) = seq n ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) )
11 10 breq1i 
 |-  ( 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 )
12 11 anbi2i 
 |-  ( ( 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 ) )
13 12 exbii 
 |-  ( 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 ) )
14 13 rexbii 
 |-  ( 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 ) )
15 seqeq3 
 |-  ( ( j e. ZZ |-> if ( j e. A , C , 1 ) ) = ( k e. ZZ |-> if ( k e. B , D , 1 ) ) -> seq m ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) = seq m ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) ) )
16 8 15 ax-mp 
 |-  seq m ( x. , ( j e. ZZ |-> if ( j e. A , C , 1 ) ) ) = seq m ( x. , ( k e. ZZ |-> if ( k e. B , D , 1 ) ) )
17 16 breq1i 
 |-  ( 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 )
18 3 14 17 3anbi123i 
 |-  ( ( 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 ) )
19 18 rexbii 
 |-  ( 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 ) )
20 f1oeq3 
 |-  ( A = B -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... m ) -1-1-onto-> B ) )
21 1 20 ax-mp 
 |-  ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... m ) -1-1-onto-> B )
22 2 cbvcsbv 
 |-  [_ ( f ` n ) / j ]_ C = [_ ( f ` n ) / k ]_ D
23 22 mpteq2i 
 |-  ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ D )
24 seqeq3 
 |-  ( ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) -> seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) = seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) )
25 23 24 ax-mp 
 |-  seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) = seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) )
26 25 fveq1i 
 |-  ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m )
27 26 eqeq2i 
 |-  ( x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ C ) ) ` m ) <-> x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ D ) ) ` m ) )
28 21 27 anbi12i 
 |-  ( ( 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 ) ) )
29 28 exbii 
 |-  ( 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 ) ) )
30 29 rexbii 
 |-  ( 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 ) ) )
31 19 30 orbi12i 
 |-  ( ( 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 ) ) ) )
32 31 iotabii 
 |-  ( 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 ) ) ) )
33 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 ) ) ) )
34 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 ) ) ) )
35 32 33 34 3eqtr4i 
 |-  prod_ j e. A C = prod_ k e. B D