Theorem negsval

Description: The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	negsval	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) = ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-negs	⊢ -us = norec ( ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) ) )
2	1	norecov	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) = ( 𝐴 ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) ) ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ) )
3		elex	⊢ ( 𝐴 ∈ No → 𝐴 ∈ V )
4		negsfn	⊢ -us Fn No
5		fnfun	⊢ ( -us Fn No → Fun -us )
6	4 5	ax-mp	⊢ Fun -us
7		fvex	⊢ ( L ‘ 𝐴 ) ∈ V
8		fvex	⊢ ( R ‘ 𝐴 ) ∈ V
9	7 8	unex	⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∈ V
10		resfunexg	⊢ ( ( Fun -us ∧ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ∈ V ) → ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ∈ V )
11	6 9 10	mp2an	⊢ ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ∈ V
12	11	a1i	⊢ ( 𝐴 ∈ No → ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ∈ V )
13		ovexd	⊢ ( 𝐴 ∈ No → ( ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( R ‘ 𝐴 ) ) |s ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( L ‘ 𝐴 ) ) ) ∈ V )
14		fveq2	⊢ ( 𝑥 = 𝐴 → ( R ‘ 𝑥 ) = ( R ‘ 𝐴 ) )
15	14	imaeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝑛 “ ( R ‘ 𝑥 ) ) = ( 𝑛 “ ( R ‘ 𝐴 ) ) )
16		fveq2	⊢ ( 𝑥 = 𝐴 → ( L ‘ 𝑥 ) = ( L ‘ 𝐴 ) )
17	16	imaeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝑛 “ ( L ‘ 𝑥 ) ) = ( 𝑛 “ ( L ‘ 𝐴 ) ) )
18	15 17	oveq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) = ( ( 𝑛 “ ( R ‘ 𝐴 ) ) |s ( 𝑛 “ ( L ‘ 𝐴 ) ) ) )
19		imaeq1	⊢ ( 𝑛 = ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) → ( 𝑛 “ ( R ‘ 𝐴 ) ) = ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( R ‘ 𝐴 ) ) )
20		imaeq1	⊢ ( 𝑛 = ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) → ( 𝑛 “ ( L ‘ 𝐴 ) ) = ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( L ‘ 𝐴 ) ) )
21	19 20	oveq12d	⊢ ( 𝑛 = ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) → ( ( 𝑛 “ ( R ‘ 𝐴 ) ) |s ( 𝑛 “ ( L ‘ 𝐴 ) ) ) = ( ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( R ‘ 𝐴 ) ) |s ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( L ‘ 𝐴 ) ) ) )
22		eqid	⊢ ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) )
23	18 21 22	ovmpog	⊢ ( ( 𝐴 ∈ V ∧ ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ∈ V ∧ ( ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( R ‘ 𝐴 ) ) |s ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( L ‘ 𝐴 ) ) ) ∈ V ) → ( 𝐴 ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) ) ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ) = ( ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( R ‘ 𝐴 ) ) |s ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( L ‘ 𝐴 ) ) ) )
24	3 12 13 23	syl3anc	⊢ ( 𝐴 ∈ No → ( 𝐴 ( 𝑥 ∈ V , 𝑛 ∈ V ↦ ( ( 𝑛 “ ( R ‘ 𝑥 ) ) |s ( 𝑛 “ ( L ‘ 𝑥 ) ) ) ) ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) ) = ( ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( R ‘ 𝐴 ) ) |s ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( L ‘ 𝐴 ) ) ) )
25		ssun2	⊢ ( R ‘ 𝐴 ) ⊆ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) )
26		resima2	⊢ ( ( R ‘ 𝐴 ) ⊆ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) → ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( R ‘ 𝐴 ) ) = ( -us “ ( R ‘ 𝐴 ) ) )
27	25 26	ax-mp	⊢ ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( R ‘ 𝐴 ) ) = ( -us “ ( R ‘ 𝐴 ) )
28		ssun1	⊢ ( L ‘ 𝐴 ) ⊆ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) )
29		resima2	⊢ ( ( L ‘ 𝐴 ) ⊆ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) → ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( L ‘ 𝐴 ) ) = ( -us “ ( L ‘ 𝐴 ) ) )
30	28 29	ax-mp	⊢ ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( L ‘ 𝐴 ) ) = ( -us “ ( L ‘ 𝐴 ) )
31	27 30	oveq12i	⊢ ( ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( R ‘ 𝐴 ) ) |s ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( L ‘ 𝐴 ) ) ) = ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) )
32	31	a1i	⊢ ( 𝐴 ∈ No → ( ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( R ‘ 𝐴 ) ) |s ( ( -us ↾ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) ) “ ( L ‘ 𝐴 ) ) ) = ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) )
33	2 24 32	3eqtrd	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) = ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) )