# Metamath Proof Explorer

## Theorem cbvprod

Description: Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses cbvprod.1
`|- ( j = k -> B = C )`
cbvprod.2
`|- F/_ k A`
cbvprod.3
`|- F/_ j A`
cbvprod.4
`|- F/_ k B`
cbvprod.5
`|- F/_ j C`
Assertion cbvprod
`|- prod_ j e. A B = prod_ k e. A C`

### Proof

Step Hyp Ref Expression
1 cbvprod.1
` |-  ( j = k -> B = C )`
2 cbvprod.2
` |-  F/_ k A`
3 cbvprod.3
` |-  F/_ j A`
4 cbvprod.4
` |-  F/_ k B`
5 cbvprod.5
` |-  F/_ j C`
6 biid
` |-  ( A C_ ( ZZ>= ` m ) <-> A C_ ( ZZ>= ` m ) )`
7 2 nfcri
` |-  F/ k j e. A`
8 nfcv
` |-  F/_ k 1`
9 7 4 8 nfif
` |-  F/_ k if ( j e. A , B , 1 )`
10 3 nfcri
` |-  F/ j k e. A`
11 nfcv
` |-  F/_ j 1`
12 10 5 11 nfif
` |-  F/_ j if ( k e. A , C , 1 )`
13 eleq1w
` |-  ( j = k -> ( j e. A <-> k e. A ) )`
14 13 1 ifbieq1d
` |-  ( j = k -> if ( j e. A , B , 1 ) = if ( k e. A , C , 1 ) )`
15 9 12 14 cbvmpt
` |-  ( j e. ZZ |-> if ( j e. A , B , 1 ) ) = ( k e. ZZ |-> if ( k e. A , C , 1 ) )`
16 seqeq3
` |-  ( ( j e. ZZ |-> if ( j e. A , B , 1 ) ) = ( k e. ZZ |-> if ( k e. A , C , 1 ) ) -> seq n ( x. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) = seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) )`
17 15 16 ax-mp
` |-  seq n ( x. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) = seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) )`
18 17 breq1i
` |-  ( seq n ( x. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) ~~> y <-> seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> y )`
19 18 anbi2i
` |-  ( ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) ~~> y ) <-> ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> y ) )`
20 19 exbii
` |-  ( E. y ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) ~~> y ) <-> E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> y ) )`
21 20 rexbii
` |-  ( E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) ~~> y ) <-> E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> y ) )`
22 seqeq3
` |-  ( ( j e. ZZ |-> if ( j e. A , B , 1 ) ) = ( k e. ZZ |-> if ( k e. A , C , 1 ) ) -> seq m ( x. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) = seq m ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) )`
23 15 22 ax-mp
` |-  seq m ( x. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) = seq m ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) )`
24 23 breq1i
` |-  ( seq m ( x. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) ~~> x <-> seq m ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> x )`
25 6 21 24 3anbi123i
` |-  ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( j e. ZZ |-> if ( j 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 , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> x ) )`
26 25 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 , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( j e. ZZ |-> if ( j 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 , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> x ) )`
27 4 5 1 cbvcsbw
` |-  [_ ( f ` n ) / j ]_ B = [_ ( f ` n ) / k ]_ C`
28 27 mpteq2i
` |-  ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ C )`
29 seqeq3
` |-  ( ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) -> seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) = seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) )`
30 28 29 ax-mp
` |-  seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) = seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) )`
31 30 fveq1i
` |-  ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m )`
32 31 eqeq2i
` |-  ( x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) <-> x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) )`
33 32 anbi2i
` |-  ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) )`
34 33 exbii
` |-  ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) )`
35 34 rexbii
` |-  ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) )`
36 26 35 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 , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( j e. ZZ |-> if ( j 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 ) / j ]_ 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 , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k 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 ) / k ]_ C ) ) ` m ) ) ) )`
37 36 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 , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( j e. ZZ |-> if ( j 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 ) / j ]_ B ) ) ` m ) ) ) ) = ( 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 , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k 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 ) / k ]_ C ) ) ` m ) ) ) )`
38 df-prod
` |-  prod_ j 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. , ( j e. ZZ |-> if ( j e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( j e. ZZ |-> if ( j 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 ) / j ]_ B ) ) ` m ) ) ) )`
39 df-prod
` |-  prod_ k 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. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k 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 ) / k ]_ C ) ) ` m ) ) ) )`
40 37 38 39 3eqtr4i
` |-  prod_ j e. A B = prod_ k e. A C`