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	Could not format assertion : No typesetting found for |- { 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 ) ) } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqeq1	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
2	1	2rexbidv	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
3		oveq1	Could not format ( p = r -> ( p x.s B ) = ( r x.s B ) ) : No typesetting found for |- ( p = r -> ( p x.s B ) = ( r x.s B ) ) with typecode |-
4	3	oveq1d	Could not format ( p = r -> ( ( p x.s B ) +s ( A x.s q ) ) = ( ( r x.s B ) +s ( A x.s q ) ) ) : No typesetting found for |- ( p = r -> ( ( p x.s B ) +s ( A x.s q ) ) = ( ( r x.s B ) +s ( A x.s q ) ) ) with typecode |-
5		oveq1	Could not format ( p = r -> ( p x.s q ) = ( r x.s q ) ) : No typesetting found for |- ( p = r -> ( p x.s q ) = ( r x.s q ) ) with typecode |-
6	4 5	oveq12d	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
7	6	eqeq2d	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
8		oveq2	Could not format ( q = s -> ( A x.s q ) = ( A x.s s ) ) : No typesetting found for |- ( q = s -> ( A x.s q ) = ( A x.s s ) ) with typecode |-
9	8	oveq2d	Could not format ( q = s -> ( ( r x.s B ) +s ( A x.s q ) ) = ( ( r x.s B ) +s ( A x.s s ) ) ) : No typesetting found for |- ( q = s -> ( ( r x.s B ) +s ( A x.s q ) ) = ( ( r x.s B ) +s ( A x.s s ) ) ) with typecode |-
10		oveq2	Could not format ( q = s -> ( r x.s q ) = ( r x.s s ) ) : No typesetting found for |- ( q = s -> ( r x.s q ) = ( r x.s s ) ) with typecode |-
11	9 10	oveq12d	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
12	11	eqeq2d	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
13	7 12	cbvrex2vw	Could not format ( 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 ) ) ) : No typesetting found for |- ( 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 ) ) ) with typecode |-
14	2 13	bitrdi	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
15	14	cbvabv	Could not format { 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 ) ) } : No typesetting found for |- { 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 ) ) } with typecode |-