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