Metamath Proof Explorer

Theorem mulsval2lem

Description: Lemma for mulsval2 . Change bound variables in one of the cases. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Assertion mulsval2lem 
|- { a | E. p e. X E. q e. Y a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } = { b | E. r e. X E. s e. Y b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) }

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( a = b -> ( a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> b = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
2 1 2rexbidv 
 |-  ( a = b -> ( E. p e. X E. q e. Y a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> E. p e. X E. q e. Y b = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) )
3 oveq1 
 |-  ( p = r -> ( p x.s B ) = ( r x.s B ) )
4 3 oveq1d 
 |-  ( p = r -> ( ( p x.s B ) +s ( A x.s q ) ) = ( ( r x.s B ) +s ( A x.s q ) ) )
5 oveq1 
 |-  ( p = r -> ( p x.s q ) = ( r x.s q ) )
6 4 5 oveq12d 
 |-  ( p = r -> ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) = ( ( ( r x.s B ) +s ( A x.s q ) ) -s ( r x.s q ) ) )
7 6 eqeq2d 
 |-  ( p = r -> ( b = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> b = ( ( ( r x.s B ) +s ( A x.s q ) ) -s ( r x.s q ) ) ) )
8 oveq2 
 |-  ( q = s -> ( A x.s q ) = ( A x.s s ) )
9 8 oveq2d 
 |-  ( q = s -> ( ( r x.s B ) +s ( A x.s q ) ) = ( ( r x.s B ) +s ( A x.s s ) ) )
10 oveq2 
 |-  ( q = s -> ( r x.s q ) = ( r x.s s ) )
11 9 10 oveq12d 
 |-  ( q = s -> ( ( ( r x.s B ) +s ( A x.s q ) ) -s ( r x.s q ) ) = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
12 11 eqeq2d 
 |-  ( q = s -> ( b = ( ( ( r x.s B ) +s ( A x.s q ) ) -s ( r x.s q ) ) <-> b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
13 7 12 cbvrex2vw 
 |-  ( E. p e. X E. q e. Y b = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> E. r e. X E. s e. Y b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) )
14 2 13 bitrdi 
 |-  ( a = b -> ( E. p e. X E. q e. Y a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> E. r e. X E. s e. Y b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) )
15 14 cbvabv 
 |-  { a | E. p e. X E. q e. Y a = ( ( ( p x.s B ) +s ( A x.s q ) ) -s ( p x.s q ) ) } = { b | E. r e. X E. s e. Y b = ( ( ( r x.s B ) +s ( A x.s s ) ) -s ( r x.s s ) ) }