Metamath Proof Explorer

Theorem prodeq1

Description: Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017)

Ref Expression
Assertion prodeq1 
|- ( A = B -> prod_ k e. A C = prod_ k e. B C )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( A = B -> ( A C_ ( ZZ>= ` m ) <-> B C_ ( ZZ>= ` m ) ) )
2 eleq2 
 |-  ( A = B -> ( k e. A <-> k e. B ) )
3 2 ifbid 
 |-  ( A = B -> if ( k e. A , C , 1 ) = if ( k e. B , C , 1 ) )
4 3 mpteq2dv 
 |-  ( A = B -> ( k e. ZZ |-> if ( k e. A , C , 1 ) ) = ( k e. ZZ |-> if ( k e. B , C , 1 ) ) )
5 4 seqeq3d 
 |-  ( A = B -> seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) = seq n ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) )
6 5 breq1d 
 |-  ( A = B -> ( seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> y <-> seq n ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) ~~> y ) )
7 6 anbi2d 
 |-  ( A = B -> ( ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> y ) <-> ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) ~~> y ) ) )
8 7 exbidv 
 |-  ( A = B -> ( E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> y ) <-> E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) ~~> y ) ) )
9 8 rexbidv 
 |-  ( A = B -> ( E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> y ) <-> E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) ~~> y ) ) )
10 4 seqeq3d 
 |-  ( A = B -> seq m ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) = seq m ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) )
11 10 breq1d 
 |-  ( A = B -> ( seq m ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) ~~> x <-> seq m ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) ~~> x ) )
12 1 9 11 3anbi123d 
 |-  ( A = B -> ( ( 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 ) <-> ( B C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) ~~> x ) ) )
13 12 rexbidv 
 |-  ( A = B -> ( 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. ZZ ( B C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) ~~> x ) ) )
14 f1oeq3 
 |-  ( A = B -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... m ) -1-1-onto-> B ) )
15 14 anbi1d 
 |-  ( A = B -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
16 15 exbidv 
 |-  ( A = B -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
17 16 rexbidv 
 |-  ( A = B -> ( 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 ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> B /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ C ) ) ` m ) ) ) )
18 13 17 orbi12d 
 |-  ( A = B -> ( ( 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 ) ) ) <-> ( 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 , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. B , C , 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 ]_ C ) ) ` m ) ) ) ) )
19 18 iotabidv 
 |-  ( 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 , 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 ) ) ) ) = ( 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 , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. B , C , 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 ]_ C ) ) ` m ) ) ) ) )
20 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 ) ) ) )
21 df-prod 
 |-  prod_ k e. B C = ( 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 , C , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. B , C , 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 ]_ C ) ) ` m ) ) ) )
22 19 20 21 3eqtr4g 
 |-  ( A = B -> prod_ k e. A C = prod_ k e. B C )