Metamath Proof Explorer


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 ‘ 𝐴 ) ) ) )