Metamath Proof Explorer

Theorem cbvprodv

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

Ref Expression
Hypothesis cbvprod.1 
|- ( j = k -> B = C )
Assertion cbvprodv 
|- prod_ j e. A B = prod_ k e. A C

Proof

Step Hyp Ref Expression
1 cbvprod.1 
 |-  ( j = k -> B = C )
2 biid 
 |-  ( A C_ ( ZZ>= ` m ) <-> A C_ ( ZZ>= ` m ) )
3 eleq1w 
 |-  ( j = k -> ( j e. A <-> k e. A ) )
4 3 1 ifbieq1d 
 |-  ( j = k -> if ( j e. A , B , 1 ) = if ( k e. A , C , 1 ) )
5 4 cbvmptv 
 |-  ( j e. ZZ |-> if ( j e. A , B , 1 ) ) = ( k e. ZZ |-> if ( k e. A , C , 1 ) )
6 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 ) ) ) )
7 5 6 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 ) ) )
8 7 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 )
9 8 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 ) )
10 9 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 ) )
11 10 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 ) )
12 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 ) ) ) )
13 5 12 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 ) ) )
14 13 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 )
15 2 11 14 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 ) )
16 15 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 ) )
17 1 cbvcsbv 
 |-  [_ ( f ` n ) / j ]_ B = [_ ( f ` n ) / k ]_ C
18 17 mpteq2i 
 |-  ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) = ( n e. NN |-> [_ ( f ` n ) / k ]_ C )
19 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 ) ) )
20 18 19 ax-mp 
 |-  seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) = seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) )
21 20 fveq1i 
 |-  ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / j ]_ B ) ) ` m ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m )
22 21 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 ) )
23 22 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 ) ) )
24 23 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 ) ) )
25 24 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 ) ) )
26 16 25 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 ) ) ) )
27 26 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 ) ) ) )
28 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 ) ) ) )
29 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 ) ) ) )
30 27 28 29 3eqtr4i 
 |-  prod_ j e. A B = prod_ k e. A C