Theorem mulsrid

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

	Ref	Expression
Assertion	mulsrid	⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 1s ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑥 = 𝑥𝑂 → ( 𝑥 ·s 1s ) = ( 𝑥𝑂 ·s 1s ) )
2		id	⊢ ( 𝑥 = 𝑥𝑂 → 𝑥 = 𝑥𝑂 )
3	1 2	eqeq12d	⊢ ( 𝑥 = 𝑥𝑂 → ( ( 𝑥 ·s 1s ) = 𝑥 ↔ ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) )
4		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ·s 1s ) = ( 𝐴 ·s 1s ) )
5		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
6	4 5	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ·s 1s ) = 𝑥 ↔ ( 𝐴 ·s 1s ) = 𝐴 ) )
7		1sno	⊢ 1s ∈ No
8		mulsval	⊢ ( ( 𝑥 ∈ No ∧ 1s ∈ No ) → ( 𝑥 ·s 1s ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )
9	7 8	mpan2	⊢ ( 𝑥 ∈ No → ( 𝑥 ·s 1s ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )
10	9	adantr	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( 𝑥 ·s 1s ) = ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) )
11		elun1	⊢ ( 𝑝 ∈ ( L ‘ 𝑥 ) → 𝑝 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
12		oveq1	⊢ ( 𝑥𝑂 = 𝑝 → ( 𝑥𝑂 ·s 1s ) = ( 𝑝 ·s 1s ) )
13		id	⊢ ( 𝑥𝑂 = 𝑝 → 𝑥𝑂 = 𝑝 )
14	12 13	eqeq12d	⊢ ( 𝑥𝑂 = 𝑝 → ( ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ↔ ( 𝑝 ·s 1s ) = 𝑝 ) )
15	14	rspcva	⊢ ( ( 𝑝 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( 𝑝 ·s 1s ) = 𝑝 )
16	11 15	sylan	⊢ ( ( 𝑝 ∈ ( L ‘ 𝑥 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( 𝑝 ·s 1s ) = 𝑝 )
17	16	ancoms	⊢ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( 𝑝 ·s 1s ) = 𝑝 )
18	17	adantll	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( 𝑝 ·s 1s ) = 𝑝 )
19		muls01	⊢ ( 𝑥 ∈ No → ( 𝑥 ·s 0s ) = 0s )
20	19	adantr	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( 𝑥 ·s 0s ) = 0s )
21	20	adantr	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥 ·s 0s ) = 0s )
22	18 21	oveq12d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) = ( 𝑝 +s 0s ) )
23		leftssno	⊢ ( L ‘ 𝑥 ) ⊆ No
24	23	sseli	⊢ ( 𝑝 ∈ ( L ‘ 𝑥 ) → 𝑝 ∈ No )
25	24	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → 𝑝 ∈ No )
26	25	addsridd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( 𝑝 +s 0s ) = 𝑝 )
27	22 26	eqtrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) = 𝑝 )
28		muls01	⊢ ( 𝑝 ∈ No → ( 𝑝 ·s 0s ) = 0s )
29	25 28	syl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( 𝑝 ·s 0s ) = 0s )
30	27 29	oveq12d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑝 ·s 0s ) ) = ( 𝑝 -s 0s ) )
31		subsid1	⊢ ( 𝑝 ∈ No → ( 𝑝 -s 0s ) = 𝑝 )
32	25 31	syl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( 𝑝 -s 0s ) = 𝑝 )
33	30 32	eqtrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑝 ·s 0s ) ) = 𝑝 )
34	33	eqeq2d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑝 ·s 0s ) ) ↔ 𝑎 = 𝑝 ) )
35		equcom	⊢ ( 𝑎 = 𝑝 ↔ 𝑝 = 𝑎 )
36	34 35	bitrdi	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑝 ∈ ( L ‘ 𝑥 ) ) → ( 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑝 ·s 0s ) ) ↔ 𝑝 = 𝑎 ) )
37	36	rexbidva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( ∃ 𝑝 ∈ ( L ‘ 𝑥 ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑝 ·s 0s ) ) ↔ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) 𝑝 = 𝑎 ) )
38		left1s	⊢ ( L ‘ 1s ) = { 0s }
39	38	rexeqi	⊢ ( ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ ∃ 𝑞 ∈ { 0s } 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) )
40		0sno	⊢ 0s ∈ No
41	40	elexi	⊢ 0s ∈ V
42		oveq2	⊢ ( 𝑞 = 0s → ( 𝑥 ·s 𝑞 ) = ( 𝑥 ·s 0s ) )
43	42	oveq2d	⊢ ( 𝑞 = 0s → ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) = ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) )
44		oveq2	⊢ ( 𝑞 = 0s → ( 𝑝 ·s 𝑞 ) = ( 𝑝 ·s 0s ) )
45	43 44	oveq12d	⊢ ( 𝑞 = 0s → ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑝 ·s 0s ) ) )
46	45	eqeq2d	⊢ ( 𝑞 = 0s → ( 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑝 ·s 0s ) ) ) )
47	41 46	rexsn	⊢ ( ∃ 𝑞 ∈ { 0s } 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑝 ·s 0s ) ) )
48	39 47	bitri	⊢ ( ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑝 ·s 0s ) ) )
49	48	rexbii	⊢ ( ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑝 ·s 0s ) ) )
50		risset	⊢ ( 𝑎 ∈ ( L ‘ 𝑥 ) ↔ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) 𝑝 = 𝑎 )
51	37 49 50	3bitr4g	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) ↔ 𝑎 ∈ ( L ‘ 𝑥 ) ) )
52	51	eqabcdv	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } = ( L ‘ 𝑥 ) )
53		rex0	⊢ ¬ ∃ 𝑠 ∈ ∅ 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) )
54		right1s	⊢ ( R ‘ 1s ) = ∅
55	54	rexeqi	⊢ ( ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) ↔ ∃ 𝑠 ∈ ∅ 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
56	53 55	mtbir	⊢ ¬ ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) )
57	56	a1i	⊢ ( 𝑟 ∈ ( R ‘ 𝑥 ) → ¬ ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) )
58	57	nrex	⊢ ¬ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) )
59	58	abf	⊢ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } = ∅
60	59	a1i	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } = ∅ )
61	52 60	uneq12d	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) = ( ( L ‘ 𝑥 ) ∪ ∅ ) )
62		un0	⊢ ( ( L ‘ 𝑥 ) ∪ ∅ ) = ( L ‘ 𝑥 )
63	61 62	eqtrdi	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) = ( L ‘ 𝑥 ) )
64		rex0	⊢ ¬ ∃ 𝑢 ∈ ∅ 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) )
65	54	rexeqi	⊢ ( ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) ↔ ∃ 𝑢 ∈ ∅ 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
66	64 65	mtbir	⊢ ¬ ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) )
67	66	a1i	⊢ ( 𝑡 ∈ ( L ‘ 𝑥 ) → ¬ ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) )
68	67	nrex	⊢ ¬ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) )
69	68	abf	⊢ { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } = ∅
70	69	a1i	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } = ∅ )
71		elun2	⊢ ( 𝑣 ∈ ( R ‘ 𝑥 ) → 𝑣 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
72		oveq1	⊢ ( 𝑥𝑂 = 𝑣 → ( 𝑥𝑂 ·s 1s ) = ( 𝑣 ·s 1s ) )
73		id	⊢ ( 𝑥𝑂 = 𝑣 → 𝑥𝑂 = 𝑣 )
74	72 73	eqeq12d	⊢ ( 𝑥𝑂 = 𝑣 → ( ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ↔ ( 𝑣 ·s 1s ) = 𝑣 ) )
75	74	rspcva	⊢ ( ( 𝑣 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( 𝑣 ·s 1s ) = 𝑣 )
76	71 75	sylan	⊢ ( ( 𝑣 ∈ ( R ‘ 𝑥 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( 𝑣 ·s 1s ) = 𝑣 )
77	76	ancoms	⊢ ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( 𝑣 ·s 1s ) = 𝑣 )
78	77	adantll	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( 𝑣 ·s 1s ) = 𝑣 )
79	20	adantr	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥 ·s 0s ) = 0s )
80	78 79	oveq12d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 0s ) ) = ( 𝑣 +s 0s ) )
81		rightssno	⊢ ( R ‘ 𝑥 ) ⊆ No
82	81	sseli	⊢ ( 𝑣 ∈ ( R ‘ 𝑥 ) → 𝑣 ∈ No )
83	82	adantl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → 𝑣 ∈ No )
84	83	addsridd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( 𝑣 +s 0s ) = 𝑣 )
85	80 84	eqtrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 0s ) ) = 𝑣 )
86		muls01	⊢ ( 𝑣 ∈ No → ( 𝑣 ·s 0s ) = 0s )
87	83 86	syl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( 𝑣 ·s 0s ) = 0s )
88	85 87	oveq12d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑣 ·s 0s ) ) = ( 𝑣 -s 0s ) )
89		subsid1	⊢ ( 𝑣 ∈ No → ( 𝑣 -s 0s ) = 𝑣 )
90	83 89	syl	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( 𝑣 -s 0s ) = 𝑣 )
91	88 90	eqtrd	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑣 ·s 0s ) ) = 𝑣 )
92	91	eqeq2d	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑣 ·s 0s ) ) ↔ 𝑑 = 𝑣 ) )
93	38	rexeqi	⊢ ( ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ ∃ 𝑤 ∈ { 0s } 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) )
94		oveq2	⊢ ( 𝑤 = 0s → ( 𝑥 ·s 𝑤 ) = ( 𝑥 ·s 0s ) )
95	94	oveq2d	⊢ ( 𝑤 = 0s → ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) = ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 0s ) ) )
96		oveq2	⊢ ( 𝑤 = 0s → ( 𝑣 ·s 𝑤 ) = ( 𝑣 ·s 0s ) )
97	95 96	oveq12d	⊢ ( 𝑤 = 0s → ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑣 ·s 0s ) ) )
98	97	eqeq2d	⊢ ( 𝑤 = 0s → ( 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑣 ·s 0s ) ) ) )
99	41 98	rexsn	⊢ ( ∃ 𝑤 ∈ { 0s } 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑣 ·s 0s ) ) )
100	93 99	bitri	⊢ ( ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 0s ) ) -s ( 𝑣 ·s 0s ) ) )
101		equcom	⊢ ( 𝑣 = 𝑑 ↔ 𝑑 = 𝑣 )
102	92 100 101	3bitr4g	⊢ ( ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) ∧ 𝑣 ∈ ( R ‘ 𝑥 ) ) → ( ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ 𝑣 = 𝑑 ) )
103	102	rexbidva	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) 𝑣 = 𝑑 ) )
104		risset	⊢ ( 𝑑 ∈ ( R ‘ 𝑥 ) ↔ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) 𝑣 = 𝑑 )
105	103 104	bitr4di	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) ↔ 𝑑 ∈ ( R ‘ 𝑥 ) ) )
106	105	eqabcdv	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } = ( R ‘ 𝑥 ) )
107	70 106	uneq12d	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) = ( ∅ ∪ ( R ‘ 𝑥 ) ) )
108		0un	⊢ ( ∅ ∪ ( R ‘ 𝑥 ) ) = ( R ‘ 𝑥 )
109	107 108	eqtrdi	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) = ( R ‘ 𝑥 ) )
110	63 109	oveq12d	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 1s ) 𝑎 = ( ( ( 𝑝 ·s 1s ) +s ( 𝑥 ·s 𝑞 ) ) -s ( 𝑝 ·s 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 1s ) 𝑏 = ( ( ( 𝑟 ·s 1s ) +s ( 𝑥 ·s 𝑠 ) ) -s ( 𝑟 ·s 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 1s ) 𝑐 = ( ( ( 𝑡 ·s 1s ) +s ( 𝑥 ·s 𝑢 ) ) -s ( 𝑡 ·s 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 1s ) 𝑑 = ( ( ( 𝑣 ·s 1s ) +s ( 𝑥 ·s 𝑤 ) ) -s ( 𝑣 ·s 𝑤 ) ) } ) ) = ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) )
111		lrcut	⊢ ( 𝑥 ∈ No → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = 𝑥 )
112	111	adantr	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = 𝑥 )
113	10 110 112	3eqtrd	⊢ ( ( 𝑥 ∈ No ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 ) → ( 𝑥 ·s 1s ) = 𝑥 )
114	113	ex	⊢ ( 𝑥 ∈ No → ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥𝑂 ·s 1s ) = 𝑥𝑂 → ( 𝑥 ·s 1s ) = 𝑥 ) )
115	3 6 114	noinds	⊢ ( 𝐴 ∈ No → ( 𝐴 ·s 1s ) = 𝐴 )