Metamath Proof Explorer

Theorem prodeq1i

Description: Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017) Remove DV conditions. (Revised by GG, 1-Sep-2025)

Ref Expression
Hypothesis prodeq1i.1 
|- A = B
Assertion prodeq1i 
|- prod_ k e. A C = prod_ k e. B C

Proof

Step Hyp Ref Expression
1 prodeq1i.1 
 |-  A = B
2 1 sseq1i 
 |-  ( A C_ ( ZZ>= ` m ) <-> B C_ ( ZZ>= ` m ) )
3 1 eleq2i 
 |-  ( k e. A <-> k e. B )
4 ifbi 
 |-  ( ( k e. A <-> k e. B ) -> if ( k e. A , C , 1 ) = if ( k e. B , C , 1 ) )
5 3 4 ax-mp 
 |-  if ( k e. A , C , 1 ) = if ( k e. B , C , 1 )
6 5 mpteq2i 
 |-  ( k e. ZZ |-> if ( k e. A , C , 1 ) ) = ( k e. ZZ |-> if ( k e. B , C , 1 ) )
7 seqeq3 
 |-  ( ( k e. ZZ |-> if ( k e. A , C , 1 ) ) = ( k e. ZZ |-> if ( k e. B , C , 1 ) ) -> seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) = seq n ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) )
8 6 7 ax-mp 
 |-  seq n ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) = seq n ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) )
9 8 breq1i 
 |-  ( 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 )
10 9 anbi2i 
 |-  ( ( 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 ) )
11 10 exbii 
 |-  ( 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 ) )
12 11 rexbii 
 |-  ( 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 ) )
13 seqeq3 
 |-  ( ( k e. ZZ |-> if ( k e. A , C , 1 ) ) = ( k e. ZZ |-> if ( k e. B , C , 1 ) ) -> seq m ( x. , ( k e. ZZ |-> if ( k e. A , C , 1 ) ) ) = seq m ( x. , ( k e. ZZ |-> if ( k e. B , C , 1 ) ) ) )
14 6 13 ax-mp 
 |-  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 breq1i 
 |-  ( 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 2 12 15 3anbi123i 
 |-  ( ( 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 rexbii 
 |-  ( 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 1 18 ax-mp 
 |-  ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... m ) -1-1-onto-> B )
20 19 anbi1i 
 |-  ( ( 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 ) ) )
21 20 exbii 
 |-  ( 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 ) ) )
22 21 rexbii 
 |-  ( 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 ) ) )
23 17 22 orbi12i 
 |-  ( ( 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 ) ) ) )
24 23 iotabii 
 |-  ( 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 ) ) ) )
25 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 ) ) ) )
26 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 ) ) ) )
27 24 25 26 3eqtr4i 
 |-  prod_ k e. A C = prod_ k e. B C