Metamath Proof Explorer

Theorem mulscan2d

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

Ref Expression
Hypotheses mulscan2d.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
mulscan2d.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
mulscan2d.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
mulscan2d.4 ⊢ ( 𝜑 → 𝐶 ≠ 0s )
Assertion mulscan2d ( 𝜑 → ( ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 mulscan2d.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 mulscan2d.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
3 mulscan2d.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
4 mulscan2d.4 ⊢ ( 𝜑 → 𝐶 ≠ 0s )
5 0sno ⊢ 0s ∈ No
6 sltneg ⊢ ( ( 𝐶 ∈ No ∧ 0s ∈ No ) → ( 𝐶 <s 0s ↔ ( -us ‘ 0s ) <s ( -us ‘ 𝐶 ) ) )
7 3 5 6 sylancl ⊢ ( 𝜑 → ( 𝐶 <s 0s ↔ ( -us ‘ 0s ) <s ( -us ‘ 𝐶 ) ) )
8 negs0s ⊢ ( -us ‘ 0s ) = 0s
9 8 breq1i ⊢ ( ( -us ‘ 0s ) <s ( -us ‘ 𝐶 ) ↔ 0s <s ( -us ‘ 𝐶 ) )
10 7 9 bitrdi ⊢ ( 𝜑 → ( 𝐶 <s 0s ↔ 0s <s ( -us ‘ 𝐶 ) ) )
11 1 3 mulnegs2d ⊢ ( 𝜑 → ( 𝐴 ·s ( -us ‘ 𝐶 ) ) = ( -us ‘ ( 𝐴 ·s 𝐶 ) ) )
12 2 3 mulnegs2d ⊢ ( 𝜑 → ( 𝐵 ·s ( -us ‘ 𝐶 ) ) = ( -us ‘ ( 𝐵 ·s 𝐶 ) ) )
13 11 12 eqeq12d ⊢ ( 𝜑 → ( ( 𝐴 ·s ( -us ‘ 𝐶 ) ) = ( 𝐵 ·s ( -us ‘ 𝐶 ) ) ↔ ( -us ‘ ( 𝐴 ·s 𝐶 ) ) = ( -us ‘ ( 𝐵 ·s 𝐶 ) ) ) )
14 1 3 mulscld ⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ∈ No )
15 2 3 mulscld ⊢ ( 𝜑 → ( 𝐵 ·s 𝐶 ) ∈ No )
16 negs11 ⊢ ( ( ( 𝐴 ·s 𝐶 ) ∈ No ∧ ( 𝐵 ·s 𝐶 ) ∈ No ) → ( ( -us ‘ ( 𝐴 ·s 𝐶 ) ) = ( -us ‘ ( 𝐵 ·s 𝐶 ) ) ↔ ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ) )
17 14 15 16 syl2anc ⊢ ( 𝜑 → ( ( -us ‘ ( 𝐴 ·s 𝐶 ) ) = ( -us ‘ ( 𝐵 ·s 𝐶 ) ) ↔ ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ) )
18 13 17 bitrd ⊢ ( 𝜑 → ( ( 𝐴 ·s ( -us ‘ 𝐶 ) ) = ( 𝐵 ·s ( -us ‘ 𝐶 ) ) ↔ ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 0s <s ( -us ‘ 𝐶 ) ) → ( ( 𝐴 ·s ( -us ‘ 𝐶 ) ) = ( 𝐵 ·s ( -us ‘ 𝐶 ) ) ↔ ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ) )
20 1 adantr ⊢ ( ( 𝜑 ∧ 0s <s ( -us ‘ 𝐶 ) ) → 𝐴 ∈ No )
21 2 adantr ⊢ ( ( 𝜑 ∧ 0s <s ( -us ‘ 𝐶 ) ) → 𝐵 ∈ No )
22 3 negscld ⊢ ( 𝜑 → ( -us ‘ 𝐶 ) ∈ No )
23 22 adantr ⊢ ( ( 𝜑 ∧ 0s <s ( -us ‘ 𝐶 ) ) → ( -us ‘ 𝐶 ) ∈ No )
24 simpr ⊢ ( ( 𝜑 ∧ 0s <s ( -us ‘ 𝐶 ) ) → 0s <s ( -us ‘ 𝐶 ) )
25 20 21 23 24 mulscan2dlem ⊢ ( ( 𝜑 ∧ 0s <s ( -us ‘ 𝐶 ) ) → ( ( 𝐴 ·s ( -us ‘ 𝐶 ) ) = ( 𝐵 ·s ( -us ‘ 𝐶 ) ) ↔ 𝐴 = 𝐵 ) )
26 19 25 bitr3d ⊢ ( ( 𝜑 ∧ 0s <s ( -us ‘ 𝐶 ) ) → ( ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ↔ 𝐴 = 𝐵 ) )
27 10 26 sylbida ⊢ ( ( 𝜑 ∧ 𝐶 <s 0s ) → ( ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ↔ 𝐴 = 𝐵 ) )
28 1 adantr ⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → 𝐴 ∈ No )
29 2 adantr ⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → 𝐵 ∈ No )
30 3 adantr ⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → 𝐶 ∈ No )
31 simpr ⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → 0s <s 𝐶 )
32 28 29 30 31 mulscan2dlem ⊢ ( ( 𝜑 ∧ 0s <s 𝐶 ) → ( ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ↔ 𝐴 = 𝐵 ) )
33 slttrine ⊢ ( ( 𝐶 ∈ No ∧ 0s ∈ No ) → ( 𝐶 ≠ 0s ↔ ( 𝐶 <s 0s ∨ 0s <s 𝐶 ) ) )
34 3 5 33 sylancl ⊢ ( 𝜑 → ( 𝐶 ≠ 0s ↔ ( 𝐶 <s 0s ∨ 0s <s 𝐶 ) ) )
35 4 34 mpbid ⊢ ( 𝜑 → ( 𝐶 <s 0s ∨ 0s <s 𝐶 ) )
36 27 32 35 mpjaodan ⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐶 ) = ( 𝐵 ·s 𝐶 ) ↔ 𝐴 = 𝐵 ) )