Metamath Proof Explorer

Theorem addsrid

Description: Surreal addition to zero is identity. Part of Theorem 3 of Conway p. 17. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion addsrid ⊢ A ∈ No → A + s 0 s = A

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ a = b → a + s 0 s = b + s 0 s
2 id ⊢ a = b → a = b
3 1 2 eqeq12d ⊢ a = b → a + s 0 s = a ↔ b + s 0 s = b
4 oveq1 ⊢ a = A → a + s 0 s = A + s 0 s
5 id ⊢ a = A → a = A
6 4 5 eqeq12d ⊢ a = A → a + s 0 s = a ↔ A + s 0 s = A
7 0no ⊢ 0 s ∈ No
8 addsval ⊢ a ∈ No ∧ 0 s ∈ No → a + s 0 s = x | ∃ y ∈ L ⁡ a x = y + s 0 s ∪ z | ∃ y ∈ L ⁡ 0 s z = a + s y | s x | ∃ w ∈ R ⁡ a x = w + s 0 s ∪ z | ∃ w ∈ R ⁡ 0 s z = a + s w
9 7 8 mpan2 ⊢ a ∈ No → a + s 0 s = x | ∃ y ∈ L ⁡ a x = y + s 0 s ∪ z | ∃ y ∈ L ⁡ 0 s z = a + s y | s x | ∃ w ∈ R ⁡ a x = w + s 0 s ∪ z | ∃ w ∈ R ⁡ 0 s z = a + s w
10 9 adantr ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → a + s 0 s = x | ∃ y ∈ L ⁡ a x = y + s 0 s ∪ z | ∃ y ∈ L ⁡ 0 s z = a + s y | s x | ∃ w ∈ R ⁡ a x = w + s 0 s ∪ z | ∃ w ∈ R ⁡ 0 s z = a + s w
11 elun1 ⊢ y ∈ L ⁡ a → y ∈ L ⁡ a ∪ R ⁡ a
12 simpr ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b
13 oveq1 ⊢ b = y → b + s 0 s = y + s 0 s
14 id ⊢ b = y → b = y
15 13 14 eqeq12d ⊢ b = y → b + s 0 s = b ↔ y + s 0 s = y
16 15 rspcva ⊢ y ∈ L ⁡ a ∪ R ⁡ a ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → y + s 0 s = y
17 11 12 16 syl2anr ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b ∧ y ∈ L ⁡ a → y + s 0 s = y
18 17 eqeq2d ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b ∧ y ∈ L ⁡ a → x = y + s 0 s ↔ x = y
19 equcom ⊢ x = y ↔ y = x
20 18 19 bitrdi ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b ∧ y ∈ L ⁡ a → x = y + s 0 s ↔ y = x
21 20 rexbidva ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → ∃ y ∈ L ⁡ a x = y + s 0 s ↔ ∃ y ∈ L ⁡ a y = x
22 risset ⊢ x ∈ L ⁡ a ↔ ∃ y ∈ L ⁡ a y = x
23 21 22 bitr4di ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → ∃ y ∈ L ⁡ a x = y + s 0 s ↔ x ∈ L ⁡ a
24 23 eqabcdv ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → x | ∃ y ∈ L ⁡ a x = y + s 0 s = L ⁡ a
25 rex0 ⊢ ¬ ∃ y ∈ ∅ z = a + s y
26 left0s ⊢ L ⁡ 0 s = ∅
27 26 rexeqi ⊢ ∃ y ∈ L ⁡ 0 s z = a + s y ↔ ∃ y ∈ ∅ z = a + s y
28 25 27 mtbir ⊢ ¬ ∃ y ∈ L ⁡ 0 s z = a + s y
29 28 abf ⊢ z | ∃ y ∈ L ⁡ 0 s z = a + s y = ∅
30 29 a1i ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → z | ∃ y ∈ L ⁡ 0 s z = a + s y = ∅
31 24 30 uneq12d ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → x | ∃ y ∈ L ⁡ a x = y + s 0 s ∪ z | ∃ y ∈ L ⁡ 0 s z = a + s y = L ⁡ a ∪ ∅
32 un0 ⊢ L ⁡ a ∪ ∅ = L ⁡ a
33 31 32 eqtrdi ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → x | ∃ y ∈ L ⁡ a x = y + s 0 s ∪ z | ∃ y ∈ L ⁡ 0 s z = a + s y = L ⁡ a
34 elun2 ⊢ w ∈ R ⁡ a → w ∈ L ⁡ a ∪ R ⁡ a
35 oveq1 ⊢ b = w → b + s 0 s = w + s 0 s
36 id ⊢ b = w → b = w
37 35 36 eqeq12d ⊢ b = w → b + s 0 s = b ↔ w + s 0 s = w
38 37 rspcva ⊢ w ∈ L ⁡ a ∪ R ⁡ a ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → w + s 0 s = w
39 34 12 38 syl2anr ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b ∧ w ∈ R ⁡ a → w + s 0 s = w
40 39 eqeq2d ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b ∧ w ∈ R ⁡ a → x = w + s 0 s ↔ x = w
41 equcom ⊢ x = w ↔ w = x
42 40 41 bitrdi ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b ∧ w ∈ R ⁡ a → x = w + s 0 s ↔ w = x
43 42 rexbidva ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → ∃ w ∈ R ⁡ a x = w + s 0 s ↔ ∃ w ∈ R ⁡ a w = x
44 risset ⊢ x ∈ R ⁡ a ↔ ∃ w ∈ R ⁡ a w = x
45 43 44 bitr4di ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → ∃ w ∈ R ⁡ a x = w + s 0 s ↔ x ∈ R ⁡ a
46 45 eqabcdv ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → x | ∃ w ∈ R ⁡ a x = w + s 0 s = R ⁡ a
47 rex0 ⊢ ¬ ∃ w ∈ ∅ z = a + s w
48 right0s ⊢ R ⁡ 0 s = ∅
49 48 rexeqi ⊢ ∃ w ∈ R ⁡ 0 s z = a + s w ↔ ∃ w ∈ ∅ z = a + s w
50 47 49 mtbir ⊢ ¬ ∃ w ∈ R ⁡ 0 s z = a + s w
51 50 abf ⊢ z | ∃ w ∈ R ⁡ 0 s z = a + s w = ∅
52 51 a1i ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → z | ∃ w ∈ R ⁡ 0 s z = a + s w = ∅
53 46 52 uneq12d ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → x | ∃ w ∈ R ⁡ a x = w + s 0 s ∪ z | ∃ w ∈ R ⁡ 0 s z = a + s w = R ⁡ a ∪ ∅
54 un0 ⊢ R ⁡ a ∪ ∅ = R ⁡ a
55 53 54 eqtrdi ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → x | ∃ w ∈ R ⁡ a x = w + s 0 s ∪ z | ∃ w ∈ R ⁡ 0 s z = a + s w = R ⁡ a
56 33 55 oveq12d ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → x | ∃ y ∈ L ⁡ a x = y + s 0 s ∪ z | ∃ y ∈ L ⁡ 0 s z = a + s y | s x | ∃ w ∈ R ⁡ a x = w + s 0 s ∪ z | ∃ w ∈ R ⁡ 0 s z = a + s w = L ⁡ a | s R ⁡ a
57 lrcut ⊢ a ∈ No → L ⁡ a | s R ⁡ a = a
58 57 adantr ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → L ⁡ a | s R ⁡ a = a
59 10 56 58 3eqtrd ⊢ a ∈ No ∧ ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → a + s 0 s = a
60 59 ex ⊢ a ∈ No → ∀ b ∈ L ⁡ a ∪ R ⁡ a b + s 0 s = b → a + s 0 s = a
61 3 6 60 noinds ⊢ A ∈ No → A + s 0 s = A