Theorem mulsrid

Description: Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	mulsrid	$$⊢A\in \mathrm{No}\to A{\cdot }_s{1}_s=A$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( x = xO -> ( x x.s 1s ) = ( xO x.s 1s ) ) : No typesetting found for |- ( x = xO -> ( x x.s 1s ) = ( xO x.s 1s ) ) with typecode |-
2		id	Could not format ( x = xO -> x = xO ) : No typesetting found for |- ( x = xO -> x = xO ) with typecode |-
3	1 2	eqeq12d	Could not format ( x = xO -> ( ( x x.s 1s ) = x <-> ( xO x.s 1s ) = xO ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s 1s ) = x <-> ( xO x.s 1s ) = xO ) ) with typecode |-
4		oveq1	$$⊢x=A\to x{\cdot }_s{1}_s=A{\cdot }_s{1}_s$$
5		id	$$⊢x=A\to x=A$$
6	4 5	eqeq12d	$$⊢x=A\to \left(x{\cdot }_s{1}_s=x\leftrightarrow A{\cdot }_s{1}_s=A\right)$$
7		1no	$$⊢1_s\in \mathrm{No}$$
8		mulsval	$$⊢\left(x\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to x{\cdot }_s{1}_s=\left(\left\{a|\exists p\in L\left(x\right)\exists q\in L\left(1_s\right)a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}\cup \left\{b|\exists r\in R\left(x\right)\exists s\in R\left(1_s\right)b=\left(\left(r{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}\right){|}_s\left(\left\{c|\exists t\in L\left(x\right)\exists u\in R\left(1_s\right)c=\left(\left(t{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}\cup \left\{d|\exists v\in R\left(x\right)\exists w\in L\left(1_s\right)d=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}\right)$$
9	7 8	mpan2	$$⊢x\in \mathrm{No}\to x{\cdot }_s{1}_s=\left(\left\{a|\exists p\in L\left(x\right)\exists q\in L\left(1_s\right)a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}\cup \left\{b|\exists r\in R\left(x\right)\exists s\in R\left(1_s\right)b=\left(\left(r{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}\right){|}_s\left(\left\{c|\exists t\in L\left(x\right)\exists u\in R\left(1_s\right)c=\left(\left(t{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}\cup \left\{d|\exists v\in R\left(x\right)\exists w\in L\left(1_s\right)d=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}\right)$$
10	9	adantr	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
11		elun1	$$⊢p\in L\left(x\right)\to p\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
12		oveq1	Could not format ( xO = p -> ( xO x.s 1s ) = ( p x.s 1s ) ) : No typesetting found for |- ( xO = p -> ( xO x.s 1s ) = ( p x.s 1s ) ) with typecode |-
13		id	Could not format ( xO = p -> xO = p ) : No typesetting found for |- ( xO = p -> xO = p ) with typecode |-
14	12 13	eqeq12d	Could not format ( xO = p -> ( ( xO x.s 1s ) = xO <-> ( p x.s 1s ) = p ) ) : No typesetting found for |- ( xO = p -> ( ( xO x.s 1s ) = xO <-> ( p x.s 1s ) = p ) ) with typecode |-
15	14	rspcva	Could not format ( ( p e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( p e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) with typecode |-
16	11 15	sylan	Could not format ( ( p e. ( _Left ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( p e. ( _Left ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) with typecode |-
17	16	ancoms	Could not format ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) with typecode |-
18	17	adantll	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) with typecode |-
19		muls01	$$⊢x\in \mathrm{No}\to x{\cdot }_s{0}_s=0_s$$
20	19	adantr	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 0s ) = 0s ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 0s ) = 0s ) with typecode |-
21	20	adantr	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( x x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( x x.s 0s ) = 0s ) with typecode |-
22	18 21	oveq12d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = ( p +s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = ( p +s 0s ) ) with typecode |-
23		leftno	$$⊢p\in L\left(x\right)\to p\in \mathrm{No}$$
24	23	adantl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> p e. No ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> p e. No ) with typecode |-
25	24	addsridd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p +s 0s ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p +s 0s ) = p ) with typecode |-
26	22 25	eqtrd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = p ) with typecode |-
27		muls01	$$⊢p\in \mathrm{No}\to p{\cdot }_s{0}_s=0_s$$
28	24 27	syl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 0s ) = 0s ) with typecode |-
29	26 28	oveq12d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = ( p -s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = ( p -s 0s ) ) with typecode |-
30		subsid1	$$⊢p\in \mathrm{No}\to p{-}_s{0}_s=p$$
31	24 30	syl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p -s 0s ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p -s 0s ) = p ) with typecode |-
32	29 31	eqtrd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = p ) with typecode |-
33	32	eqeq2d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> a = p ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> a = p ) ) with typecode |-
34		equcom	$$⊢a=p\leftrightarrow p=a$$
35	33 34	bitrdi	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> p = a ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> p = a ) ) with typecode |-
36	35	rexbidva	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> E. p e. ( _Left ` x ) p = a ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> E. p e. ( _Left ` x ) p = a ) ) with typecode |-
37		left1s	$$⊢L\left(1_s\right)=\left\{0_s\right\}$$
38	37	rexeqi	$$⊢\exists q\in L\left(1_s\right)a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\leftrightarrow \exists q\in \left\{0_s\right\}a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)$$
39		0no	$$⊢0_s\in \mathrm{No}$$
40	39	elexi	$$⊢0_s\in \mathrm{V}$$
41		oveq2	$$⊢q=0_s\to x{\cdot }_{s}q=x{\cdot }_s{0}_s$$
42	41	oveq2d	$$⊢q=0_s\to \left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}q\right)=\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)$$
43		oveq2	$$⊢q=0_s\to p{\cdot }_{s}q=p{\cdot }_s{0}_s$$
44	42 43	oveq12d	$$⊢q=0_s\to \left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)\right){-}_s\left(p{\cdot }_s{0}_s\right)$$
45	44	eqeq2d	$$⊢q=0_s\to \left(a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\leftrightarrow a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)\right){-}_s\left(p{\cdot }_s{0}_s\right)\right)$$
46	40 45	rexsn	$$⊢\exists q\in \left\{0_s\right\}a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\leftrightarrow a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)\right){-}_s\left(p{\cdot }_s{0}_s\right)$$
47	38 46	bitri	$$⊢\exists q\in L\left(1_s\right)a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\leftrightarrow a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)\right){-}_s\left(p{\cdot }_s{0}_s\right)$$
48	47	rexbii	$$⊢\exists p\in L\left(x\right)\exists q\in L\left(1_s\right)a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\leftrightarrow \exists p\in L\left(x\right)a=\left(\left(p{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)\right){-}_s\left(p{\cdot }_s{0}_s\right)$$
49		risset	$$⊢a\in L\left(x\right)\leftrightarrow \exists p\in L\left(x\right)p=a$$
50	36 48 49	3bitr4g	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a e. ( _Left ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a e. ( _Left ` x ) ) ) with typecode |-
51	50	eqabcdv	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = ( _Left ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = ( _Left ` x ) ) with typecode |-
52		rex0	$$⊢\neg \exists s\in \varnothing b=\left(\left(r{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)$$
53		right1s	$$⊢R\left(1_s\right)=\varnothing$$
54	53	rexeqi	$$⊢\exists s\in R\left(1_s\right)b=\left(\left(r{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\leftrightarrow \exists s\in \varnothing b=\left(\left(r{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)$$
55	52 54	mtbir	$$⊢\neg \exists s\in R\left(1_s\right)b=\left(\left(r{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)$$
56	55	a1i	$$⊢r\in R\left(x\right)\to \neg \exists s\in R\left(1_s\right)b=\left(\left(r{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)$$
57	56	nrex	$$⊢\neg \exists r\in R\left(x\right)\exists s\in R\left(1_s\right)b=\left(\left(r{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)$$
58	57	abf	$$⊢\left\{b|\exists r\in R\left(x\right)\exists s\in R\left(1_s\right)b=\left(\left(r{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}=\varnothing$$
59	58	a1i	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = (/) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = (/) ) with typecode |-
60	51 59	uneq12d	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( ( _Left ` x ) u. (/) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( ( _Left ` x ) u. (/) ) ) with typecode |-
61		un0	$$⊢L\left(x\right)\cup \varnothing =L\left(x\right)$$
62	60 61	eqtrdi	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( _Left ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( _Left ` x ) ) with typecode |-
63		rex0	$$⊢\neg \exists u\in \varnothing c=\left(\left(t{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)$$
64	53	rexeqi	$$⊢\exists u\in R\left(1_s\right)c=\left(\left(t{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\leftrightarrow \exists u\in \varnothing c=\left(\left(t{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)$$
65	63 64	mtbir	$$⊢\neg \exists u\in R\left(1_s\right)c=\left(\left(t{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)$$
66	65	a1i	$$⊢t\in L\left(x\right)\to \neg \exists u\in R\left(1_s\right)c=\left(\left(t{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)$$
67	66	nrex	$$⊢\neg \exists t\in L\left(x\right)\exists u\in R\left(1_s\right)c=\left(\left(t{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)$$
68	67	abf	$$⊢\left\{c|\exists t\in L\left(x\right)\exists u\in R\left(1_s\right)c=\left(\left(t{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}=\varnothing$$
69	68	a1i	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = (/) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = (/) ) with typecode |-
70		elun2	$$⊢v\in R\left(x\right)\to v\in \left(L\left(x\right)\cup R\left(x\right)\right)$$
71		oveq1	Could not format ( xO = v -> ( xO x.s 1s ) = ( v x.s 1s ) ) : No typesetting found for |- ( xO = v -> ( xO x.s 1s ) = ( v x.s 1s ) ) with typecode |-
72		id	Could not format ( xO = v -> xO = v ) : No typesetting found for |- ( xO = v -> xO = v ) with typecode |-
73	71 72	eqeq12d	Could not format ( xO = v -> ( ( xO x.s 1s ) = xO <-> ( v x.s 1s ) = v ) ) : No typesetting found for |- ( xO = v -> ( ( xO x.s 1s ) = xO <-> ( v x.s 1s ) = v ) ) with typecode |-
74	73	rspcva	Could not format ( ( v e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( v e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) with typecode |-
75	70 74	sylan	Could not format ( ( v e. ( _Right ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( v e. ( _Right ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) with typecode |-
76	75	ancoms	Could not format ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) with typecode |-
77	76	adantll	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) with typecode |-
78	20	adantr	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( x x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( x x.s 0s ) = 0s ) with typecode |-
79	77 78	oveq12d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = ( v +s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = ( v +s 0s ) ) with typecode |-
80		rightno	$$⊢v\in R\left(x\right)\to v\in \mathrm{No}$$
81	80	adantl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> v e. No ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> v e. No ) with typecode |-
82	81	addsridd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v +s 0s ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v +s 0s ) = v ) with typecode |-
83	79 82	eqtrd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = v ) with typecode |-
84		muls01	$$⊢v\in \mathrm{No}\to v{\cdot }_s{0}_s=0_s$$
85	81 84	syl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 0s ) = 0s ) with typecode |-
86	83 85	oveq12d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = ( v -s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = ( v -s 0s ) ) with typecode |-
87		subsid1	$$⊢v\in \mathrm{No}\to v{-}_s{0}_s=v$$
88	81 87	syl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v -s 0s ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v -s 0s ) = v ) with typecode |-
89	86 88	eqtrd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = v ) with typecode |-
90	89	eqeq2d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) <-> d = v ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) <-> d = v ) ) with typecode |-
91	37	rexeqi	$$⊢\exists w\in L\left(1_s\right)d=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\leftrightarrow \exists w\in \left\{0_s\right\}d=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)$$
92		oveq2	$$⊢w=0_s\to x{\cdot }_{s}w=x{\cdot }_s{0}_s$$
93	92	oveq2d	$$⊢w=0_s\to \left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}w\right)=\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)$$
94		oveq2	$$⊢w=0_s\to v{\cdot }_{s}w=v{\cdot }_s{0}_s$$
95	93 94	oveq12d	$$⊢w=0_s\to \left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)\right){-}_s\left(v{\cdot }_s{0}_s\right)$$
96	95	eqeq2d	$$⊢w=0_s\to \left(d=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\leftrightarrow d=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)\right){-}_s\left(v{\cdot }_s{0}_s\right)\right)$$
97	40 96	rexsn	$$⊢\exists w\in \left\{0_s\right\}d=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\leftrightarrow d=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)\right){-}_s\left(v{\cdot }_s{0}_s\right)$$
98	91 97	bitri	$$⊢\exists w\in L\left(1_s\right)d=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\leftrightarrow d=\left(\left(v{\cdot }_s{1}_s\right){+}_s\left(x{\cdot }_s{0}_s\right)\right){-}_s\left(v{\cdot }_s{0}_s\right)$$
99		equcom	$$⊢v=d\leftrightarrow d=v$$
100	90 98 99	3bitr4g	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> v = d ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> v = d ) ) with typecode |-
101	100	rexbidva	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) v = d ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) v = d ) ) with typecode |-
102		risset	$$⊢d\in R\left(x\right)\leftrightarrow \exists v\in R\left(x\right)v=d$$
103	101 102	bitr4di	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d e. ( _Right ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d e. ( _Right ` x ) ) ) with typecode |-
104	103	eqabcdv	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = ( _Right ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = ( _Right ` x ) ) with typecode |-
105	69 104	uneq12d	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( (/) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( (/) u. ( _Right ` x ) ) ) with typecode |-
106		0un	$$⊢\varnothing \cup R\left(x\right)=R\left(x\right)$$
107	105 106	eqtrdi	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( _Right ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( _Right ` x ) ) with typecode |-
108	62 107	oveq12d	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( _Left ` x ) |s ( _Right ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( _Left ` x ) |s ( _Right ` x ) ) ) with typecode |-
109		lrcut	$$⊢x\in \mathrm{No}\to L\left(x\right){|}_{s}R\left(x\right)=x$$
110	109	adantr	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) with typecode |-
111	10 108 110	3eqtrd	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = x ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = x ) with typecode |-
112	111	ex	Could not format ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO -> ( x x.s 1s ) = x ) ) : No typesetting found for |- ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO -> ( x x.s 1s ) = x ) ) with typecode |-
113	3 6 112	noinds	$$⊢A\in \mathrm{No}\to A{\cdot }_s{1}_s=A$$