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	⊢ { 𝑎 ∣ ∃ 𝑝 ∈ 𝑋 ∃ 𝑞 ∈ 𝑌 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } = { 𝑏 ∣ ∃ 𝑟 ∈ 𝑋 ∃ 𝑠 ∈ 𝑌 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) }

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ 𝑏 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) )
2	1	2rexbidv	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑝 ∈ 𝑋 ∃ 𝑞 ∈ 𝑌 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ ∃ 𝑝 ∈ 𝑋 ∃ 𝑞 ∈ 𝑌 𝑏 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ) )
3		oveq1	⊢ ( 𝑝 = 𝑟 → ( 𝑝 ·s 𝐵 ) = ( 𝑟 ·s 𝐵 ) )
4	3	oveq1d	⊢ ( 𝑝 = 𝑟 → ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) = ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) )
5		oveq1	⊢ ( 𝑝 = 𝑟 → ( 𝑝 ·s 𝑞 ) = ( 𝑟 ·s 𝑞 ) )
6	4 5	oveq12d	⊢ ( 𝑝 = 𝑟 → ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑟 ·s 𝑞 ) ) )
7	6	eqeq2d	⊢ ( 𝑝 = 𝑟 → ( 𝑏 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑟 ·s 𝑞 ) ) ) )
8		oveq2	⊢ ( 𝑞 = 𝑠 → ( 𝐴 ·s 𝑞 ) = ( 𝐴 ·s 𝑠 ) )
9	8	oveq2d	⊢ ( 𝑞 = 𝑠 → ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) = ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) )
10		oveq2	⊢ ( 𝑞 = 𝑠 → ( 𝑟 ·s 𝑞 ) = ( 𝑟 ·s 𝑠 ) )
11	9 10	oveq12d	⊢ ( 𝑞 = 𝑠 → ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑟 ·s 𝑞 ) ) = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
12	11	eqeq2d	⊢ ( 𝑞 = 𝑠 → ( 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑟 ·s 𝑞 ) ) ↔ 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
13	7 12	cbvrex2vw	⊢ ( ∃ 𝑝 ∈ 𝑋 ∃ 𝑞 ∈ 𝑌 𝑏 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ ∃ 𝑟 ∈ 𝑋 ∃ 𝑠 ∈ 𝑌 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
14	2 13	bitrdi	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑝 ∈ 𝑋 ∃ 𝑞 ∈ 𝑌 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ ∃ 𝑟 ∈ 𝑋 ∃ 𝑠 ∈ 𝑌 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ) )
15	14	cbvabv	⊢ { 𝑎 ∣ ∃ 𝑝 ∈ 𝑋 ∃ 𝑞 ∈ 𝑌 𝑎 = ( ( ( 𝑝 ·s 𝐵 ) +s ( 𝐴 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } = { 𝑏 ∣ ∃ 𝑟 ∈ 𝑋 ∃ 𝑠 ∈ 𝑌 𝑏 = ( ( ( 𝑟 ·s 𝐵 ) +s ( 𝐴 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) }