Metamath Proof Explorer

Theorem prodeq1f

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

Ref Expression
Hypotheses prodeq1f.1 
|- F/_ k A
prodeq1f.2 
|- F/_ k B
Assertion prodeq1f 
|- ( A = B -> prod_ k e. A C = prod_ k e. B C )

Proof

Step Hyp Ref Expression
1 prodeq1f.1 
 |-  F/_ k A
2 prodeq1f.2 
 |-  F/_ k B
3 sseq1 
 |-  ( A = B -> ( A C_ ( ZZ>= ` m ) <-> B C_ ( ZZ>= ` m ) ) )
4 1 2 nfeq 
 |-  F/ k A = B
5 eleq2 
 |-  ( A = B -> ( k e. A <-> k e. B ) )
6 5 ifbid 
 |-  ( A = B -> if ( k e. A , C , 1 ) = if ( k e. B , C , 1 ) )
7 6 adantr 
 |-  ( ( A = B /\ k e. ZZ ) -> if ( k e. A , C , 1 ) = if ( k e. B , C , 1 ) )
8 4 7 mpteq2da 
 |-  ( A = B -> ( k e. ZZ |-> if ( k e. A , C , 1 ) ) = ( k e. ZZ |-> if ( k e. B , C , 1 ) ) )
9 8 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 ) ) ) )
10 9 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 ) )
11 10 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 ) ) )
12 11 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 ) ) )
13 12 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 ) ) )
14 8 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 ) ) ) )
15 14 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 ) )
16 3 13 15 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 ) ) )
17 16 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 ) ) )
18 f1oeq3 
 |-  ( A = B -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... m ) -1-1-onto-> B ) )
19 18 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 ) ) ) )
20 19 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 ) ) ) )
21 20 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 ) ) ) )
22 17 21 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 ) ) ) ) )
23 22 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 ) ) ) ) )
24 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 ) ) ) )
25 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 ) ) ) )
26 23 24 25 3eqtr4g 
 |-  ( A = B -> prod_ k e. A C = prod_ k e. B C )