Metamath Proof Explorer

Theorem mulscan2d

Description: Cancellation of surreal multiplication when the right term is nonzero. (Contributed by Scott Fenton, 10-Mar-2025)

Ref Expression
Hypotheses mulscan2d.1 ⊢ φ → A ∈ No
mulscan2d.2 ⊢ φ → B ∈ No
mulscan2d.3 ⊢ φ → C ∈ No
mulscan2d.4 ⊢ φ → C ≠ 0 s
Assertion mulscan2d ⊢ φ → A ⋅ s C = B ⋅ s C ↔ A = B

Proof

Step Hyp Ref Expression
1 mulscan2d.1 ⊢ φ → A ∈ No
2 mulscan2d.2 ⊢ φ → B ∈ No
3 mulscan2d.3 ⊢ φ → C ∈ No
4 mulscan2d.4 ⊢ φ → C ≠ 0 s
5 0no ⊢ 0 s ∈ No
6 ltnegs ⊢ C ∈ No ∧ 0 s ∈ No → C < s 0 s ↔ + s ⁡ 0 s < s + s ⁡ C
7 3 5 6 sylancl ⊢ φ → C < s 0 s ↔ + s ⁡ 0 s < s + s ⁡ C
8 neg0s ⊢ + s ⁡ 0 s = 0 s
9 8 breq1i ⊢ + s ⁡ 0 s < s + s ⁡ C ↔ 0 s < s + s ⁡ C
10 7 9 bitrdi ⊢ φ → C < s 0 s ↔ 0 s < s + s ⁡ C
11 1 3 mulnegs2d ⊢ φ → A ⋅ s + s ⁡ C = + s ⁡ A ⋅ s C
12 2 3 mulnegs2d ⊢ φ → B ⋅ s + s ⁡ C = + s ⁡ B ⋅ s C
13 11 12 eqeq12d ⊢ φ → A ⋅ s + s ⁡ C = B ⋅ s + s ⁡ C ↔ + s ⁡ A ⋅ s C = + s ⁡ B ⋅ s C
14 1 3 mulscld ⊢ φ → A ⋅ s C ∈ No
15 2 3 mulscld ⊢ φ → B ⋅ s C ∈ No
16 negs11 ⊢ A ⋅ s C ∈ No ∧ B ⋅ s C ∈ No → + s ⁡ A ⋅ s C = + s ⁡ B ⋅ s C ↔ A ⋅ s C = B ⋅ s C
17 14 15 16 syl2anc ⊢ φ → + s ⁡ A ⋅ s C = + s ⁡ B ⋅ s C ↔ A ⋅ s C = B ⋅ s C
18 13 17 bitrd ⊢ φ → A ⋅ s + s ⁡ C = B ⋅ s + s ⁡ C ↔ A ⋅ s C = B ⋅ s C
19 18 adantr ⊢ φ ∧ 0 s < s + s ⁡ C → A ⋅ s + s ⁡ C = B ⋅ s + s ⁡ C ↔ A ⋅ s C = B ⋅ s C
20 1 adantr ⊢ φ ∧ 0 s < s + s ⁡ C → A ∈ No
21 2 adantr ⊢ φ ∧ 0 s < s + s ⁡ C → B ∈ No
22 3 negscld ⊢ φ → + s ⁡ C ∈ No
23 22 adantr ⊢ φ ∧ 0 s < s + s ⁡ C → + s ⁡ C ∈ No
24 simpr ⊢ φ ∧ 0 s < s + s ⁡ C → 0 s < s + s ⁡ C
25 20 21 23 24 mulscan2dlem ⊢ φ ∧ 0 s < s + s ⁡ C → A ⋅ s + s ⁡ C = B ⋅ s + s ⁡ C ↔ A = B
26 19 25 bitr3d ⊢ φ ∧ 0 s < s + s ⁡ C → A ⋅ s C = B ⋅ s C ↔ A = B
27 10 26 sylbida ⊢ φ ∧ C < s 0 s → A ⋅ s C = B ⋅ s C ↔ A = B
28 1 adantr ⊢ φ ∧ 0 s < s C → A ∈ No
29 2 adantr ⊢ φ ∧ 0 s < s C → B ∈ No
30 3 adantr ⊢ φ ∧ 0 s < s C → C ∈ No
31 simpr ⊢ φ ∧ 0 s < s C → 0 s < s C
32 28 29 30 31 mulscan2dlem ⊢ φ ∧ 0 s < s C → A ⋅ s C = B ⋅ s C ↔ A = B
33 ltstrine ⊢ C ∈ No ∧ 0 s ∈ No → C ≠ 0 s ↔ C < s 0 s ∨ 0 s < s C
34 3 5 33 sylancl ⊢ φ → C ≠ 0 s ↔ C < s 0 s ∨ 0 s < s C
35 4 34 mpbid ⊢ φ → C < s 0 s ∨ 0 s < s C
36 27 32 35 mpjaodan ⊢ φ → A ⋅ s C = B ⋅ s C ↔ A = B