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 | p X q Y a = p s B + s A s q - s p s q = b | r X s Y b = r s B + s A s s - s r s s

Proof

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