Theorem addscllem1

Description: Lemma for addscl (future) Alternate expression for surreal addition. (Contributed by Scott Fenton, 23-Aug-2024)

	Ref	Expression
Assertion	addscllem1	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( ( +s " ( ( _L ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _L ` B ) ) ) ) |s ( ( +s " ( ( _R ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _R ` B ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		addsval	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { x | E. l e. ( _L ` A ) x = ( l +s B ) } u. { y | E. l e. ( _L ` B ) y = ( A +s l ) } ) |s ( { x | E. r e. ( _R ` A ) x = ( r +s B ) } u. { y | E. r e. ( _R ` B ) y = ( A +s r ) } ) ) )
2		addsfn	|- +s Fn ( No X. No )
3		leftssno	|- ( _L ` A ) C_ No
4	3	a1i	|- ( A e. No -> ( _L ` A ) C_ No )
5		snssi	|- ( B e. No -> { B } C_ No )
6		xpss12	|- ( ( ( _L ` A ) C_ No /\ { B } C_ No ) -> ( ( _L ` A ) X. { B } ) C_ ( No X. No ) )
7	4 5 6	syl2an	|- ( ( A e. No /\ B e. No ) -> ( ( _L ` A ) X. { B } ) C_ ( No X. No ) )
8		ovelimab	|- ( ( +s Fn ( No X. No ) /\ ( ( _L ` A ) X. { B } ) C_ ( No X. No ) ) -> ( x e. ( +s " ( ( _L ` A ) X. { B } ) ) <-> E. l e. ( _L ` A ) E. r e. { B } x = ( l +s r ) ) )
9	2 7 8	sylancr	|- ( ( A e. No /\ B e. No ) -> ( x e. ( +s " ( ( _L ` A ) X. { B } ) ) <-> E. l e. ( _L ` A ) E. r e. { B } x = ( l +s r ) ) )
10		oveq2	|- ( r = B -> ( l +s r ) = ( l +s B ) )
11	10	eqeq2d	|- ( r = B -> ( x = ( l +s r ) <-> x = ( l +s B ) ) )
12	11	rexsng	|- ( B e. No -> ( E. r e. { B } x = ( l +s r ) <-> x = ( l +s B ) ) )
13	12	adantl	|- ( ( A e. No /\ B e. No ) -> ( E. r e. { B } x = ( l +s r ) <-> x = ( l +s B ) ) )
14	13	rexbidv	|- ( ( A e. No /\ B e. No ) -> ( E. l e. ( _L ` A ) E. r e. { B } x = ( l +s r ) <-> E. l e. ( _L ` A ) x = ( l +s B ) ) )
15	9 14	bitrd	|- ( ( A e. No /\ B e. No ) -> ( x e. ( +s " ( ( _L ` A ) X. { B } ) ) <-> E. l e. ( _L ` A ) x = ( l +s B ) ) )
16	15	abbi2dv	|- ( ( A e. No /\ B e. No ) -> ( +s " ( ( _L ` A ) X. { B } ) ) = { x | E. l e. ( _L ` A ) x = ( l +s B ) } )
17		snssi	|- ( A e. No -> { A } C_ No )
18		leftssno	|- ( _L ` B ) C_ No
19	18	a1i	|- ( B e. No -> ( _L ` B ) C_ No )
20		xpss12	|- ( ( { A } C_ No /\ ( _L ` B ) C_ No ) -> ( { A } X. ( _L ` B ) ) C_ ( No X. No ) )
21	17 19 20	syl2an	|- ( ( A e. No /\ B e. No ) -> ( { A } X. ( _L ` B ) ) C_ ( No X. No ) )
22		ovelimab	|- ( ( +s Fn ( No X. No ) /\ ( { A } X. ( _L ` B ) ) C_ ( No X. No ) ) -> ( y e. ( +s " ( { A } X. ( _L ` B ) ) ) <-> E. r e. { A } E. l e. ( _L ` B ) y = ( r +s l ) ) )
23	2 21 22	sylancr	|- ( ( A e. No /\ B e. No ) -> ( y e. ( +s " ( { A } X. ( _L ` B ) ) ) <-> E. r e. { A } E. l e. ( _L ` B ) y = ( r +s l ) ) )
24		oveq1	|- ( r = A -> ( r +s l ) = ( A +s l ) )
25	24	eqeq2d	|- ( r = A -> ( y = ( r +s l ) <-> y = ( A +s l ) ) )
26	25	rexbidv	|- ( r = A -> ( E. l e. ( _L ` B ) y = ( r +s l ) <-> E. l e. ( _L ` B ) y = ( A +s l ) ) )
27	26	rexsng	|- ( A e. No -> ( E. r e. { A } E. l e. ( _L ` B ) y = ( r +s l ) <-> E. l e. ( _L ` B ) y = ( A +s l ) ) )
28	27	adantr	|- ( ( A e. No /\ B e. No ) -> ( E. r e. { A } E. l e. ( _L ` B ) y = ( r +s l ) <-> E. l e. ( _L ` B ) y = ( A +s l ) ) )
29	23 28	bitrd	|- ( ( A e. No /\ B e. No ) -> ( y e. ( +s " ( { A } X. ( _L ` B ) ) ) <-> E. l e. ( _L ` B ) y = ( A +s l ) ) )
30	29	abbi2dv	|- ( ( A e. No /\ B e. No ) -> ( +s " ( { A } X. ( _L ` B ) ) ) = { y | E. l e. ( _L ` B ) y = ( A +s l ) } )
31	16 30	uneq12d	|- ( ( A e. No /\ B e. No ) -> ( ( +s " ( ( _L ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _L ` B ) ) ) ) = ( { x | E. l e. ( _L ` A ) x = ( l +s B ) } u. { y | E. l e. ( _L ` B ) y = ( A +s l ) } ) )
32		rightssno	|- ( _R ` A ) C_ No
33	32	a1i	|- ( A e. No -> ( _R ` A ) C_ No )
34		xpss12	|- ( ( ( _R ` A ) C_ No /\ { B } C_ No ) -> ( ( _R ` A ) X. { B } ) C_ ( No X. No ) )
35	33 5 34	syl2an	|- ( ( A e. No /\ B e. No ) -> ( ( _R ` A ) X. { B } ) C_ ( No X. No ) )
36		ovelimab	|- ( ( +s Fn ( No X. No ) /\ ( ( _R ` A ) X. { B } ) C_ ( No X. No ) ) -> ( x e. ( +s " ( ( _R ` A ) X. { B } ) ) <-> E. r e. ( _R ` A ) E. l e. { B } x = ( r +s l ) ) )
37	2 35 36	sylancr	|- ( ( A e. No /\ B e. No ) -> ( x e. ( +s " ( ( _R ` A ) X. { B } ) ) <-> E. r e. ( _R ` A ) E. l e. { B } x = ( r +s l ) ) )
38		oveq2	|- ( l = B -> ( r +s l ) = ( r +s B ) )
39	38	eqeq2d	|- ( l = B -> ( x = ( r +s l ) <-> x = ( r +s B ) ) )
40	39	rexsng	|- ( B e. No -> ( E. l e. { B } x = ( r +s l ) <-> x = ( r +s B ) ) )
41	40	adantl	|- ( ( A e. No /\ B e. No ) -> ( E. l e. { B } x = ( r +s l ) <-> x = ( r +s B ) ) )
42	41	rexbidv	|- ( ( A e. No /\ B e. No ) -> ( E. r e. ( _R ` A ) E. l e. { B } x = ( r +s l ) <-> E. r e. ( _R ` A ) x = ( r +s B ) ) )
43	37 42	bitrd	|- ( ( A e. No /\ B e. No ) -> ( x e. ( +s " ( ( _R ` A ) X. { B } ) ) <-> E. r e. ( _R ` A ) x = ( r +s B ) ) )
44	43	abbi2dv	|- ( ( A e. No /\ B e. No ) -> ( +s " ( ( _R ` A ) X. { B } ) ) = { x | E. r e. ( _R ` A ) x = ( r +s B ) } )
45		rightssno	|- ( _R ` B ) C_ No
46	45	a1i	|- ( B e. No -> ( _R ` B ) C_ No )
47		xpss12	|- ( ( { A } C_ No /\ ( _R ` B ) C_ No ) -> ( { A } X. ( _R ` B ) ) C_ ( No X. No ) )
48	17 46 47	syl2an	|- ( ( A e. No /\ B e. No ) -> ( { A } X. ( _R ` B ) ) C_ ( No X. No ) )
49		ovelimab	|- ( ( +s Fn ( No X. No ) /\ ( { A } X. ( _R ` B ) ) C_ ( No X. No ) ) -> ( y e. ( +s " ( { A } X. ( _R ` B ) ) ) <-> E. l e. { A } E. r e. ( _R ` B ) y = ( l +s r ) ) )
50	2 48 49	sylancr	|- ( ( A e. No /\ B e. No ) -> ( y e. ( +s " ( { A } X. ( _R ` B ) ) ) <-> E. l e. { A } E. r e. ( _R ` B ) y = ( l +s r ) ) )
51		oveq1	|- ( l = A -> ( l +s r ) = ( A +s r ) )
52	51	eqeq2d	|- ( l = A -> ( y = ( l +s r ) <-> y = ( A +s r ) ) )
53	52	rexbidv	|- ( l = A -> ( E. r e. ( _R ` B ) y = ( l +s r ) <-> E. r e. ( _R ` B ) y = ( A +s r ) ) )
54	53	rexsng	|- ( A e. No -> ( E. l e. { A } E. r e. ( _R ` B ) y = ( l +s r ) <-> E. r e. ( _R ` B ) y = ( A +s r ) ) )
55	54	adantr	|- ( ( A e. No /\ B e. No ) -> ( E. l e. { A } E. r e. ( _R ` B ) y = ( l +s r ) <-> E. r e. ( _R ` B ) y = ( A +s r ) ) )
56	50 55	bitrd	|- ( ( A e. No /\ B e. No ) -> ( y e. ( +s " ( { A } X. ( _R ` B ) ) ) <-> E. r e. ( _R ` B ) y = ( A +s r ) ) )
57	56	abbi2dv	|- ( ( A e. No /\ B e. No ) -> ( +s " ( { A } X. ( _R ` B ) ) ) = { y | E. r e. ( _R ` B ) y = ( A +s r ) } )
58	44 57	uneq12d	|- ( ( A e. No /\ B e. No ) -> ( ( +s " ( ( _R ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _R ` B ) ) ) ) = ( { x | E. r e. ( _R ` A ) x = ( r +s B ) } u. { y | E. r e. ( _R ` B ) y = ( A +s r ) } ) )
59	31 58	oveq12d	|- ( ( A e. No /\ B e. No ) -> ( ( ( +s " ( ( _L ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _L ` B ) ) ) ) |s ( ( +s " ( ( _R ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _R ` B ) ) ) ) ) = ( ( { x | E. l e. ( _L ` A ) x = ( l +s B ) } u. { y | E. l e. ( _L ` B ) y = ( A +s l ) } ) |s ( { x | E. r e. ( _R ` A ) x = ( r +s B ) } u. { y | E. r e. ( _R ` B ) y = ( A +s r ) } ) ) )
60	1 59	eqtr4d	|- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( ( +s " ( ( _L ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _L ` B ) ) ) ) |s ( ( +s " ( ( _R ` A ) X. { B } ) ) u. ( +s " ( { A } X. ( _R ` B ) ) ) ) ) )