Metamath Proof Explorer


Theorem prodeq2w

Description: Equality theorem for product, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Assertion prodeq2w k B = C k A B = k A C

Proof

Step Hyp Ref Expression
1 eqid =
2 ifeq1 B = C if k A B 1 = if k A C 1
3 2 alimi k B = C k if k A B 1 = if k A C 1
4 alral k if k A B 1 = if k A C 1 k if k A B 1 = if k A C 1
5 3 4 syl k B = C k if k A B 1 = if k A C 1
6 mpteq12 = k if k A B 1 = if k A C 1 k if k A B 1 = k if k A C 1
7 1 5 6 sylancr k B = C k if k A B 1 = k if k A C 1
8 7 seqeq3d k B = C seq n × k if k A B 1 = seq n × k if k A C 1
9 8 breq1d k B = C seq n × k if k A B 1 y seq n × k if k A C 1 y
10 9 anbi2d k B = C y 0 seq n × k if k A B 1 y y 0 seq n × k if k A C 1 y
11 10 exbidv k B = C y y 0 seq n × k if k A B 1 y y y 0 seq n × k if k A C 1 y
12 11 rexbidv k B = C n m y y 0 seq n × k if k A B 1 y n m y y 0 seq n × k if k A C 1 y
13 7 seqeq3d k B = C seq m × k if k A B 1 = seq m × k if k A C 1
14 13 breq1d k B = C seq m × k if k A B 1 x seq m × k if k A C 1 x
15 12 14 3anbi23d k B = C A m n m y y 0 seq n × k if k A B 1 y seq m × k if k A B 1 x A m n m y y 0 seq n × k if k A C 1 y seq m × k if k A C 1 x
16 15 rexbidv k B = C m A m n m y y 0 seq n × k if k A B 1 y seq m × k if k A B 1 x m A m n m y y 0 seq n × k if k A C 1 y seq m × k if k A C 1 x
17 csbeq2 k B = C f n / k B = f n / k C
18 17 mpteq2dv k B = C n f n / k B = n f n / k C
19 18 seqeq3d k B = C seq 1 × n f n / k B = seq 1 × n f n / k C
20 19 fveq1d k B = C seq 1 × n f n / k B m = seq 1 × n f n / k C m
21 20 eqeq2d k B = C x = seq 1 × n f n / k B m x = seq 1 × n f n / k C m
22 21 anbi2d k B = C f : 1 m 1-1 onto A x = seq 1 × n f n / k B m f : 1 m 1-1 onto A x = seq 1 × n f n / k C m
23 22 exbidv k B = C f f : 1 m 1-1 onto A x = seq 1 × n f n / k B m f f : 1 m 1-1 onto A x = seq 1 × n f n / k C m
24 23 rexbidv k B = C m f f : 1 m 1-1 onto A x = seq 1 × n f n / k B m m f f : 1 m 1-1 onto A x = seq 1 × n f n / k C m
25 16 24 orbi12d k B = C m A m n m y y 0 seq n × k if k A B 1 y seq m × k if k A B 1 x m f f : 1 m 1-1 onto A x = seq 1 × n f n / k B m m A m n m y y 0 seq n × k if k A C 1 y seq m × k if k A C 1 x m f f : 1 m 1-1 onto A x = seq 1 × n f n / k C m
26 25 iotabidv k B = C ι x | m A m n m y y 0 seq n × k if k A B 1 y seq m × k if k A B 1 x m f f : 1 m 1-1 onto A x = seq 1 × n f n / k B m = ι x | m A m n m y y 0 seq n × k if k A C 1 y seq m × k if k A C 1 x m f f : 1 m 1-1 onto A x = seq 1 × n f n / k C m
27 df-prod k A B = ι x | m A m n m y y 0 seq n × k if k A B 1 y seq m × k if k A B 1 x m f f : 1 m 1-1 onto A x = seq 1 × n f n / k B m
28 df-prod k A C = ι x | m A m n m y y 0 seq n × k if k A C 1 y seq m × k if k A C 1 x m f f : 1 m 1-1 onto A x = seq 1 × n f n / k C m
29 26 27 28 3eqtr4g k B = C k A B = k A C