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