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