Theorem addsid1

Description: Surreal addition to zero is identity. Part of Theorem 3 of Conway p. 17. (Contributed by Scott Fenton, 20-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( a = b -> ( a +s 0s ) = ( b +s 0s ) ) : No typesetting found for |- ( a = b -> ( a +s 0s ) = ( b +s 0s ) ) with typecode |-
2		id	$$⊢a=b\to a=b$$
3	1 2	eqeq12d	Could not format ( a = b -> ( ( a +s 0s ) = a <-> ( b +s 0s ) = b ) ) : No typesetting found for |- ( a = b -> ( ( a +s 0s ) = a <-> ( b +s 0s ) = b ) ) with typecode |-
4		oveq1	Could not format ( a = A -> ( a +s 0s ) = ( A +s 0s ) ) : No typesetting found for |- ( a = A -> ( a +s 0s ) = ( A +s 0s ) ) with typecode |-
5		id	$$⊢a=A\to a=A$$
6	4 5	eqeq12d	Could not format ( a = A -> ( ( a +s 0s ) = a <-> ( A +s 0s ) = A ) ) : No typesetting found for |- ( a = A -> ( ( a +s 0s ) = a <-> ( A +s 0s ) = A ) ) with typecode |-
7		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
8		addsval	Could not format ( ( a e. No /\ 0s e. No ) -> ( a +s 0s ) = ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) ) : No typesetting found for |- ( ( a e. No /\ 0s e. No ) -> ( a +s 0s ) = ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) ) with typecode |-
9	7 8	mpan2	Could not format ( a e. No -> ( a +s 0s ) = ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) ) : No typesetting found for |- ( a e. No -> ( a +s 0s ) = ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) ) with typecode |-
10	9	adantr	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( a +s 0s ) = ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( a +s 0s ) = ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) ) with typecode |-
11		elun1	$$⊢y\in L\left(a\right)\to y\in \left(L\left(a\right)\cup R\left(a\right)\right)$$
12		simpr	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) with typecode |-
13		oveq1	Could not format ( b = y -> ( b +s 0s ) = ( y +s 0s ) ) : No typesetting found for |- ( b = y -> ( b +s 0s ) = ( y +s 0s ) ) with typecode |-
14		id	$$⊢b=y\to b=y$$
15	13 14	eqeq12d	Could not format ( b = y -> ( ( b +s 0s ) = b <-> ( y +s 0s ) = y ) ) : No typesetting found for |- ( b = y -> ( ( b +s 0s ) = b <-> ( y +s 0s ) = y ) ) with typecode |-
16	15	rspcva	Could not format ( ( y e. ( ( _L ` a ) u. ( _R ` a ) ) /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( y +s 0s ) = y ) : No typesetting found for |- ( ( y e. ( ( _L ` a ) u. ( _R ` a ) ) /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( y +s 0s ) = y ) with typecode |-
17	11 12 16	syl2anr	Could not format ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ y e. ( _L ` a ) ) -> ( y +s 0s ) = y ) : No typesetting found for |- ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ y e. ( _L ` a ) ) -> ( y +s 0s ) = y ) with typecode |-
18	17	eqeq2d	Could not format ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ y e. ( _L ` a ) ) -> ( x = ( y +s 0s ) <-> x = y ) ) : No typesetting found for |- ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ y e. ( _L ` a ) ) -> ( x = ( y +s 0s ) <-> x = y ) ) with typecode |-
19		equcom	$$⊢x=y\leftrightarrow y=x$$
20	18 19	bitrdi	Could not format ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ y e. ( _L ` a ) ) -> ( x = ( y +s 0s ) <-> y = x ) ) : No typesetting found for |- ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ y e. ( _L ` a ) ) -> ( x = ( y +s 0s ) <-> y = x ) ) with typecode |-
21	20	rexbidva	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. y e. ( _L ` a ) x = ( y +s 0s ) <-> E. y e. ( _L ` a ) y = x ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. y e. ( _L ` a ) x = ( y +s 0s ) <-> E. y e. ( _L ` a ) y = x ) ) with typecode |-
22		risset	$$⊢x\in L\left(a\right)\leftrightarrow \exists y\in L\left(a\right)y=x$$
23	21 22	bitr4di	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. y e. ( _L ` a ) x = ( y +s 0s ) <-> x e. ( _L ` a ) ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. y e. ( _L ` a ) x = ( y +s 0s ) <-> x e. ( _L ` a ) ) ) with typecode |-
24	23	abbi1dv	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } = ( _L ` a ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } = ( _L ` a ) ) with typecode |-
25		rex0	Could not format -. E. y e. (/) z = ( a +s y ) : No typesetting found for |- -. E. y e. (/) z = ( a +s y ) with typecode |-
26		left0s	Could not format ( _L ` 0s ) = (/) : No typesetting found for |- ( _L ` 0s ) = (/) with typecode |-
27	26	rexeqi	Could not format ( E. y e. ( _L ` 0s ) z = ( a +s y ) <-> E. y e. (/) z = ( a +s y ) ) : No typesetting found for |- ( E. y e. ( _L ` 0s ) z = ( a +s y ) <-> E. y e. (/) z = ( a +s y ) ) with typecode |-
28	25 27	mtbir	Could not format -. E. y e. ( _L ` 0s ) z = ( a +s y ) : No typesetting found for |- -. E. y e. ( _L ` 0s ) z = ( a +s y ) with typecode |-
29	28	abf	Could not format { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } = (/) : No typesetting found for |- { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } = (/) with typecode |-
30	29	a1i	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } = (/) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } = (/) ) with typecode |-
31	24 30	uneq12d	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) = ( ( _L ` a ) u. (/) ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) = ( ( _L ` a ) u. (/) ) ) with typecode |-
32		un0	$$⊢L\left(a\right)\cup \varnothing =L\left(a\right)$$
33	31 32	eqtrdi	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) = ( _L ` a ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) = ( _L ` a ) ) with typecode |-
34		elun2	$$⊢w\in R\left(a\right)\to w\in \left(L\left(a\right)\cup R\left(a\right)\right)$$
35		oveq1	Could not format ( b = w -> ( b +s 0s ) = ( w +s 0s ) ) : No typesetting found for |- ( b = w -> ( b +s 0s ) = ( w +s 0s ) ) with typecode |-
36		id	$$⊢b=w\to b=w$$
37	35 36	eqeq12d	Could not format ( b = w -> ( ( b +s 0s ) = b <-> ( w +s 0s ) = w ) ) : No typesetting found for |- ( b = w -> ( ( b +s 0s ) = b <-> ( w +s 0s ) = w ) ) with typecode |-
38	37	rspcva	Could not format ( ( w e. ( ( _L ` a ) u. ( _R ` a ) ) /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( w +s 0s ) = w ) : No typesetting found for |- ( ( w e. ( ( _L ` a ) u. ( _R ` a ) ) /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( w +s 0s ) = w ) with typecode |-
39	34 12 38	syl2anr	Could not format ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ w e. ( _R ` a ) ) -> ( w +s 0s ) = w ) : No typesetting found for |- ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ w e. ( _R ` a ) ) -> ( w +s 0s ) = w ) with typecode |-
40	39	eqeq2d	Could not format ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ w e. ( _R ` a ) ) -> ( x = ( w +s 0s ) <-> x = w ) ) : No typesetting found for |- ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ w e. ( _R ` a ) ) -> ( x = ( w +s 0s ) <-> x = w ) ) with typecode |-
41		equcom	$$⊢x=w\leftrightarrow w=x$$
42	40 41	bitrdi	Could not format ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ w e. ( _R ` a ) ) -> ( x = ( w +s 0s ) <-> w = x ) ) : No typesetting found for |- ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ w e. ( _R ` a ) ) -> ( x = ( w +s 0s ) <-> w = x ) ) with typecode |-
43	42	rexbidva	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. w e. ( _R ` a ) x = ( w +s 0s ) <-> E. w e. ( _R ` a ) w = x ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. w e. ( _R ` a ) x = ( w +s 0s ) <-> E. w e. ( _R ` a ) w = x ) ) with typecode |-
44		risset	$$⊢x\in R\left(a\right)\leftrightarrow \exists w\in R\left(a\right)w=x$$
45	43 44	bitr4di	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. w e. ( _R ` a ) x = ( w +s 0s ) <-> x e. ( _R ` a ) ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. w e. ( _R ` a ) x = ( w +s 0s ) <-> x e. ( _R ` a ) ) ) with typecode |-
46	45	abbi1dv	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } = ( _R ` a ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } = ( _R ` a ) ) with typecode |-
47		rex0	Could not format -. E. w e. (/) z = ( a +s w ) : No typesetting found for |- -. E. w e. (/) z = ( a +s w ) with typecode |-
48		right0s	Could not format ( _R ` 0s ) = (/) : No typesetting found for |- ( _R ` 0s ) = (/) with typecode |-
49	48	rexeqi	Could not format ( E. w e. ( _R ` 0s ) z = ( a +s w ) <-> E. w e. (/) z = ( a +s w ) ) : No typesetting found for |- ( E. w e. ( _R ` 0s ) z = ( a +s w ) <-> E. w e. (/) z = ( a +s w ) ) with typecode |-
50	47 49	mtbir	Could not format -. E. w e. ( _R ` 0s ) z = ( a +s w ) : No typesetting found for |- -. E. w e. ( _R ` 0s ) z = ( a +s w ) with typecode |-
51	50	abf	Could not format { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } = (/) : No typesetting found for |- { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } = (/) with typecode |-
52	51	a1i	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } = (/) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } = (/) ) with typecode |-
53	46 52	uneq12d	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) = ( ( _R ` a ) u. (/) ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) = ( ( _R ` a ) u. (/) ) ) with typecode |-
54		un0	$$⊢R\left(a\right)\cup \varnothing =R\left(a\right)$$
55	53 54	eqtrdi	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) = ( _R ` a ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) = ( _R ` a ) ) with typecode |-
56	33 55	oveq12d	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) = ( ( _L ` a ) |s ( _R ` a ) ) ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) = ( ( _L ` a ) |s ( _R ` a ) ) ) with typecode |-
57		lrcut	$$⊢a\in \mathrm{No}\to L\left(a\right){|}_{s}R\left(a\right)=a$$
58	57	adantr	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( ( _L ` a ) |s ( _R ` a ) ) = a ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( ( _L ` a ) |s ( _R ` a ) ) = a ) with typecode |-
59	10 56 58	3eqtrd	Could not format ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( a +s 0s ) = a ) : No typesetting found for |- ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( a +s 0s ) = a ) with typecode |-
60	59	ex	Could not format ( a e. No -> ( A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b -> ( a +s 0s ) = a ) ) : No typesetting found for |- ( a e. No -> ( A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b -> ( a +s 0s ) = a ) ) with typecode |-
61	3 6 60	noinds	Could not format ( A e. No -> ( A +s 0s ) = A ) : No typesetting found for |- ( A e. No -> ( A +s 0s ) = A ) with typecode |-