Theorem muls01

Description: Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	muls01	Could not format assertion : No typesetting found for |- ( A e. No -> ( A x.s 0s ) = 0s ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
2		mulsval	Could not format ( ( A e. No /\ 0s e. No ) -> ( A x.s 0s ) = ( ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( ( A e. No /\ 0s e. No ) -> ( A x.s 0s ) = ( ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
3	1 2	mpan2	Could not format ( A e. No -> ( A x.s 0s ) = ( ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( A e. No -> ( A x.s 0s ) = ( ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
4		rex0	Could not format -. E. q e. (/) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) : No typesetting found for |- -. E. q e. (/) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) with typecode |-
5		left0s	Could not format ( _Left ` 0s ) = (/) : No typesetting found for |- ( _Left ` 0s ) = (/) with typecode |-
6	5	rexeqi	Could not format ( E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> E. q e. (/) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) : No typesetting found for |- ( E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) <-> E. q e. (/) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) with typecode |-
7	4 6	mtbir	Could not format -. E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) : No typesetting found for |- -. E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) with typecode |-
8	7	a1i	Could not format ( p e. ( _Left ` A ) -> -. E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) : No typesetting found for |- ( p e. ( _Left ` A ) -> -. E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) ) with typecode |-
9	8	nrex	Could not format -. E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) : No typesetting found for |- -. E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) with typecode |-
10	9	abf	Could not format { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } = (/) : No typesetting found for |- { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } = (/) with typecode |-
11		rex0	Could not format -. E. s e. (/) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) : No typesetting found for |- -. E. s e. (/) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) with typecode |-
12		right0s	Could not format ( _Right ` 0s ) = (/) : No typesetting found for |- ( _Right ` 0s ) = (/) with typecode |-
13	12	rexeqi	Could not format ( E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) <-> E. s e. (/) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) : No typesetting found for |- ( E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) <-> E. s e. (/) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) with typecode |-
14	11 13	mtbir	Could not format -. E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) : No typesetting found for |- -. E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) with typecode |-
15	14	a1i	Could not format ( r e. ( _Right ` A ) -> -. E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) : No typesetting found for |- ( r e. ( _Right ` A ) -> -. E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) ) with typecode |-
16	15	nrex	Could not format -. E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) : No typesetting found for |- -. E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) with typecode |-
17	16	abf	Could not format { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } = (/) : No typesetting found for |- { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } = (/) with typecode |-
18	10 17	uneq12i	Could not format ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) = ( (/) u. (/) ) : No typesetting found for |- ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) = ( (/) u. (/) ) with typecode |-
19		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
20	18 19	eqtri	Could not format ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) = (/) : No typesetting found for |- ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) = (/) with typecode |-
21		rex0	Could not format -. E. u e. (/) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) : No typesetting found for |- -. E. u e. (/) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) with typecode |-
22	12	rexeqi	Could not format ( E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> E. u e. (/) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) : No typesetting found for |- ( E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) <-> E. u e. (/) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) with typecode |-
23	21 22	mtbir	Could not format -. E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) : No typesetting found for |- -. E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) with typecode |-
24	23	a1i	Could not format ( t e. ( _Left ` A ) -> -. E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) : No typesetting found for |- ( t e. ( _Left ` A ) -> -. E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) ) with typecode |-
25	24	nrex	Could not format -. E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) : No typesetting found for |- -. E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) with typecode |-
26	25	abf	Could not format { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } = (/) : No typesetting found for |- { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } = (/) with typecode |-
27		rex0	Could not format -. E. w e. (/) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) : No typesetting found for |- -. E. w e. (/) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) with typecode |-
28	5	rexeqi	Could not format ( E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> E. w e. (/) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) : No typesetting found for |- ( E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) <-> E. w e. (/) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) with typecode |-
29	27 28	mtbir	Could not format -. E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) : No typesetting found for |- -. E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) with typecode |-
30	29	a1i	Could not format ( v e. ( _Right ` A ) -> -. E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) : No typesetting found for |- ( v e. ( _Right ` A ) -> -. E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) ) with typecode |-
31	30	nrex	Could not format -. E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) : No typesetting found for |- -. E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) with typecode |-
32	31	abf	Could not format { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } = (/) : No typesetting found for |- { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } = (/) with typecode |-
33	26 32	uneq12i	Could not format ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) = ( (/) u. (/) ) : No typesetting found for |- ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) = ( (/) u. (/) ) with typecode |-
34	33 19	eqtri	Could not format ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) = (/) : No typesetting found for |- ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) = (/) with typecode |-
35	20 34	oveq12i	Could not format ( ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) = ( (/) |s (/) ) : No typesetting found for |- ( ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) = ( (/) |s (/) ) with typecode |-
36		df-0s	Could not format 0s = ( (/) |s (/) ) : No typesetting found for |- 0s = ( (/) |s (/) ) with typecode |-
37	35 36	eqtr4i	Could not format ( ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) = 0s : No typesetting found for |- ( ( { a | E. p e. ( _Left ` A ) E. q e. ( _Left ` 0s ) a = ( ( ( p x.s 0s ) +s ( A x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` A ) E. s e. ( _Right ` 0s ) b = ( ( ( r x.s 0s ) +s ( A x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` A ) E. u e. ( _Right ` 0s ) c = ( ( ( t x.s 0s ) +s ( A x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` A ) E. w e. ( _Left ` 0s ) d = ( ( ( v x.s 0s ) +s ( A x.s w ) ) -s ( v x.s w ) ) } ) ) = 0s with typecode |-
38	3 37	eqtrdi	Could not format ( A e. No -> ( A x.s 0s ) = 0s ) : No typesetting found for |- ( A e. No -> ( A x.s 0s ) = 0s ) with typecode |-